```(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}"))
(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)
)))
```