(def-language counting-theorem-language
    (embedded-language group-actions-language)
    (constants
        (zeta uu)))

(def-theory counting-theorem-theory 
    (language counting-theorem-language)
    (component-theories group-actions))

(def-constant fct%mapping 
    "lambda(beta:uu, 
          iota(c:sets[gg], 
              forsome(g:gg, 
                  c = right%trans(stabilizer(zeta),g) and beta = act(zeta,g))))"
    (theory counting-theorem-theory))

(def-constant stabilizer%right%cosets 
    "indic{a:sets[gg], forsome(g:gg, a = right%trans(stabilizer(zeta),g))}"
    (theory counting-theorem-theory))

(def-theorem cardinality-of-zeta-orbit 
    "orbit(zeta) equinumerous stabilizer%right%cosets"
    lemma
    (theory counting-theorem-theory)
    (proof
      (
        (instantiate-existential ("fct%mapping"))
        insistent-direct-inference
        insistent-direct-inference
        (apply-macete-with-minor-premises domain-of-fct-mapping)
        (apply-macete-with-minor-premises range-of-fct-mapping)
        (apply-macete-with-minor-premises tr%injective-implies-injective-on)
        (apply-macete-with-minor-premises injectiveness-of-fct-mapping)
        )))

(def-theorem cardinality-of-a-finite-zeta-orbit 
    "f_indic_q{orbit(zeta)} 
          implies 
      f_card{orbit(zeta)} = f_card{stabilizer%right%cosets}"
    reverse
    lemma
    (theory counting-theorem-theory)
    (proof
      (
        direct-inference
        (apply-macete-with-minor-premises 
          tr%finite-and-equinumerous-implies-f-card-equal)
        (apply-macete-with-minor-premises cardinality-of-zeta-orbit)
        )))

(def-theorem stabilizer%right%cosets-are-equinumerous 
    "forall(a:sets[gg],
          a in stabilizer%right%cosets implies a equinumerous stabilizer(zeta))"
    lemma
    (theory counting-theorem-theory)
    (proof
      (
        (unfold-single-defined-constant-globally stabilizer%right%cosets)
        direct-and-antecedent-inference-strategy
        (contrapose "with(p:prop, p)")
        simplify
        (contrapose "with(p:prop, p)")
        (antecedent-inference "with(p:prop, p)")
        (backchain "with(p:prop, p)")
        (weaken (0))
        (force-substitution 
          "stabilizer(zeta)" "right%trans(stabilizer(zeta),e)" (1))
        (apply-macete-with-minor-premises right-cosets-are-equinumerous)
        (apply-macete-with-minor-premises trivial-right-translation)
        )))

(def-theorem stabilizer%right%cosets-have-equal-f-card 
    "forall(a:sets[gg],
          f_indic_q{stabilizer(zeta)} and a in stabilizer%right%cosets 
              implies 
          f_card{a} = f_card{stabilizer(zeta)})"
    lemma
    (theory counting-theorem-theory)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises 
          tr%f-card-equal-iff-finite-and-equinumerous)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises 
          stabilizer%right%cosets-are-equinumerous)
        (apply-macete-with-minor-premises 
          stabilizer%right%cosets-are-equinumerous)
        )))

(def-theorem finiteness-of-zeta-stabilizer 
    "f_indic_q{gg%subgroup} implies f_indic_q{stabilizer(zeta)}"
    lemma
    (theory counting-theorem-theory)
    (proof
      (
        direct-inference
        (apply-macete-with-minor-premises finiteness-of-stabilizers)
        )))

(def-theorem stabilizer%right%cosets-is-a-partition 
    "partition_q{stabilizer%right%cosets,gg%subgroup}"
    lemma
    (theory counting-theorem-theory)
    (proof
      (
        (unfold-single-defined-constant-globally stabilizer%right%cosets)
        insistent-direct-inference
        simplify
        direct-and-antecedent-inference-strategy
        (incorporate-antecedent "with(v,u:sets[gg],not(u=v))")
        (backchain "with(g_$0:gg,u:sets[gg],u=right%trans(stabilizer(zeta),g_$0))")
        (backchain "with(g_$0:gg,u:sets[gg],u=right%trans(stabilizer(zeta),g_$0))")
        (backchain "with(g:gg,v:sets[gg],v=right%trans(stabilizer(zeta),g))")
        (backchain "with(g:gg,v:sets[gg],v=right%trans(stabilizer(zeta),g))")
        (weaken (0 1))
        (instantiate-theorem 
          overlapping-right-cosets ("stabilizer(zeta)" "g_$0" "g"))
        (contrapose "with(p:prop, p)")
        (apply-macete-with-minor-premises stabilizers-are-subgroups)
        simplify
        simplify
        (weaken (0))
        simplify
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("right%trans(stabilizer(zeta),x)"))
        (instantiate-existential ("x"))
        (unfold-single-defined-constant-globally right%trans)
        simplify
        (instantiate-existential ("e"))
        (apply-macete-with-minor-premises subgroups-contain-e)
        (apply-macete-with-minor-premises stabilizers-are-subgroups)
        simplify
        (unfold-single-defined-constant-globally gg%subgroup)
        simplify
        )))

(def-theorem finiteness-of-zeta-orbit 
    "f_indic_q{gg%subgroup} implies f_indic_q{orbit(zeta)}"
    (theory counting-theorem-theory)
    (proof
      (
        direct-inference
        (assume-theorem cardinality-of-zeta-orbit)
        (cut-with-single-formula 
          "f_card{orbit(zeta)} = f_card{stabilizer%right%cosets}")
        (apply-macete-with-minor-premises 
          tr%f-card-equal-iff-finite-and-equinumerous)
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula 
          "partition_q{stabilizer%right%cosets,gg%subgroup}")
        (apply-macete-with-minor-premises tr%finiteness-of-a-partition)
        (antecedent-inference "partition_q{stabilizer%right%cosets,gg%subgroup};")
        (instantiate-existential ("gg%subgroup"))
        (apply-macete-with-minor-premises stabilizer%right%cosets-is-a-partition)
        )))

(def-theorem finiteness-of-orbits 
    finiteness-of-zeta-orbit
    (theory group-actions)
    (home-theory counting-theorem-theory)
    (usages transportable-macete)
    (proof existing-theorem))

(def-theorem fundamental-counting-theorem 
    "f_indic_q{gg%subgroup} 
          implies 
      f_card{gg%subgroup} = f_card{stabilizer(zeta)} * f_card{orbit(zeta)}"
    (theory group-actions)
    (home-theory counting-theorem-theory)
    (usages transportable-macete)
    (proof
      (
        direct-inference
        (cut-with-single-formula "f_indic_q{stabilizer(zeta)}")
        (cut-with-single-formula "f_indic_q{orbit(zeta)}")
        (cut-with-single-formula 
          "f_card{orbit(zeta)}=f_card{stabilizer%right%cosets}")
        (backchain "f_card{orbit(zeta)}=f_card{stabilizer%right%cosets}")
        (assume-theorem stabilizer%right%cosets-is-a-partition)
        (antecedent-inference "partition_q{stabilizer%right%cosets,gg%subgroup}")
        (apply-macete-with-minor-premises tr%finite-uniform-partition-theorem)
        direct-inference
        (apply-macete stabilizer%right%cosets-have-equal-f-card)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises rev%cardinality-of-a-finite-zeta-orbit)
        (apply-macete-with-minor-premises finiteness-of-zeta-orbit)
        (apply-macete-with-minor-premises finiteness-of-zeta-stabilizer)
        )))

(def-theorem lagranges-theorem 
    "forall(a:sets[gg], 
          f_indic_q{gg%subgroup} and subgroup(a) 
              implies 
          forsome(m:nn, f_card{gg%subgroup} = m * f_card{a}))"
    (theory groups)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-transported-theorem 
          fundamental-counting-theorem 
          act->right%trans 
          ("a"))
        (force-substitution "a" "indic{g:gg,right%trans(a,g)=a}" (0))
        (instantiate-existential ("f_card{right%cosets(a)}"))
        simplify
        (apply-macete-with-minor-premises subgroup-is-right%trans-stabilizer)
        (apply-macete-with-minor-premises tr%dom-of-an-indicator)
        )))

(def-constant conjugate%class 
    "lambda(g:gg, indic{h:gg, forsome(i:gg, h = inv(i) mul g mul i)})"
    (theory groups))

(def-constant normalizer 
    "lambda(g:gg, indic{h:gg, inv(h) mul g mul h = g})"
    (theory groups))

(def-theorem index-of-normalizer 
    "forall(g:gg, 
          f_indic_q{gg%subgroup}
              implies
          f_card{gg%subgroup} = 
          f_card{normalizer(g)}*f_card{conjugate%class(g)})"
    (theory groups)
    (usages transportable-macete)
    (proof
      (
        (assume-transported-theorem 
          fundamental-counting-theorem act->conjugate)
        )))
          

(def-constant set%conjugate%class 
    "lambda(a:sets[gg], 
          indic{b:sets[gg], forsome(g:gg, b = set%conjugate(a,g))})"
    (theory groups))

(def-constant set%normalizer 
    "lambda(a:sets[gg], indic{g:gg, set%conjugate(a,g) = a})"
    (theory groups))

(def-theorem index-of-set-normalizer 
    "forall(a:sets[gg],
          f_indic_q{gg%subgroup}
              implies
          f_card{gg%subgroup} = 
          f_card{set%normalizer(a)}*f_card{set%conjugate%class(a)})"
    (theory groups)
    (usages transportable-macete)
    (proof
      (
        (assume-transported-theorem 
          fundamental-counting-theorem act->set%conjugate)
        )))