(def-constant subgroup"lambda(a:sets[gg], nonempty_indic_q{a} and forall(g,h:gg, ((g in a) and (h in a)) implies ((g mul h) in a)) and forall(g:gg, (g in a) implies (inv(g) in a)))"(theory groups))

(def-constant gg%subgroup"sort_to_indic(gg)"(theory groups))

(def-constant e%subgroup"singleton{e}"(theory groups))

(def-theorem gg-is-a-subgroup"subgroup(gg%subgroup)"(theory groups) (usages transportable-macete) (proof ( unfold-defined-constants simplify (instantiate-existential ("e")) simplify )))

(def-theorem singleton-e-is-a-subgroup"subgroup(e%subgroup)"(theory groups) (usages transportable-macete) (proof ( unfold-defined-constants simplify-insistently direct-and-antecedent-inference-strategy simplify simplify )))

(def-theorem subgroups-are-subsets-of-gg%subgroup"forall(a:sets[gg], subgroup(a) implies a subseteq gg%subgroup)"(theory groups) (usages transportable-macete) (proof ( unfold-defined-constants direct-and-antecedent-inference-strategy insistent-direct-inference simplify )))

(def-theorem subgroups-are-nonempty"forall(a:sets[gg], subgroup(a) implies nonempty_indic_q{a})"(theory groups) (usages transportable-macete) (proof ( (unfold-single-defined-constant-globally subgroup) simplify )))

(def-theorem subgroups-closed-under-mul"forall(a:sets[gg], subgroup(a) implies forall(g,h:gg, (g in a) and (h in a) implies (g mul h) in a))"(theory groups) (usages transportable-macete) (proof ( (unfold-single-defined-constant-globally subgroup) direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop, forall(g,h:gg,p))"("g""h")) )))

(def-theorem subgroups-closed-under-inv"forall(a:sets[gg], subgroup(a) implies forall(g,h:gg, (g in a) implies inv(g) in a))"(theory groups) (usages transportable-macete) (proof ( (unfold-single-defined-constant-globally subgroup) direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop, forall(g:gg,p))"("g")) )))

(def-theorem subgroups-contain-e"forall(a:sets[gg], subgroup(a) implies (e in a))"(theory groups) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem subgroups-are-nonempty ("a")) (force-substitution"e""x mul inv(x)"(0)) (apply-macete-with-minor-premises subgroups-closed-under-mul) simplify (apply-macete-with-minor-premises subgroups-closed-under-inv) simplify simplify simplify )))

(def-compound-macete subgroup-membership (series (repeat subgroups-closed-under-mul subgroups-closed-under-inv subgroups-contain-e) simplify))

(def-theorem subgroups-are-groups"forall(a:sets[gg], subgroup(a) implies group{a,mul,e,inv})"(theory groups) (usages transportable-macete) (proof ( insistent-direct-inference-strategy (apply-macete-with-minor-premises subgroup-membership) (apply-macete-with-minor-premises subgroup-membership) (apply-macete-with-minor-premises subgroup-membership) simplify simplify simplify simplify simplify )))

(def-theorem groups->subgroup-obl-1"forall(a:sets[gg], nonempty_indic_q{a} and forall(g,h:gg,g in a and h in a implies (g mul h) in a) and forall(g:gg,g in a implies inv(g) in a) implies e in a)"lemma (theory groups) (proof ( direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(a:sets[gg], forall(g,h:gg,g in a and h in a implies (g mul h) in a));"("x""inv(x)")) (instantiate-universal-antecedent"with(a:sets[gg],forall(g:gg,g in a implies inv(g) in a));"("x")) (incorporate-antecedent"with(x:gg,a:sets[gg],(x mul inv(x)) in a);") simplify )))

(def-theorem groups->subgroup-obl-2"forall(a:sets[gg], nonempty_indic_q{a} and forall(g,h:gg,g in a and h in a implies (g mul h) in a) and forall(g:gg,g in a implies inv(g) in a) implies forall(x:gg,x in a implies if(e in a, x, ?gg)=x))"lemma (theory groups) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem groups->subgroup-obl-1 ("a")) (contrapose"with(a:sets[gg],empty_indic_q{a});") auto-instantiate-existential simplify )))

(def-translation groups->subgroup (source groups) (target groups) (assumptions"with(a:sets[gg], nonempty_indic_q{a})""with(a:sets[gg], forall(g,h:gg, (g in a) and (h in a) implies (g mul h) in a))""with(a:sets[gg], forall(g:gg, (g in a) implies (inv(g) in a)))") (fixed-theories h-o-real-arithmetic) (sort-pairs (gg (indic"with(a:sets[gg], a)"))) (constant-pairs (mul"with(a:sets[gg], lambda(x,y:gg, if((x in a) and (y in a), x mul y, ?gg)))") (inv"with(a:sets[gg], lambda(x:gg, if(x in a, inv(x), ?gg)))")) force-under-quick-load (theory-interpretation-check using-simplification))