awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M × N
rw :
  HMul.hMul (α := M × N) (β := M × N) ((toProd : (a : M ∗ N) → M × N) ((inl : (a : M) → M ∗ N) x.1) : M × N)
      ((toProd : (a : M ∗ N) → M × N) ((inr : (a : N) → M ∗ N) x.2) : M × N) =
    x
rw₁ :
  HMul.hMul (α := M × N) (β := M × N) (x.1, 1) ((toProd : (a : M ∗ N) → M × N) ((inr : (a : N) → M ∗ N) x.2) : M × N) =
    x
⊢ (toProd : (a : M ∗ N) → M × N)
      (HMul.hMul (α := M ∗ N) (β := M ∗ N) ((inl : (a : M) → M ∗ N) x.1 : M ∗ N)
        ((inr : (a : N) → M ∗ N) x.2 : M ∗ N)) =
    x
have rw₂ : (x.1, 1) * (1, x.2) = x
Tactic: rw [map_mul, toProd_apply_inl, toProd_apply_inr, Prod.fst_mul_snd]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : Monoid M
inst_1 : Monoid N
x : M × N
rw :
  HMul.hMul (α := M × N) (β := M × N) ((toProd : (a : M ∗ N) → M × N) ((inl : (a : M) → M ∗ N) x.1) : M × N)
      ((toProd : (a : M ∗ N) → M × N) ((inr : (a : N) → M ∗ N) x.2) : M × N) =
    x
rw₁ :
  HMul.hMul (α := M × N) (β := M × N) (x.1, 1) ((toProd : (a : M ∗ N) → M × N) ((inr : (a : N) → M ∗ N) x.2) : M × N) =
    x
rw₂ : (x.1, 1) * (1, x.2) = x
⊢ (toProd : (a : M ∗ N) → M × N)
      (HMul.hMul (α := M ∗ N) (β := M ∗ N) ((inl : (a : M) → M ∗ N) x.1 : M ∗ N)
        ((inr : (a : N) → M ∗ N) x.2 : M ∗ N)) =
    x
have rw₃ : x = x
Tactic: rw [map_mul, toProd_apply_inl, toProd_apply_inr, Prod.fst_mul_snd]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
x : FreeMonoid (G ⊕ H)
⊢ (coprodCon G H : (a : FreeMonoid (G ⊕ H)) → FreeMonoid (G ⊕ H) → Prop)
    (HMul.hMul (α := FreeMonoid (G ⊕ H))
      ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
          (List.reverse (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) x))) :
        FreeMonoid (G ⊕ H))
      x)
    1
have rw : HMul.hMul (α := G ∗ H) (β := G ∗ H)
    ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
        ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
          (List.reverse (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) x)))) :
      G ∗ H)
    ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) x : G ∗ H) =
  1
Tactic: rw [← mk_eq_mk, map_mul, map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx :
  HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H) =
    1
⊢ HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) (of x * xs))))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x * xs) : G ∗ H) =
    1
have mul_of : HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of (Sum.map Inv.inv Inv.inv x)) : G ∗ H) *
    HMul.hMul (α := G ∗ H) (β := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x) : G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H) =
  1
Tactic: simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ofList_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx :
  HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H) =
    1
⊢ HMul.hMul (α := G ∗ H) (β := G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
            ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
              (List.reverse
                (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
          G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of (Sum.map Inv.inv Inv.inv x)) : G ∗ H) *
      HMul.hMul (α := G ∗ H) (β := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x) : G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H) =
    1
have mul_of : HMul.hMul (α := G ∗ H)
    ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
        ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
          (List.reverse (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
      G ∗ H)
    (HMul.hMul (α := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of (Sum.map Inv.inv Inv.inv x)) : G ∗ H)
      (HMul.hMul (α := G ∗ H) (β := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x) : G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H))) =
  1
Tactic: rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx :
  HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H) =
    1
mul_of :
  HMul.hMul (α := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      (HMul.hMul (α := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of (Sum.map Inv.inv Inv.inv x)) : G ∗ H)
        (HMul.hMul (α := G ∗ H) (β := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x) : G ∗ H)
          ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H))) =
    1
⊢ HMul.hMul (α := G ∗ H) (β := G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
            ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
              (List.reverse
                (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
          G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of (Sum.map Inv.inv Inv.inv x)) : G ∗ H) *
      HMul.hMul (α := G ∗ H) (β := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x) : G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H) =
    1
have mul_of₁ : HMul.hMul (α := G ∗ H)
    ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
        ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
          (List.reverse (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
      G ∗ H)
    (HMul.hMul (β := G ∗ H)
      (HMul.hMul (α := G ∗ H) (β := G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of (Sum.map Inv.inv Inv.inv x)) : G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x) : G ∗ H))
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H)) =
  1
Tactic: rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx :
  HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H) =
    1
mul_of :
  HMul.hMul (α := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      (HMul.hMul (α := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of (Sum.map Inv.inv Inv.inv x)) : G ∗ H)
        (HMul.hMul (α := G ∗ H) (β := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x) : G ∗ H)
          ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H))) =
    1
mul_of₁ :
  HMul.hMul (α := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      (HMul.hMul (β := G ∗ H)
        (HMul.hMul (α := G ∗ H) (β := G ∗ H)
          ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of (Sum.map Inv.inv Inv.inv x)) : G ∗ H)
          ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x) : G ∗ H))
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H)) =
    1
⊢ HMul.hMul (α := G ∗ H) (β := G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
            ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
              (List.reverse
                (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
          G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of (Sum.map Inv.inv Inv.inv x)) : G ∗ H) *
      HMul.hMul (α := G ∗ H) (β := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x) : G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H) =
    1
have mul_of₂ : HMul.hMul (α := G ∗ H)
    ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
        ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
          (List.reverse (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
      G ∗ H)
    (HMul.hMul (α := G ∗ H) (β := G ∗ H) (1 : G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H)) =
  1
Tactic: rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
x : FreeMonoid (G ⊕ H)
⊢ HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) x)))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) x : G ∗ H) =
    1
have one : HMul.hMul (α := G ∗ H) (β := G ∗ H)
    ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
        ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
          (List.reverse (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) 1)))) :
      G ∗ H)
    ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) 1 : G ∗ H) =
  1
Tactic: induction x using FreeMonoid.inductionOn' with
  | one => simp
  | mul_of x xs ihx =>
    simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ofList_singleton]
    rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
x : FreeMonoid (G ⊕ H)
one :
  HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) 1)))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) 1 : G ∗ H) =
    1
⊢ HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) x)))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) x : G ∗ H) =
    1
have mul_of : ∀ (x : G ⊕ H) (xs : FreeMonoid (G ⊕ H))
  (ihx :
    HMul.hMul (α := G ∗ H) (β := G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
            ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
              (List.reverse
                (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
          G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H) =
      1),
  HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) (of x * xs))))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x * xs) : G ∗ H) =
    1
Tactic: induction x using FreeMonoid.inductionOn' with
  | one => simp
  | mul_of x xs ihx =>
    simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ofList_singleton]
    rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
⊢ Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr) ⊤
have rw : Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
  (Subgroup.closure (Set.range (ι := G) (⇑inl : (a : G) → G ∗ H) ∪ Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
Tactic: rw [← closure_range_inl_union_inr, Subgroup.closure_union, ← MonoidHom.coe_range,
    ← MonoidHom.coe_range, Subgroup.closure_eq, Subgroup.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
rw :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (Set.range (ι := G) (⇑inl : (a : G) → G ∗ H) ∪ Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
⊢ Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr) ⊤
have rw₁ : Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
  (Subgroup.closure (Set.range (ι := G) (⇑inl : (a : G) → G ∗ H)) ⊔
    Subgroup.closure (Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
Tactic: rw [← closure_range_inl_union_inr, Subgroup.closure_union, ← MonoidHom.coe_range,
    ← MonoidHom.coe_range, Subgroup.closure_eq, Subgroup.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
rw :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (Set.range (ι := G) (⇑inl : (a : G) → G ∗ H) ∪ Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
rw₁ :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (Set.range (ι := G) (⇑inl : (a : G) → G ∗ H)) ⊔
      Subgroup.closure (Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
⊢ Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr) ⊤
have rw₂ : Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
  (Subgroup.closure (↑(MonoidHom.range inl) : Set (G ∗ H)) ⊔
    Subgroup.closure (Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
Tactic: rw [← closure_range_inl_union_inr, Subgroup.closure_union, ← MonoidHom.coe_range,
    ← MonoidHom.coe_range, Subgroup.closure_eq, Subgroup.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
rw :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (Set.range (ι := G) (⇑inl : (a : G) → G ∗ H) ∪ Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
rw₁ :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (Set.range (ι := G) (⇑inl : (a : G) → G ∗ H)) ⊔
      Subgroup.closure (Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
rw₂ :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (↑(MonoidHom.range inl) : Set (G ∗ H)) ⊔
      Subgroup.closure (Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
⊢ Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr) ⊤
have rw₃ : Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
  (Subgroup.closure (↑(MonoidHom.range inl) : Set (G ∗ H)) ⊔ Subgroup.closure (↑(MonoidHom.range inr) : Set (G ∗ H)))
Tactic: rw [← closure_range_inl_union_inr, Subgroup.closure_union, ← MonoidHom.coe_range,
    ← MonoidHom.coe_range, Subgroup.closure_eq, Subgroup.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
rw :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (Set.range (ι := G) (⇑inl : (a : G) → G ∗ H) ∪ Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
rw₁ :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (Set.range (ι := G) (⇑inl : (a : G) → G ∗ H)) ⊔
      Subgroup.closure (Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
rw₂ :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (↑(MonoidHom.range inl) : Set (G ∗ H)) ⊔
      Subgroup.closure (Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
rw₃ :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (↑(MonoidHom.range inl) : Set (G ∗ H)) ⊔ Subgroup.closure (↑(MonoidHom.range inr) : Set (G ∗ H)))
⊢ Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr) ⊤
have rw₄ : Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
  (MonoidHom.range inl ⊔ Subgroup.closure (↑(MonoidHom.range inr) : Set (G ∗ H)))
Tactic: rw [← closure_range_inl_union_inr, Subgroup.closure_union, ← MonoidHom.coe_range,
    ← MonoidHom.coe_range, Subgroup.closure_eq, Subgroup.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
rw :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (Set.range (ι := G) (⇑inl : (a : G) → G ∗ H) ∪ Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
rw₁ :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (Set.range (ι := G) (⇑inl : (a : G) → G ∗ H)) ⊔
      Subgroup.closure (Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
rw₂ :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (↑(MonoidHom.range inl) : Set (G ∗ H)) ⊔
      Subgroup.closure (Set.range (ι := H) (⇑inr : (a : H) → G ∗ H)))
rw₃ :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (Subgroup.closure (↑(MonoidHom.range inl) : Set (G ∗ H)) ⊔ Subgroup.closure (↑(MonoidHom.range inr) : Set (G ∗ H)))
rw₄ :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr)
    (MonoidHom.range inl ⊔ Subgroup.closure (↑(MonoidHom.range inr) : Set (G ∗ H)))
⊢ Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr) ⊤
have rw₅ : Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr) (MonoidHom.range inl ⊔ MonoidHom.range inr)
Tactic: rw [← closure_range_inl_union_inr, Subgroup.closure_union, ← MonoidHom.coe_range,
    ← MonoidHom.coe_range, Subgroup.closure_eq, Subgroup.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
K : Type u_3
inst_2 : Group K
f : G ∗ H →* K
⊢ f.range = (f.comp inl).range ⊔ (f.comp inr).range
have rw : Subgroup.map f ⊤ = (f.comp inl).range ⊔ (f.comp inr).range
Tactic: rw [MonoidHom.range_eq_map, ← range_inl_sup_range_inr, Subgroup.map_sup, MonoidHom.map_range,
    MonoidHom.map_range]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
K : Type u_3
inst_2 : Group K
f : G ∗ H →* K
rw : Subgroup.map f ⊤ = (f.comp inl).range ⊔ (f.comp inr).range
⊢ f.range = (f.comp inl).range ⊔ (f.comp inr).range
have rw₁ : Subgroup.map f (MonoidHom.range inl ⊔ MonoidHom.range inr) = (f.comp inl).range ⊔ (f.comp inr).range
Tactic: rw [MonoidHom.range_eq_map, ← range_inl_sup_range_inr, Subgroup.map_sup, MonoidHom.map_range,
    MonoidHom.map_range]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
K : Type u_3
inst_2 : Group K
f : G ∗ H →* K
rw : Subgroup.map f ⊤ = (f.comp inl).range ⊔ (f.comp inr).range
rw₁ : Subgroup.map f (MonoidHom.range inl ⊔ MonoidHom.range inr) = (f.comp inl).range ⊔ (f.comp inr).range
⊢ f.range = (f.comp inl).range ⊔ (f.comp inr).range
have rw₂ : Subgroup.map f (MonoidHom.range inl) ⊔ Subgroup.map f (MonoidHom.range inr) = (f.comp inl).range ⊔ (f.comp inr).range
Tactic: rw [MonoidHom.range_eq_map, ← range_inl_sup_range_inr, Subgroup.map_sup, MonoidHom.map_range,
    MonoidHom.map_range]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
K : Type u_3
inst_2 : Group K
f : G ∗ H →* K
rw : Subgroup.map f ⊤ = (f.comp inl).range ⊔ (f.comp inr).range
rw₁ : Subgroup.map f (MonoidHom.range inl ⊔ MonoidHom.range inr) = (f.comp inl).range ⊔ (f.comp inr).range
rw₂ :
  Subgroup.map f (MonoidHom.range inl) ⊔ Subgroup.map f (MonoidHom.range inr) = (f.comp inl).range ⊔ (f.comp inr).range
⊢ f.range = (f.comp inl).range ⊔ (f.comp inr).range
have rw₃ : (f.comp inl).range ⊔ Subgroup.map f (MonoidHom.range inr) = (f.comp inl).range ⊔ (f.comp inr).range
Tactic: rw [MonoidHom.range_eq_map, ← range_inl_sup_range_inr, Subgroup.map_sup, MonoidHom.map_range,
    MonoidHom.map_range]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
K : Type u_3
inst_2 : Group K
f : G ∗ H →* K
rw : Subgroup.map f ⊤ = (f.comp inl).range ⊔ (f.comp inr).range
rw₁ : Subgroup.map f (MonoidHom.range inl ⊔ MonoidHom.range inr) = (f.comp inl).range ⊔ (f.comp inr).range
rw₂ :
  Subgroup.map f (MonoidHom.range inl) ⊔ Subgroup.map f (MonoidHom.range inr) = (f.comp inl).range ⊔ (f.comp inr).range
rw₃ : (f.comp inl).range ⊔ Subgroup.map f (MonoidHom.range inr) = (f.comp inl).range ⊔ (f.comp inr).range
⊢ f.range = (f.comp inl).range ⊔ (f.comp inr).range
have rw₄ : (f.comp inl).range ⊔ (f.comp inr).range = (f.comp inl).range ⊔ (f.comp inr).range
Tactic: rw [MonoidHom.range_eq_map, ← range_inl_sup_range_inr, Subgroup.map_sup, MonoidHom.map_range,
    MonoidHom.map_range]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
⊢ Eq (α := M ∗ M' →* M ∗ M')
    (MonoidHom.comp (N := N ∗ N') (Coprod.map (↑e.symm : N →* M) (↑e'.symm : N' →* M'))
      (Coprod.map (↑e : M →* N) (↑e' : M' →* N')))
    (MonoidHom.id (M ∗ M'))
have h₁ : ∀ (x : M),
  Eq (α := M ∗ M')
    ((MonoidHom.comp (N := M ∗ M')
            (MonoidHom.comp (N := N ∗ N') (Coprod.map (↑e.symm : N →* M) (↑e'.symm : N' →* M'))
              (Coprod.map (↑e : M →* N) (↑e' : M' →* N')))
            inl :
          (a : M) → M ∗ M')
        x :
      M ∗ M')
    ((MonoidHom.comp (MonoidHom.id (M ∗ M')) inl : (a : M) → M ∗ M') x : M ∗ M')
Tactic: ext