(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)
)))