```
(def-constant normal
"lambda(a:sets[gg],
forall(g,h:gg, h in a implies (g mul h mul inv(g)) in a))"
(theory groups))
```

```
(def-constant right%coset%app
"lambda(f:[gg,gg],a:sets[gg],
lambda(b:sets[gg],
iota(c:sets[gg],
forsome(g:gg, b = right%trans(a,g) and
c = right%trans(a,f(g))))))"
(theory groups))
```

```
(def-constant right%cosets
"lambda(a:sets[gg],
indic{b:sets[gg], forsome(g:gg, b=right%trans(a,g))})"
(theory groups))
```

```
(def-theorem right%coset%app-is-total
"total_q{right%coset%app,[[gg,gg],sets[gg],[sets[gg],sets[gg]]]}"
(theory groups)
(usages d-r-convergence)
(proof
(
(unfold-single-defined-constant-globally right%coset%app)
simplify-insistently
)))
```

```
(def-theorem right%cosets-is-total
"total_q{right%cosets,[sets[gg],sets[sets[gg]]]}"
(theory groups)
(usages d-r-convergence)
(proof
(
(unfold-single-defined-constant-globally right%cosets)
simplify-insistently
)))
```

```
(def-theorem right%cosets-membership
"forall(a,b:sets[gg],
a in right%cosets(b) iff forsome(g:gg, a = right%trans(b,g)))"
(theory groups)
(usages transportable-macete)
(proof
(
(unfold-single-defined-constant-globally right%cosets)
simplify-insistently
)))
```

```
(def-theorem normal-iff-cosets-property
"forall(a:sets[gg],
normal(a) iff forall(g:gg, left%trans(g,a) = right%trans(a,g)))"
(theory groups)
(usages transportable-macete)
(proof; 61 nodes
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (0 0 0)")
extensionality
direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (0 0 0)")
(instantiate-existential ("(g mul i) mul inv(g)"))
(block
(script-comment "node added by `instantiate-existential' at (0 0)")
(backchain "with(g,x_0:gg,x_0=g);")
(backchain "with(p:prop,forall(g,h:gg,p));"))
simplify)
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (1 0 0)")
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("(inv(g) mul i) mul inv(inv(g))"))
(backchain "with(p:prop,forall(g,h:gg,p));")
simplify))
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (0 1 0 0)")
(instantiate-universal-antecedent "with(p:prop,forall(g:gg,p));" ("g"))
(incorporate-antecedent "with(f:sets[gg],f=f);")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent
"with(g:gg,a:sets[gg],
indic{h:gg,  forsome(i:gg,i in a and h=g mul i)}
subseteq
indic{h:gg,  forsome(i:gg, i in a and h=i mul g)});"
("g mul h"))
(block
(script-comment
"node added by `instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(p:prop,not(p));")
simplify-insistently
auto-instantiate-existential)
(block
(script-comment
"node added by `instantiate-universal-antecedent' at (0 0 1)")
(contrapose "with(h,g:gg,f:[gg,prop],(g mul h) in pred_to_indic(f));")
simplify-insistently
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,not(p));")
(force-substitution "g mul h" "i_\$0 mul g" (0))
(weaken (0))
simplify))
)))
```

```
(def-theorem normal-iff-conjugates-property
"forall(a:sets[gg],
normal(a) iff forall(g:gg, set%conjugate(a,g) = a))"
(theory groups)
(usages transportable-macete)
(proof; 18 nodes
(
(unfold-single-defined-constant-globally set%conjugate)
(force-substitution
"right%trans(left%trans(inv(g),a),g)=a"
"left%trans(inv(g),a) = right%trans(a,inv(g))"
(0))
(apply-macete-with-minor-premises normal-iff-cosets-property)
direct-and-antecedent-inference-strategy
(backchain "with(p:prop, forall(g:gg,p))")
(force-substitution "g" "inv(inv(g))" (0 1))
(backchain "with(p:prop, forall(g:gg,p))")
simplify
(force-substitution
"right%trans(left%trans(inv(g),a),g)=a"
"right%trans(right%trans(left%trans(inv(g),a),g),inv(g)) =
right%trans(a,inv(g))"
(0))
simplify
(apply-macete-with-minor-premises rev%right-translation-macete)
)))
```

```
(def-theorem normal-implies-cosets-property
"forall(a:sets[gg],g:gg,
normal(a) implies left%trans(g,a) = right%trans(a,g))"
(theory groups)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem normal-iff-cosets-property ("a"))
(backchain "with(p:prop, forall(g:gg,p))")
)))
```

```
(def-compound-macete simplify-normal-subgroup-expressions
(repeat
(without-minor-premises normal-implies-cosets-property)
(without-minor-premises idempotence-of-subgroups)
set%mul-right%trans-associativity
right%trans-set%mul-associativity))
```

```
(def-theorem right-coset-inversion
"forall(a:sets[gg],g:gg,
normal(a)
implies
right%coset%app(inv,a)(right%trans(a,g)) = right%trans(a,inv(g)))"
(theory groups)
(usages transportable-macete)
(proof; 36 nodes
(
(unfold-single-defined-constant-globally right%coset%app)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises eliminate-iota-macete)
direct-and-antecedent-inference-strategy
(instantiate-existential ("g"))
(force-substitution "b_\$0" "right%trans(a,inv(g_\$0))" (0))
(weaken (2))
(instantiate-theorem normal-iff-cosets-property ("a"))
(apply-macete-with-minor-premises right-translation-macete)
(instantiate-existential ("g"))
simplify
(backchain-backwards "with(p:prop, forall(g:gg,p))")
(apply-macete-with-minor-premises right%trans-left%trans-associativity)
(backchain
"with(g_\$0,g:gg,a:sets[gg], right%trans(a,g)=right%trans(a,g_\$0));")
(backchain-backwards "with(p:prop, forall(g:gg,p))")
simplify
)))
```

```
(def-theorem right-coset-multiplication
"forall(a:sets[gg],
subgroup(a) and normal(a)
implies
forall(g,h:gg,
right%trans(a,g) set%mul right%trans(a,h)
=
right%trans(a, g mul h)))"
(theory groups)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises simplify-normal-subgroup-expressions)
(apply-macete-with-minor-premises simplify-set-translations)
)))
```

```
(def-compound-macete simplify-right-coset-expressions
(series
(repeat
(without-minor-premises right-coset-inversion)
(without-minor-premises right-coset-multiplication))
simplify))
```

```
(def-theorem right-coset-left-identity
"forall(a,b:sets[gg],
subgroup(a) and normal(a) and b in right%cosets(a)
implies
a set%mul b = b)"
(theory groups)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises right%cosets-membership)
direct-and-antecedent-inference-strategy
(force-substitution "b" "right%trans(a,g)" (0 1))
(force-substitution "a" "right%trans(a,e)" (0))
(apply-macete-with-minor-premises simplify-right-coset-expressions)
simplify
)))
```

```
(def-theorem right-coset-right-identity
"forall(a,b:sets[gg],
subgroup(a) and normal(a) and b in right%cosets(a)
implies
b set%mul a = b)"
(theory groups)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises right%cosets-membership)
direct-and-antecedent-inference-strategy
(force-substitution "b" "right%trans(a,g)" (0 1))
(force-substitution "a" "right%trans(a,e)" (1))
(apply-macete-with-minor-premises simplify-right-coset-expressions)
simplify
)))
```

```
(def-theorem right-coset-left-inverse
"forall(a,b:sets[gg],
subgroup(a) and normal(a) and b in right%cosets(a)
implies
right%coset%app(inv,a)(b) set%mul b = a)"
(theory groups)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises right%cosets-membership)
direct-and-antecedent-inference-strategy
(force-substitution "b" "right%trans(a,g)" (0 1))
(force-substitution "a" "right%trans(a,e)" (0))
(weaken (0))
simplify
(apply-macete-with-minor-premises simplify-right-coset-expressions)
simplify
)))
```

```
(def-theorem right-coset-right-inverse
"forall(a,b:sets[gg],
subgroup(a) and normal(a) and b in right%cosets(a)
implies
b set%mul right%coset%app(inv,a)(b) = a)"
(theory groups)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises right%cosets-membership)
direct-and-antecedent-inference-strategy
(force-substitution "b" "right%trans(a,g)" (0 1))
(force-substitution "a" "right%trans(a,e)" (1))
(weaken (0))
simplify
(apply-macete-with-minor-premises simplify-right-coset-expressions)
simplify
)))
```

```
(def-theorem factor-groups-are-groups
"forall(a:sets[gg],
subgroup(a) and normal(a)
implies
group{right%cosets(a), set%mul, a, right%coset%app(inv,a)})"
(theory groups)
(usages transportable-macete)
(proof; 44 nodes
(
direct-and-antecedent-inference-strategy
insistent-direct-inference
(apply-macete-with-minor-premises right%cosets-membership)
direct-and-antecedent-inference-strategy
(instantiate-existential ("g_\$0 mul g"))
(force-substitution
"x set%mul y" "right%trans(a,g_\$0) set%mul right%trans(a,g)" (0))
(apply-macete-with-minor-premises right-coset-multiplication)
(apply-macete-with-minor-premises right%cosets-membership)
(instantiate-existential ("e"))
simplify
(apply-macete-with-minor-premises right%cosets-membership)
direct-and-antecedent-inference-strategy
(instantiate-existential ("inv(g)"))
(force-substitution "x" "right%trans(a,g)" (0))
(apply-macete-with-minor-premises right-coset-inversion)
(antecedent-inference "with(p:prop, forsome(g:gg,p))")
(apply-macete-with-minor-premises right-coset-left-identity)
(apply-macete-with-minor-premises right-coset-right-identity)
(apply-macete-with-minor-premises right-coset-left-inverse)
(apply-macete-with-minor-premises right-coset-right-inverse)
(apply-macete-with-minor-premises set%mul-associativity)
direct-and-antecedent-inference-strategy
)))
```