(def-language lct-language (embedded-language groups) (constants (a"sets[gg]") (b"sets[gg]")))

(def-theory lct-theory (language lct-language) (component-theories groups) (axioms (a-is-a-subgroup"subgroup(a)") (b-is-a-subgroup"subgroup(b)")))

(def-compound-macete lct-macete (repeat subgroup-membership a-is-a-subgroup b-is-a-subgroup))

(def-theorem a-contains-e"e in a"(theory lct-theory) (usages rewrite) (proof ( (apply-macete-with-minor-premises lct-macete) )))

(def-theorem b-contains-e"e in b"(theory lct-theory) (usages rewrite) (proof ( (apply-macete-with-minor-premises lct-macete) )))

(def-atomic-sort b%sort"lambda(x:gg, x in b)"(theory lct-theory) (witness"e"))

(def-constant a%cosets"indic{c:sets[gg], forsome(g:gg, g in b and c = right%trans(a,g))}"(theory lct-theory))

(def-theorem a%cosets-contains-a"a in a%cosets"(theory lct-theory) (proof ( (unfold-single-defined-constant-globally a%cosets) simplify (instantiate-existential ("e")) simplify (apply-macete-with-minor-premises trivial-right-translation) )))

(def-atomic-sort a%cosets%sort"lambda(x:sets[gg], x in a%cosets)"(theory lct-theory) (witness"a"))

(def-theorem a-is-defined-in-a%cosets%sort"#(a,a%cosets%sort)"lemma (theory lct-theory) (usages rewrite) (proof ( (apply-macete-with-minor-premises a%cosets%sort-defining-axiom_lct-theory) beta-reduce-repeatedly (apply-macete-with-minor-premises a%cosets-contains-a) )))

(def-theorem b%sort-members-are-in-b"forall(x:b%sort, x=x implies x in b)"lemma (theory lct-theory) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem b%sort-defining-axiom_lct-theory ("x")) (contrapose"with(x:b%sort,not(#(x,b%sort)))") )))

(def-theorem b-is-total"total_q{b,sets[b%sort]} iff truth"(theory lct-theory) (usages rewrite) (proof ( simplify insistent-direct-inference (apply-macete-with-minor-premises b%sort-members-are-in-b) )))

(def-theorem a%cosets%sort-members-are-in-a%cosets"forall(x:a%cosets%sort, x=x implies x in a%cosets)"lemma (theory lct-theory) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem a%cosets%sort-defining-axiom_lct-theory ("x")) (contrapose"with(x:a%cosets%sort,not(#(x,a%cosets%sort)))") )))

(def-theorem a%cosets-is-total"total_q{a%cosets,sets[a%cosets%sort]} iff truth"(theory lct-theory) (usages rewrite) (proof ( simplify insistent-direct-inference (apply-macete-with-minor-premises a%cosets%sort-members-are-in-a%cosets) )))

(def-translation lct-interpretation (source group-actions) (target lct-theory) (fixed-theories h-o-real-arithmetic) (sort-pairs (gg"b%sort") (uu"a%cosets%sort")) (constant-pairs (mul"restrict2{mul,b,b}") (inv"restrict{inv,b}") (act"restrict2{right%trans,a%cosets,b}")) force-under-quick-load (theory-interpretation-check using-simplification))

(def-transported-symbols (gg%subgroup orbit stabilizer) (translation lct-interpretation) (renamer lct-renamer))

(def-theorem finiteness-of-a"f_indic_q{gg%subgroup} implies f_indic_q{a}"lemma (theory lct-theory) (proof ( direct-inference (apply-macete-with-minor-premises finiteness-of-subgroups) (apply-macete-with-minor-premises a-is-a-subgroup) )))

(def-theorem finiteness-of-b"f_indic_q{gg%subgroup} implies f_indic_q{b}"lemma (theory lct-theory) (proof ( direct-inference (apply-macete-with-minor-premises finiteness-of-subgroups) (apply-macete-with-minor-premises b-is-a-subgroup) )))

(def-theorem finiteness-of-a-inters-b"f_indic_q{gg%subgroup} implies f_indic_q{a inters b}"lemma (theory lct-theory) (proof ( direct-inference (apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite) (instantiate-existential ("gg%subgroup")) insistent-direct-inference (unfold-single-defined-constant-globally gg%subgroup) simplify )))

(def-theorem finiteness-of-ab"f_indic_q{gg%subgroup} implies f_indic_q{a set%mul b}"lemma (theory lct-theory) (proof ( direct-inference (apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite) (instantiate-existential ("gg%subgroup")) insistent-direct-inference unfold-defined-constants simplify )))

(def-theorem b-is-lct%gg%subgroup"b=lct%gg%subgroup"lemma reverse (theory lct-theory) (proof ( (unfold-single-defined-constant-globally lct%gg%subgroup) extensionality direct-inference (case-split ("#(x_0,b%sort)")) simplify (apply-macete-with-minor-premises tr%value-of-a-defined-indicator-application) (apply-macete-with-minor-premises b%sort-members-are-in-b) simplify (contrapose"with(p:prop,p)") simplify )))

(def-theorem f-card-of-b"f_card{b} == f_card{lct%gg%subgroup}"lemma reverse (theory lct-theory) (proof ( (apply-macete-with-minor-premises tr%equinumerous-implies-f-card-quasi-equal) (instantiate-existential ("id{b}")) (apply-macete-with-minor-premises tr%dom-of-id) (block (script-comment"node added by `instantiate-existential' at (0 0 1)") (unfold-single-defined-constant-globally lct%gg%subgroup) extensionality direct-inference simplify (apply-macete-with-minor-premises b%sort-members-are-in-b)) (apply-macete-with-minor-premises tr%id-is-injective-on-dom) (block (script-comment"node added by `instantiate-existential' at (1)") sort-definedness simplify) )))

(def-theorem finiteness-of-lct%gg%subgroup"f_indic_q{b} implies f_indic_q{lct%gg%subgroup}"lemma (theory lct-theory) (proof ( direct-inference (assume-theorem f-card-of-b) )))

(def-theorem lct%orbit-of-a-is-a%cosets"lct%orbit(a)=a%cosets"lemma (theory lct-theory) (proof ( unfold-defined-constants extensionality direct-inference (case-split ("#(x_0,a%cosets%sort)")) (block (script-comment"node added by `case-split' at (1)") simplify direct-and-antecedent-inference-strategy auto-instantiate-existential (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (1 0 0)") (contrapose"with(p:prop,not(p));") auto-instantiate-existential (apply-macete-with-minor-premises a%cosets-contains-a))) (block (script-comment"node added by `case-split' at (2)") simplify direct-and-antecedent-inference-strategy (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises a%cosets%sort-defining-axiom_lct-theory) (unfold-single-defined-constant-globally a%cosets) simplify auto-instantiate-existential) )))

(def-theorem f-card-of-lct%orbit-at-a"f_card{lct%orbit(a)} == f_card{a%cosets}"lemma (theory lct-theory) (proof ( (assume-theorem lct%orbit-of-a-is-a%cosets) (apply-macete-with-minor-premises tr%equinumerous-implies-f-card-quasi-equal) (instantiate-existential ("id{lct%orbit(a)}")) insistent-direct-inference (block (script-comment"node added by `insistent-direct-inference' at (0)") insistent-direct-inference (apply-macete-with-minor-premises tr%dom-of-id) (block (script-comment"node added by `insistent-direct-inference' at (1)") (backchain"with(f:sets[a%cosets%sort],f=a%cosets);") extensionality direct-inference simplify)) (apply-macete-with-minor-premises tr%id-is-injective-on-dom) )))

(def-theorem lct%stabilizer-of-a-is-a-inters-b"lct%stabilizer(a) = a inters b"lemma (theory lct-theory) (proof ( (unfold-single-defined-constant-globally lct%stabilizer) extensionality direct-inference (case-split ("#(x_0,b%sort)")) (block (script-comment"node added by `case-split' at (1)") simplify (apply-macete-with-minor-premises subgroup-is-right%trans-stabilizer) (block (script-comment"node added by `apply-macete-with-minor-premises' at (0)") direct-and-antecedent-inference-strategy (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises a%cosets-contains-a) simplify) (apply-macete-with-minor-premises a-is-a-subgroup)) (block (script-comment"node added by `case-split' at (2)") simplify (contrapose"with(p:prop,p);") (apply-macete-with-minor-premises b%sort-defining-axiom_lct-theory)) )))

(def-theorem f-card-of-lct%stabilizer-at-a"f_card{lct%stabilizer(a)} == f_card{a inters b}"lemma (theory lct-theory) (proof ( (assume-theorem lct%stabilizer-of-a-is-a-inters-b) (apply-macete-with-minor-premises tr%equinumerous-implies-f-card-quasi-equal) (instantiate-existential ("id{lct%stabilizer(a)}")) insistent-direct-inference (block (script-comment"node added by `insistent-direct-inference' at (0)") insistent-direct-inference (apply-macete-with-minor-premises tr%dom-of-id) (block (script-comment"node added by `insistent-direct-inference' at (1)") (backchain"lct%stabilizer(a)=a inters b;") extensionality direct-inference simplify)) (apply-macete-with-minor-premises tr%id-is-injective-on-dom) )))

(def-theorem a%cosets-is-a-partition-of-ab"partition_q{a%cosets, a set%mul b}"lemma (theory lct-theory) (proof ( unfold-defined-constants insistent-direct-inference (block (script-comment"node added by `insistent-direct-inference' at (0)") simplify direct-and-antecedent-inference-strategy (incorporate-antecedent"with(p:prop,not(p));") (force-substitution"u ""right%trans(a,g_$0)"(0 1)) (force-substitution"v""right%trans(a,g)"(0 1)) (weaken (0 1 2 3)) (instantiate-theorem overlapping-right-cosets ("a""g_$0""g")) (block (script-comment"node added by `instantiate-theorem' at (0 0)") (contrapose"with(p:prop,p);") (apply-macete-with-minor-premises a-is-a-subgroup)) simplify simplify) (block (script-comment"node added by `insistent-direct-inference' at (1)") (weaken (0)) simplify direct-and-antecedent-inference-strategy (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (0 0 0 0)") (instantiate-existential ("right%trans(a,i)")) (instantiate-existential ("i")) (block (script-comment"node added by `instantiate-existential' at (0 1)") (unfold-single-defined-constant-globally right%trans) simplify auto-instantiate-existential)) (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (0 1 0 0 0 0)") (incorporate-antecedent"with(x:gg,u:sets[gg],x in u);") (backchain"with(f,u:sets[gg],u=f);") (unfold-single-defined-constant-globally right%trans) (weaken (1)) simplify direct-and-antecedent-inference-strategy (instantiate-existential ("g""i")))) )))

(def-theorem finiteness-of-a%cosets"f_indic_q{gg%subgroup} implies f_indic_q{a%cosets}"lemma (theory lct-theory) (proof ( direct-inference (assume-theorem a%cosets-is-a-partition-of-ab) (antecedent-inference"partition_q{a%cosets,a set%mul b}") (apply-macete-with-minor-premises tr%finiteness-of-a-partition) auto-instantiate-existential (apply-macete-with-minor-premises finiteness-of-ab) )))

(def-theorem a%cosets-are-equinumerous"forall(c:sets[gg], c in a%cosets implies c equinumerous a)"lemma (theory lct-theory) (proof ( (unfold-single-defined-constant-globally a%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"a""right%trans(a,e)"(1)) (apply-macete-with-minor-premises right-cosets-are-equinumerous) (apply-macete-with-minor-premises trivial-right-translation) )))

(def-theorem a%cosets-have-equal-f-card"forall(c:sets[gg], f_indic_q{a} and c in a%cosets implies f_card{c} = f_card{a})"lemma (theory lct-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 a%cosets-are-equinumerous) (apply-macete-with-minor-premises a%cosets-are-equinumerous) )))

(def-theorem a-has-positive-f-card"f_indic_q{gg%subgroup} implies 0 < f_card{a}"lemma (theory lct-theory) (proof ( direct-inference (cut-with-single-formula"f_indic_q{a}") (apply-macete-with-minor-premises tr%positive-f-card-iff-nonempty) (instantiate-existential ("e")) simplify (apply-macete-with-minor-premises finiteness-of-a) )))

(def-theorem a%cosets-has-positive-f-card"f_indic_q{gg%subgroup} implies 0 < f_card{a%cosets}"lemma (theory lct-theory) (proof ( direct-inference (cut-with-single-formula"f_indic_q{a%cosets}") (apply-macete-with-minor-premises tr%positive-f-card-iff-nonempty) (instantiate-existential ("a")) (apply-macete-with-minor-premises a%cosets-contains-a) (apply-macete-with-minor-premises finiteness-of-a%cosets) )))

(def-theorem little-counting-theorem"f_indic_q{gg%subgroup} implies f_card{a set%mul b}*f_card{a inters b} = f_card{a}*f_card{b}"(theory groups) (home-theory lct-theory) (usages transportable-macete) (proof; 50 nodes ( direct-inference (cut-with-single-formula"0<f_card{a}") (cut-with-single-formula"f_indic_q{b}") (cut-with-single-formula"0<f_card{a%cosets}") (cut-with-single-formula"f_indic_q{lct%gg%subgroup}") (cut-with-single-formula"f_indic_q{a set%mul b}") (cut-with-single-formula"f_indic_q{a inters b}") (apply-macete-with-minor-premises f-card-of-b) (instantiate-transported-theorem fundamental-counting-theorem lct-interpretation ("a")) (backchain"with(m,n:nn, m=n)") (apply-macete-with-minor-premises f-card-of-lct%orbit-at-a) (apply-macete-with-minor-premises f-card-of-lct%stabilizer-at-a) (assume-theorem a%cosets-is-a-partition-of-ab) (instantiate-transported-theorem finite-uniform-partition-theorem () ("a%cosets""a set%mul b""f_card{a}")) (contrapose"with(p:prop, not(p))") (apply-macete-with-minor-premises a%cosets-have-equal-f-card) (apply-macete-with-minor-premises a%cosets-contains-a) (backchain"f_card{a set%mul b}=f_card{a}*f_card{a%cosets}") simplify (apply-macete-with-minor-premises finiteness-of-a-inters-b) (apply-macete-with-minor-premises finiteness-of-ab) (apply-macete-with-minor-premises finiteness-of-lct%gg%subgroup) (apply-macete-with-minor-premises a%cosets-has-positive-f-card) (apply-macete-with-minor-premises finiteness-of-b) (apply-macete-with-minor-premises a-has-positive-f-card) )))