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