awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coprod.Basic
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) (β := 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
⊢ 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:
simp only [toList_of_mul, map_cons, reverse_cons, ofList_append, map_mul, ofList_singleton]

Premises used: FreeMonoid.ofList_append, List.map_cons, FreeMonoid.toList_of_mul, map_mul, List.reverse_cons, FreeMonoid.ofList_singleton
-- Module: Mathlib.GroupTheory.Coprod.Basic
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
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
⊢ 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:
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]

Premises used: FreeMonoid.ofList_append, List.map_cons, mul_assoc, FreeMonoid.toList_of_mul, map_mul, List.reverse_cons, FreeMonoid.ofList_singleton, Monoid.Coprod.mk, FreeMonoid.of, DFunLike.coe, Monoid.Coprod.mk_of_inv_mul, one_mul
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
w : FreeMonoid (G ⊕ H)
⊢ Eq (α := G ∗ H) (((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) w)⁻¹ : 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)) w)))) :
      G ∗ H)

Tactic:
rfl

Premises used: Quot.map, Quotient.map', Con.toQuotient, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
⊢ Eq (α := Subgroup (G ∗ H))
    (Subgroup.closure (Set.range (ι := G) (⇑inl : (a : G) → G ∗ H) ∪ Set.range (ι := H) (⇑inr : (a : H) → G ∗ H))) ⊤

Tactic:
Subgroup.closure_eq_top_of_mclosure_eq_top mclosure_range_inl_union_inr

Premises used: Subgroup.closure_eq_top_of_mclosure_eq_top, Monoid.Coprod.mclosure_range_inl_union_inr
-- Module: Mathlib.GroupTheory.Coprod.Basic
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)))
rw₅ rw₆ :
  Eq (α := Subgroup (G ∗ H)) (MonoidHom.range inl ⊔ MonoidHom.range inr) (MonoidHom.range inl ⊔ MonoidHom.range inr)
⊢ Eq (α := Subgroup (G ∗ H)) (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]

Premises used: Subgroup.closure_eq, Monoid.Coprod.closure_range_inl_union_inr, MonoidHom.coe_range, Subgroup.closure_union
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
⊢ Codisjoint (α := Subgroup (G ∗ H)) (MonoidHom.range inl) (MonoidHom.range inr)

Tactic:
codisjoint_iff.2 range_inl_sup_range_inr

Premises used: Iff.mpr, Monoid.Coprod.range_inl_sup_range_inr, codisjoint_iff
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
⊢ Eq (α := Subgroup (H ∗ G)) (MonoidHom.range (swap G H)) ⊤

Tactic:
MonoidHom.range_eq_top.2 swap_surjective

Premises used: Iff.mpr, Monoid.Coprod.swap_surjective, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.Coprod.Basic
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
rw₄ rw₅ : (f.comp inl).range ⊔ (f.comp inr).range = (f.comp inl).range ⊔ (f.comp inr).range
⊢ f.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]

Premises used: Monoid.Coprod.range_inl_sup_range_inr, Subgroup.map_sup, MonoidHom.map_range, MonoidHom.range_eq_map
-- Module: Mathlib.GroupTheory.Coprod.Basic
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 →* K
g : H →* K
⊢ (lift f g).range = f.range ⊔ g.range

Tactic:
simp [range_eq]

Premises used: Monoid.Coprod.range_eq
-- Module: Mathlib.GroupTheory.Coprod.Basic
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'
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')
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')))
              inr :
            (a : M') → M ∗ M')
          x :
        M ∗ M')
      ((MonoidHom.comp (MonoidHom.id (M ∗ M')) inr : (a : M') → M ∗ M') x : M ∗ M')
⊢ 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'))

Tactic:
ext
-- Module: Mathlib.GroupTheory.Coprod.Basic
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'
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:
simp
-- Module: Mathlib.GroupTheory.Coprod.Basic
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'
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')))
            inr :
          (a : M') → M ∗ M')
        x :
      M ∗ M')
    ((MonoidHom.comp (MonoidHom.id (M ∗ M')) inr : (a : M') → M ∗ M') x : M ∗ M')

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coprod.Basic
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'
h₁ :
  ∀ (x : N),
    Eq (α := N ∗ N')
      ((MonoidHom.comp (N := N ∗ N')
              (MonoidHom.comp (N := M ∗ M') (Coprod.map (↑e : M →* N) (↑e' : M' →* N'))
                (Coprod.map (↑e.symm : N →* M) (↑e'.symm : N' →* M')))
              inl :
            (a : N) → N ∗ N')
          x :
        N ∗ N')
      ((MonoidHom.comp (MonoidHom.id (N ∗ N')) inl : (a : N) → N ∗ N') x : N ∗ N')
h₂ :
  ∀ (x : N'),
    Eq (α := N ∗ N')
      ((MonoidHom.comp (N := N ∗ N')
              (MonoidHom.comp (N := M ∗ M') (Coprod.map (↑e : M →* N) (↑e' : M' →* N'))
                (Coprod.map (↑e.symm : N →* M) (↑e'.symm : N' →* M')))
              inr :
            (a : N') → N ∗ N')
          x :
        N ∗ N')
      ((MonoidHom.comp (MonoidHom.id (N ∗ N')) inr : (a : N') → N ∗ N') x : N ∗ N')
⊢ Eq (α := N ∗ N' →* N ∗ N')
    (MonoidHom.comp (N := M ∗ M') (Coprod.map (↑e : M →* N) (↑e' : M' →* N'))
      (Coprod.map (↑e.symm : N →* M) (↑e'.symm : N' →* M')))
    (MonoidHom.id (N ∗ N'))

Tactic:
ext
-- Module: Mathlib.GroupTheory.Coprod.Basic
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'
x : N
⊢ Eq (α := N ∗ N')
    ((MonoidHom.comp (N := N ∗ N')
            (MonoidHom.comp (N := M ∗ M') (Coprod.map (↑e : M →* N) (↑e' : M' →* N'))
              (Coprod.map (↑e.symm : N →* M) (↑e'.symm : N' →* M')))
            inl :
          (a : N) → N ∗ N')
        x :
      N ∗ N')
    ((MonoidHom.comp (MonoidHom.id (N ∗ N')) inl : (a : N) → N ∗ N') x : N ∗ N')

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coprod.Basic
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'
x : N'
⊢ Eq (α := N ∗ N')
    ((MonoidHom.comp (N := N ∗ N')
            (MonoidHom.comp (N := M ∗ M') (Coprod.map (↑e : M →* N) (↑e' : M' →* N'))
              (Coprod.map (↑e.symm : N →* M) (↑e'.symm : N' →* M')))
            inr :
          (a : N') → N ∗ N')
        x :
      N ∗ N')
    ((MonoidHom.comp (MonoidHom.id (N ∗ N')) inr : (a : N') → N ∗ N') x : N ∗ N')

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
h₁ :
  ∀ (x : M),
    Eq (α := (M ∗ N) ∗ P)
      ((MonoidHom.comp (N := M ∗ N)
              (MonoidHom.comp (N := (M ∗ N) ∗ P)
                (MonoidHom.comp (N := M ∗ (N ∗ P))
                  (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P)))
                  (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr)))
                inl)
              inl :
            (a : M) → (M ∗ N) ∗ P)
          x :
        (M ∗ N) ∗ P)
      ((MonoidHom.comp (MonoidHom.comp (MonoidHom.id ((M ∗ N) ∗ P)) inl) inl : (a : M) → (M ∗ N) ∗ P) x : (M ∗ N) ∗ P)
h₂ :
  ∀ (x : N),
    Eq (α := (M ∗ N) ∗ P)
      ((MonoidHom.comp (N := M ∗ N)
              (MonoidHom.comp (N := (M ∗ N) ∗ P)
                (MonoidHom.comp (N := M ∗ (N ∗ P))
                  (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P)))
                  (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr)))
                inl)
              inr :
            (a : N) → (M ∗ N) ∗ P)
          x :
        (M ∗ N) ∗ P)
      ((MonoidHom.comp (MonoidHom.comp (MonoidHom.id ((M ∗ N) ∗ P)) inl) inr : (a : N) → (M ∗ N) ∗ P) x : (M ∗ N) ∗ P)
h₃ :
  ∀ (x : P),
    Eq (α := (M ∗ N) ∗ P)
      ((MonoidHom.comp (N := (M ∗ N) ∗ P)
              (MonoidHom.comp (N := M ∗ (N ∗ P))
                (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P)))
                (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr)))
              inr :
            (a : P) → (M ∗ N) ∗ P)
          x :
        (M ∗ N) ∗ P)
      ((MonoidHom.comp (MonoidHom.id ((M ∗ N) ∗ P)) inr : (a : P) → (M ∗ N) ∗ P) x : (M ∗ N) ∗ P)
⊢ Eq (α := (M ∗ N) ∗ P →* (M ∗ N) ∗ P)
    (MonoidHom.comp (N := M ∗ (N ∗ P)) (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P)))
      (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr)))
    (MonoidHom.id ((M ∗ N) ∗ P))

Tactic:
ext
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
x : M
⊢ Eq (α := (M ∗ N) ∗ P)
    ((MonoidHom.comp (N := M ∗ N)
            (MonoidHom.comp (N := (M ∗ N) ∗ P)
              (MonoidHom.comp (N := M ∗ (N ∗ P))
                (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P)))
                (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr)))
              inl)
            inl :
          (a : M) → (M ∗ N) ∗ P)
        x :
      (M ∗ N) ∗ P)
    ((MonoidHom.comp (MonoidHom.comp (MonoidHom.id ((M ∗ N) ∗ P)) inl) inl : (a : M) → (M ∗ N) ∗ P) x : (M ∗ N) ∗ P)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
x : N
⊢ Eq (α := (M ∗ N) ∗ P)
    ((MonoidHom.comp (N := M ∗ N)
            (MonoidHom.comp (N := (M ∗ N) ∗ P)
              (MonoidHom.comp (N := M ∗ (N ∗ P))
                (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P)))
                (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr)))
              inl)
            inr :
          (a : N) → (M ∗ N) ∗ P)
        x :
      (M ∗ N) ∗ P)
    ((MonoidHom.comp (MonoidHom.comp (MonoidHom.id ((M ∗ N) ∗ P)) inl) inr : (a : N) → (M ∗ N) ∗ P) x : (M ∗ N) ∗ P)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
x : P
⊢ Eq (α := (M ∗ N) ∗ P)
    ((MonoidHom.comp (N := (M ∗ N) ∗ P)
            (MonoidHom.comp (N := M ∗ (N ∗ P)) (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P)))
              (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr)))
            inr :
          (a : P) → (M ∗ N) ∗ P)
        x :
      (M ∗ N) ∗ P)
    ((MonoidHom.comp (MonoidHom.id ((M ∗ N) ∗ P)) inr : (a : P) → (M ∗ N) ∗ P) x : (M ∗ N) ∗ P)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
h₁ :
  ∀ (x : M),
    Eq (α := M ∗ (N ∗ P))
      ((MonoidHom.comp (N := M ∗ (N ∗ P))
              (MonoidHom.comp (N := (M ∗ N) ∗ P)
                (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr))
                (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P))))
              inl :
            (a : M) → M ∗ (N ∗ P))
          x :
        M ∗ (N ∗ P))
      ((MonoidHom.comp (MonoidHom.id (M ∗ (N ∗ P))) inl : (a : M) → M ∗ (N ∗ P)) x : M ∗ (N ∗ P))
h₂ :
  ∀ (x : N),
    Eq (α := M ∗ (N ∗ P))
      ((MonoidHom.comp (N := N ∗ P)
              (MonoidHom.comp (N := M ∗ (N ∗ P))
                (MonoidHom.comp (N := (M ∗ N) ∗ P)
                  (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr))
                  (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P))))
                inr)
              inl :
            (a : N) → M ∗ (N ∗ P))
          x :
        M ∗ (N ∗ P))
      ((MonoidHom.comp (MonoidHom.comp (MonoidHom.id (M ∗ (N ∗ P))) inr) inl : (a : N) → M ∗ (N ∗ P)) x : M ∗ (N ∗ P))
h₃ :
  ∀ (x : P),
    Eq (α := M ∗ (N ∗ P))
      ((MonoidHom.comp (N := N ∗ P)
              (MonoidHom.comp (N := M ∗ (N ∗ P))
                (MonoidHom.comp (N := (M ∗ N) ∗ P)
                  (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr))
                  (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P))))
                inr)
              inr :
            (a : P) → M ∗ (N ∗ P))
          x :
        M ∗ (N ∗ P))
      ((MonoidHom.comp (MonoidHom.comp (MonoidHom.id (M ∗ (N ∗ P))) inr) inr : (a : P) → M ∗ (N ∗ P)) x : M ∗ (N ∗ P))
⊢ Eq (α := M ∗ (N ∗ P) →* M ∗ (N ∗ P))
    (MonoidHom.comp (N := (M ∗ N) ∗ P) (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr))
      (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P))))
    (MonoidHom.id (M ∗ (N ∗ P)))

Tactic:
ext
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
x : M
⊢ Eq (α := M ∗ (N ∗ P))
    ((MonoidHom.comp (N := M ∗ (N ∗ P))
            (MonoidHom.comp (N := (M ∗ N) ∗ P) (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr))
              (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P))))
            inl :
          (a : M) → M ∗ (N ∗ P))
        x :
      M ∗ (N ∗ P))
    ((MonoidHom.comp (MonoidHom.id (M ∗ (N ∗ P))) inl : (a : M) → M ∗ (N ∗ P)) x : M ∗ (N ∗ P))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
x : N
⊢ Eq (α := M ∗ (N ∗ P))
    ((MonoidHom.comp (N := N ∗ P)
            (MonoidHom.comp (N := M ∗ (N ∗ P))
              (MonoidHom.comp (N := (M ∗ N) ∗ P)
                (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr))
                (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P))))
              inr)
            inl :
          (a : N) → M ∗ (N ∗ P))
        x :
      M ∗ (N ∗ P))
    ((MonoidHom.comp (MonoidHom.comp (MonoidHom.id (M ∗ (N ∗ P))) inr) inl : (a : N) → M ∗ (N ∗ P)) x : M ∗ (N ∗ P))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
x : P
⊢ Eq (α := M ∗ (N ∗ P))
    ((MonoidHom.comp (N := N ∗ P)
            (MonoidHom.comp (N := M ∗ (N ∗ P))
              (MonoidHom.comp (N := (M ∗ N) ∗ P)
                (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (MonoidHom.comp inr inr))
                (Coprod.lift (MonoidHom.comp inl inl) (Coprod.map inr (MonoidHom.id P))))
              inr)
            inr :
          (a : P) → M ∗ (N ∗ P))
        x :
      M ∗ (N ∗ P))
    ((MonoidHom.comp (MonoidHom.comp (MonoidHom.id (M ∗ (N ∗ P))) inr) inr : (a : P) → M ∗ (N ∗ P)) x : M ∗ (N ∗ P))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
x : M
⊢ Eq (α := M ∗ (N ∗ P))
    ((coprodAssoc M N P : (a : (M ∗ N) ∗ P) → M ∗ (N ∗ P))
        ((inl : (a : M ∗ N) → (M ∗ N) ∗ P) ((inl : (a : M) → M ∗ N) x)) :
      M ∗ (N ∗ P))
    ((inl : (a : M) → M ∗ (N ∗ P)) x : M ∗ (N ∗ P))

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Sum.map, Quotient.liftOn', List.map, List.foldl, Con.liftOn, FreeMonoid.of, Con.toQuotient, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
x : N
⊢ Eq (α := M ∗ (N ∗ P))
    ((coprodAssoc M N P : (a : (M ∗ N) ∗ P) → M ∗ (N ∗ P))
        ((inl : (a : M ∗ N) → (M ∗ N) ∗ P) ((inr : (a : N) → M ∗ N) x)) :
      M ∗ (N ∗ P))
    ((inr : (a : N ∗ P) → M ∗ (N ∗ P)) ((inl : (a : N) → N ∗ P) x) : M ∗ (N ∗ P))

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Sum.map, Quotient.liftOn', Set.Mem, List.map, setOf, List.foldl, Con.liftOn, FreeMonoid.of, Con.toQuotient, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
x : P
⊢ Eq (α := M ∗ (N ∗ P))
    ((coprodAssoc M N P : (a : (M ∗ N) ∗ P) → M ∗ (N ∗ P)) ((inr : (a : P) → (M ∗ N) ∗ P) x) : M ∗ (N ∗ P))
    ((inr : (a : N ∗ P) → M ∗ (N ∗ P)) ((inr : (a : P) → N ∗ P) x) : M ∗ (N ∗ P))

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', Set.Mem, setOf, List.foldl, Con.liftOn, Con.toQuotient, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
x : M
⊢ Eq (α := (M ∗ N) ∗ P)
    ((symm (coprodAssoc M N P) : (a : M ∗ (N ∗ P)) → (M ∗ N) ∗ P) ((inl : (a : M) → M ∗ (N ∗ P)) x) : (M ∗ N) ∗ P)
    ((inl : (a : M ∗ N) → (M ∗ N) ∗ P) ((inl : (a : M) → M ∗ N) x) : (M ∗ N) ∗ P)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Quotient.liftOn', Set.Mem, setOf, List.foldl, Con.liftOn, Con.toQuotient, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid P
x : N
⊢ Eq (α := (M ∗ N) ∗ P)
    ((symm (coprodAssoc M N P) : (a : M ∗ (N ∗ P)) → (M ∗ N) ∗ P)
        ((inr : (a : N ∗ P) → M ∗ (N ∗ P)) ((inl : (a : N) → N ∗ P) x)) :
      (M ∗ N) ∗ P)
    ((inl : (a : M ∗ N) → (M ∗ N) ∗ P) ((inr : (a : N) → M ∗ N) x) : (M ∗ N) ∗ P)

Tactic:
rfl

Premises used: FreeMonoid.prodAux, Sum.map, Quotient.liftOn', Set.Mem, List.map, setOf, List.foldl, Con.liftOn, FreeMonoid.of, Con.toQuotient, rfl, Sum.elim