awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Surjective (α := FreeMonoid (M ⊕ N)) (β := M ∗ N) (⇑mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N)

Tactic:
Quot.mk_surjective

Premises used: Con.Quotient, Quotient, Con.toQuotient, Quot.mk_surjective, Monoid.Coprod
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := FreeMonoid (M ⊕ N) →* M ∗ N) mk) ⊤

Tactic:
Con.mrange_mk'

Premises used: Monoid.Coprod.mk, Monoid.Coprod, Con.mrange_mk'
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
w₁ w₂ : FreeMonoid (M ⊕ N)
⊢ Eq (α := M ∗ N) ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) w₁ : M ∗ N)
      ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) w₂ : M ∗ N) ↔
    (coprodCon M N : (a : FreeMonoid (M ⊕ N)) → FreeMonoid (M ⊕ N) → Prop) w₁ w₂

Tactic:
Con.eq _

Premises used: Con.eq, Con.toQuotient, Monoid.Coprod
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
x : M
⊢ Eq (α := M ∗ N) ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) (of (Sum.inl x)) : M ∗ N) ((inl : (a : M) → M ∗ N) x : M ∗ N)

Tactic:
rfl

Premises used: Con.toQuotient, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
x : N
⊢ Eq (α := M ∗ N) ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) (of (Sum.inr x)) : M ∗ N) ((inr : (a : N) → M ∗ N) x : M ∗ N)

Tactic:
rfl

Premises used: Con.toQuotient, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
C : M ∗ N → Prop
m : M ∗ N
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inl : (a : M) → M ∗ N) m : M ∗ N) x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inr : (a : N) → M ∗ N) n : M ∗ N) x)
rcases : ∀ (x : FreeMonoid (M ⊕ N)), C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) x)
⊢ C m

Tactic:
rcases mk_surjective m with ⟨x, rfl⟩

Premises used: Monoid.Coprod.mk_surjective, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inl : (a : M) → M ∗ N) m : M ∗ N) x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inr : (a : N) → M ∗ N) n : M ∗ N) x)
⊢ C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) 1)

Tactic:
one

Premises used: Con.toQuotient
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inl : (a : M) → M ∗ N) m : M ∗ N) x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inr : (a : N) → M ∗ N) n : M ∗ N) x)
⊢ C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) 1)

Tactic:
exact one
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inl : (a : M) → M ∗ N) m : M ∗ N) x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inr : (a : N) → M ∗ N) n : M ∗ N) x)
xs : FreeMonoid (M ⊕ N)
ih : C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) xs)
m : M
⊢ C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) (of (Sum.inl m) * xs))

Tactic:
simpa using inl_mul m _ ih
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inl : (a : M) → M ∗ N) m : M ∗ N) x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inr : (a : N) → M ∗ N) n : M ∗ N) x)
xs : FreeMonoid (M ⊕ N)
ih : C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) xs)
n : N
⊢ C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) (of (Sum.inr n) * xs))

Tactic:
simpa using inr_mul n _ ih
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inl : (a : M) → M ∗ N) m : M ∗ N) x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inr : (a : N) → M ∗ N) n : M ∗ N) x)
x : M ⊕ N
xs : FreeMonoid (M ⊕ N)
ih : C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) xs)
mul_of : ∀ (m : M), C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) (of (Sum.inl m) * xs))
mul_of₁ : ∀ (n : N), C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) (of (Sum.inr n) * xs))
⊢ C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) (of x * xs))

Tactic:
cases x with
    | inl m => simpa using inl_mul m _ ih
    | inr n => simpa using inr_mul n _ ih

Premises used: Monoid.Coprod.inl, Monoid.Coprod.inr
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inl : (a : M) → M ∗ N) m : M ∗ N) x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (HMul.hMul (α := M ∗ N) ((inr : (a : N) → M ∗ N) n : M ∗ N) x)
x : FreeMonoid (M ⊕ N)
one₁ : C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) 1)
mul_of :
  ∀ (x : M ⊕ N) (xs : FreeMonoid (M ⊕ N)) (ih : C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) xs)),
    C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) (of x * xs))
⊢ C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) x)

Tactic:
induction x using FreeMonoid.inductionOn' with
  | one => exact one
  | mul_of x xs ih =>
    cases x with
    | inl m => simpa using inl_mul m _ ih
    | inr n => simpa using inr_mul n _ ih

Premises used: Monoid.Coprod.inl, Monoid.Coprod.inr
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
C : M ∗ N → Prop
m : M ∗ N
inl : ∀ (m : M), C ((Coprod.inl : (a : M) → M ∗ N) m)
inr : ∀ (n : N), C ((Coprod.inr : (a : N) → M ∗ N) n)
mul : ∀ (x y : M ∗ N), C x → C y → C (x * y)
⊢ C 1

Tactic:
simpa using inl 1

Premises used: OfNat.ofNat
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
f : FreeMonoid (M ⊕ N) →* P
hM₁ : Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inl 1)) : P) (1 : P)
hN₁ : Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inr 1)) : P) (1 : P)
hM :
  ∀ (x y : M),
    Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inl (x * y))) : P)
      ((f : (a : FreeMonoid (M ⊕ N)) → P) (HMul.hMul (α := FreeMonoid (M ⊕ N)) (of (Sum.inl x)) (of (Sum.inl y))) : P)
hN :
  ∀ (x y : N),
    Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inr (x * y))) : P)
      ((f : (a : FreeMonoid (M ⊕ N)) → P) (HMul.hMul (α := FreeMonoid (M ⊕ N)) (of (Sum.inr x)) (of (Sum.inr y))) : P)
x : M
⊢ Eq.{u_5 + 1} (α := P) ((clift f hM₁ hN₁ hM hN : (a : M ∗ N) → P) ((inl : (a : M) → M ∗ N) x : M ∗ N) : P)
    ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inl x)) : P)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
f : FreeMonoid (M ⊕ N) →* P
hM₁ : Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inl 1)) : P) (1 : P)
hN₁ : Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inr 1)) : P) (1 : P)
hM :
  ∀ (x y : M),
    Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inl (x * y))) : P)
      ((f : (a : FreeMonoid (M ⊕ N)) → P) (HMul.hMul (α := FreeMonoid (M ⊕ N)) (of (Sum.inl x)) (of (Sum.inl y))) : P)
hN :
  ∀ (x y : N),
    Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inr (x * y))) : P)
      ((f : (a : FreeMonoid (M ⊕ N)) → P) (HMul.hMul (α := FreeMonoid (M ⊕ N)) (of (Sum.inr x)) (of (Sum.inr y))) : P)
x : N
⊢ Eq.{u_5 + 1} (α := P) ((clift f hM₁ hN₁ hM hN : (a : M ∗ N) → P) ((inr : (a : N) → M ∗ N) x : M ∗ N) : P)
    ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inr x)) : P)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
f : FreeMonoid (M ⊕ N) →* P
hM₁ : Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inl 1)) : P) (1 : P)
hN₁ : Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inr 1)) : P) (1 : P)
hM :
  ∀ (x y : M),
    Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inl (x * y))) : P)
      ((f : (a : FreeMonoid (M ⊕ N)) → P) (HMul.hMul (α := FreeMonoid (M ⊕ N)) (of (Sum.inl x)) (of (Sum.inl y))) : P)
hN :
  ∀ (x y : N),
    Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inr (x * y))) : P)
      ((f : (a : FreeMonoid (M ⊕ N)) → P) (HMul.hMul (α := FreeMonoid (M ⊕ N)) (of (Sum.inr x)) (of (Sum.inr y))) : P)
w : FreeMonoid (M ⊕ N)
⊢ Eq.{u_5 + 1} (α := P)
    ((clift f hM₁ hN₁ hM hN : (a : M ∗ N) → P) ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) w : M ∗ N) : P)
    ((f : (a : FreeMonoid (M ⊕ N)) → P) w : P)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
f : FreeMonoid (M ⊕ N) →* P
hM₁ : Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inl 1)) : P) (1 : P)
hN₁ : Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inr 1)) : P) (1 : P)
hM :
  ∀ (x y : M),
    Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inl (x * y))) : P)
      ((f : (a : FreeMonoid (M ⊕ N)) → P) (HMul.hMul (α := FreeMonoid (M ⊕ N)) (of (Sum.inl x)) (of (Sum.inl y))) : P)
hN :
  ∀ (x y : N),
    Eq.{u_5 + 1} (α := P) ((f : (a : FreeMonoid (M ⊕ N)) → P) (of (Sum.inr (x * y))) : P)
      ((f : (a : FreeMonoid (M ⊕ N)) → P) (HMul.hMul (α := FreeMonoid (M ⊕ N)) (of (Sum.inr x)) (of (Sum.inr y))) : P)
⊢ (clift f hM₁ hN₁ hM hN).comp mk = f

Tactic:
DFunLike.ext' rfl

Premises used: DFunLike.ext', rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
rw :
  Eq (α := Submonoid (M ∗ N))
    (Submonoid.closure (Set.range (ι := M) (⇑inl : (a : M) → M ∗ N) ∪ Set.range (ι := N) (⇑inr : (a : N) → M ∗ N)))
    (Submonoid.closure
      (Set.range (ι := M) (comp (β := M ⊕ N) ((⇑mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) ∘ of) Sum.inl) ∪
        Set.range (ι := N) (comp (β := M ⊕ N) ((⇑mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) ∘ of) Sum.inr)))
⊢ Eq (α := Submonoid (M ∗ N))
    (Submonoid.closure (Set.range (ι := M) (⇑inl : (a : M) → M ∗ N) ∪ Set.range (ι := N) (⇑inr : (a : N) → M ∗ N))) ⊤

Tactic:
rw [← mrange_mk, MonoidHom.mrange_eq_map, ← closure_range_of, MonoidHom.map_mclosure,
    ← range_comp, Sum.range_eq]

Premises used: Set.range_comp, MonoidHom.mrange_eq_map, FreeMonoid.closure_range_of, Sum.range_eq, Monoid.Coprod.mrange_mk, MonoidHom.map_mclosure
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid (M ∗ N))
    (Submonoid.closure (Set.range (ι := M) (⇑inl : (a : M) → M ∗ N) ∪ Set.range (ι := N) (⇑inr : (a : N) → M ∗ N)))
    (Submonoid.closure
      (Set.range (ι := M) (comp (β := M ⊕ N) ((⇑mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) ∘ of) Sum.inl) ∪
        Set.range (ι := N) (comp (β := M ⊕ N) ((⇑mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) ∘ of) Sum.inr)))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
rw :
  Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr)
    (Submonoid.closure (Set.range (ι := M) (⇑inl : (a : M) → M ∗ N) ∪ Set.range (ι := N) (⇑inr : (a : N) → M ∗ N)))
rw₁ :
  Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr)
    (Submonoid.closure (Set.range (ι := M) (⇑inl : (a : M) → M ∗ N)) ⊔
      Submonoid.closure (Set.range (ι := N) (⇑inr : (a : N) → M ∗ N)))
rw₂ :
  Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr)
    (Submonoid.closure (↑(MonoidHom.mrange (F := M →* M ∗ N) inl) : Set (M ∗ N)) ⊔
      Submonoid.closure (Set.range (ι := N) (⇑inr : (a : N) → M ∗ N)))
rw₃ :
  Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr)
    (Submonoid.closure (↑(MonoidHom.mrange (F := M →* M ∗ N) inl) : Set (M ∗ N)) ⊔
      Submonoid.closure (↑(MonoidHom.mrange (F := N →* M ∗ N) inr) : Set (M ∗ N)))
rw₄ :
  Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr)
    (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔
      Submonoid.closure (↑(MonoidHom.mrange (F := N →* M ∗ N) inr) : Set (M ∗ N)))
rw₅ rw₆ :
  Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr)
    (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr)
⊢ Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr) ⊤

Tactic:
rw [← mclosure_range_inl_union_inr, Submonoid.closure_union, ← MonoidHom.coe_mrange,
    ← MonoidHom.coe_mrange, Submonoid.closure_eq, Submonoid.closure_eq]

Premises used: MonoidHom.coe_mrange, Submonoid.closure_eq, Submonoid.closure_union, Monoid.Coprod.mclosure_range_inl_union_inr
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Codisjoint (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl) (MonoidHom.mrange (F := N →* M ∗ N) inr)

Tactic:
codisjoint_iff.2 mrange_inl_sup_mrange_inr

Premises used: Iff.mpr, codisjoint_iff, Monoid.Coprod.mrange_inl_sup_mrange_inr
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
f : M ∗ N →* P
rw : Eq (α := Submonoid P) (Submonoid.map f ⊤) (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))
rw₁ :
  Eq (α := Submonoid P)
    (Submonoid.map f (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr))
    (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))
rw₂ :
  Eq (α := Submonoid P)
    (Submonoid.map f (MonoidHom.mrange (F := M →* M ∗ N) inl) ⊔
      Submonoid.map f (MonoidHom.mrange (F := N →* M ∗ N) inr))
    (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))
rw₃ :
  Eq (α := Submonoid P) (MonoidHom.mrange (f.comp inl) ⊔ Submonoid.map f (MonoidHom.mrange (F := N →* M ∗ N) inr))
    (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))
rw₄ rw₅ :
  Eq (α := Submonoid P) (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))
    (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))
⊢ Eq (α := Submonoid P) (MonoidHom.mrange f) (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))

Tactic:
rw [MonoidHom.mrange_eq_map, ← mrange_inl_sup_mrange_inr, Submonoid.map_sup, MonoidHom.map_mrange,
    MonoidHom.map_mrange]

Premises used: MonoidHom.mrange_eq_map, Submonoid.map_sup, MonoidHom.map_mrange, Monoid.Coprod.mrange_inl_sup_mrange_inr
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
f g : M ∗ N →* P
h₁ : f.comp inl = g.comp inl
h₂ : f.comp inr = g.comp inr
⊢ f = g

Tactic:
MonoidHom.eq_of_eqOn_denseM mclosure_range_inl_union_inr <| eqOn_union.2
    ⟨eqOn_range.2 <| DFunLike.ext'_iff.1 h₁, eqOn_range.2 <| DFunLike.ext'_iff.1 h₂⟩

Premises used: Iff.mpr, DFunLike.ext'_iff, Set.eqOn_union, Set.eqOn_range, MonoidHom.eq_of_eqOn_denseM, And.intro, Iff.mp, Monoid.Coprod.mclosure_range_inl_union_inr
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := M ∗ N →* M ∗ N) (clift mk ⋯ ⋯ ⋯ ⋯) (MonoidHom.id (M ∗ N))

Tactic:
hom_ext rfl rfl

Premises used: Monoid.Coprod.hom_ext, rfl
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
inst_4 : MulOneClass P
f : M →* M'
g : N →* N'
⊢ Eq (α := M' ∗ N')
    ((MonoidHom.comp mk (FreeMonoid.map (Sum.map (⇑f : (a : M) → M') (⇑g : (a : N) → N'))) :
          (a : FreeMonoid (M ⊕ N)) → M' ∗ N')
        (of (Sum.inl 1)) :
      M' ∗ N')
    (1 : M' ∗ N')

Tactic:
simp only [MonoidHom.comp_apply, map_of, Sum.map_inl, map_one, mk_of_inl]

Premises used: Sum.map_inl, map_one, Monoid.Coprod.mk_of_inl, FreeMonoid.map_of, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
inst_4 : MulOneClass P
f : M →* M'
g : N →* N'
⊢ Eq (α := M' ∗ N')
    ((MonoidHom.comp mk (FreeMonoid.map (Sum.map (⇑f : (a : M) → M') (⇑g : (a : N) → N'))) :
          (a : FreeMonoid (M ⊕ N)) → M' ∗ N')
        (of (Sum.inr 1)) :
      M' ∗ N')
    (1 : M' ∗ N')

Tactic:
simp only [MonoidHom.comp_apply, map_of, Sum.map_inr, map_one, mk_of_inr]

Premises used: Monoid.Coprod.mk_of_inr, map_one, Sum.map_inr, FreeMonoid.map_of, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
inst_4 : MulOneClass P
f : M →* M'
g : N →* N'
x y : M
⊢ Eq (α := M' ∗ N')
    ((MonoidHom.comp mk (FreeMonoid.map (Sum.map (⇑f : (a : M) → M') (⇑g : (a : N) → N'))) :
          (a : FreeMonoid (M ⊕ N)) → M' ∗ N')
        (of (Sum.inl (x * y))) :
      M' ∗ N')
    ((MonoidHom.comp mk (FreeMonoid.map (Sum.map (⇑f : (a : M) → M') (⇑g : (a : N) → N'))) :
          (a : FreeMonoid (M ⊕ N)) → M' ∗ N')
        (HMul.hMul (α := FreeMonoid (M ⊕ N)) (of (Sum.inl x)) (of (Sum.inl y))) :
      M' ∗ N')

Tactic:
simp only [MonoidHom.comp_apply, map_of, Sum.map_inl, map_mul, mk_of_inl]

Premises used: Sum.map_inl, map_mul, Monoid.Coprod.mk_of_inl, FreeMonoid.map_of, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
inst_4 : MulOneClass P
f : M →* M'
g : N →* N'
x y : N
⊢ Eq (α := M' ∗ N')
    ((MonoidHom.comp mk (FreeMonoid.map (Sum.map (⇑f : (a : M) → M') (⇑g : (a : N) → N'))) :
          (a : FreeMonoid (M ⊕ N)) → M' ∗ N')
        (of (Sum.inr (x * y))) :
      M' ∗ N')
    ((MonoidHom.comp mk (FreeMonoid.map (Sum.map (⇑f : (a : M) → M') (⇑g : (a : N) → N'))) :
          (a : FreeMonoid (M ⊕ N)) → M' ∗ N')
        (HMul.hMul (α := FreeMonoid (M ⊕ N)) (of (Sum.inr x)) (of (Sum.inr y))) :
      M' ∗ N')

Tactic:
simp only [MonoidHom.comp_apply, map_of, Sum.map_inr, map_mul, mk_of_inr]

Premises used: map_mul, Monoid.Coprod.mk_of_inr, Sum.map_inr, FreeMonoid.map_of, MonoidHom.comp_apply
-- 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'
f : M →* M'
g : N →* N'
l : List (M ⊕ N)
⊢ Eq (α := M' ∗ N')
    ((map f g : (a : M ∗ N) → M' ∗ N')
        ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) ((ofList : (a : List (M ⊕ N)) → FreeMonoid (M ⊕ N)) l)) :
      M' ∗ N')
    ((mk : (a : FreeMonoid (M' ⊕ N')) → M' ∗ N')
        ((ofList : (a : List (M' ⊕ N')) → FreeMonoid (M' ⊕ N'))
          (List.map (Sum.map (⇑f : (a : M) → M') (⇑g : (a : N) → N')) l)) :
      M' ∗ N')

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, Con.toQuotient, rfl
-- 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'
f : M →* M'
g : N →* N'
x : M
⊢ Eq (α := M' ∗ N') ((map f g : (a : M ∗ N) → M' ∗ N') ((inl : (a : M) → M ∗ N) x) : M' ∗ N')
    ((inl : (a : M') → M' ∗ N') ((f : (a : M) → M') x) : M' ∗ N')

Tactic:
rfl

Premises used: Sum.map, Quotient.liftOn', List.map, Con.liftOn, FreeMonoid.of, Con.toQuotient, rfl, Sum.elim
-- 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'
f : M →* M'
g : N →* N'
x : N
⊢ Eq (α := M' ∗ N') ((map f g : (a : M ∗ N) → M' ∗ N') ((inr : (a : N) → M ∗ N) x) : M' ∗ N')
    ((inr : (a : N') → M' ∗ N') ((g : (a : N) → N') x) : M' ∗ N')

Tactic:
rfl

Premises used: Sum.map, Quotient.liftOn', List.map, Con.liftOn, FreeMonoid.of, Con.toQuotient, rfl, Sum.elim
-- 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'
f : M →* M'
g : N →* N'
⊢ (map f g).comp inl = MonoidHom.comp inl f

Tactic:
rfl

Premises used: Sum.map, Quotient.liftOn', List.map, Con.Quotient, Quotient, Con.liftOn, FreeMonoid.of, Monoid.Coprod.inl, Con.toQuotient, Monoid.Coprod.clift, Con.lift, rfl, Sum.elim
-- 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'
f : M →* M'
g : N →* N'
⊢ (map f g).comp inr = MonoidHom.comp inr g

Tactic:
rfl

Premises used: Sum.map, Quotient.liftOn', List.map, Con.Quotient, Quotient, Con.liftOn, FreeMonoid.of, Con.toQuotient, Monoid.Coprod.inr, Monoid.Coprod.clift, Con.lift, rfl, Sum.elim
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := M ∗ N →* M ∗ N) (map (MonoidHom.id M) (MonoidHom.id N)) (MonoidHom.id (M ∗ N))

Tactic:
hom_ext rfl rfl

Premises used: Monoid.Coprod.hom_ext, rfl
-- 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'
M'' : Type u_6
N'' : Type u_7
inst_4 : MulOneClass M''
inst_5 : MulOneClass N''
f' : M' →* M''
g' : N' →* N''
f : M →* M'
g : N →* N'
⊢ (map f' g').comp (map f g) = map (f'.comp f) (g'.comp g)

Tactic:
hom_ext rfl rfl

Premises used: Monoid.Coprod.hom_ext, rfl
-- 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'
M'' : Type u_6
N'' : Type u_7
inst_4 : MulOneClass M''
inst_5 : MulOneClass N''
f' : M' →* M''
g' : N' →* N''
f : M →* M'
g : N →* N'
x : M ∗ N
⊢ Eq (α := M'' ∗ N'') ((map f' g' : (a : M' ∗ N') → M'' ∗ N'') ((map f g : (a : M ∗ N) → M' ∗ N') x) : M'' ∗ N'')
    ((map (f'.comp f) (g'.comp g) : (a : M ∗ N) → M'' ∗ N'') x : M'' ∗ N'')

Tactic:
DFunLike.congr_fun (map_comp_map f' g' f g) x

Premises used: DFunLike.congr_fun, Quotient.liftOn', Con.liftOn, Monoid.Coprod.map_comp_map
-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
inst_4 : MulOneClass P
⊢ Eq (α := N ∗ M)
    ((MonoidHom.comp mk (FreeMonoid.map Sum.swap) : (a : FreeMonoid (M ⊕ N)) → N ∗ M) (of (Sum.inl 1)) : N ∗ M)
    (1 : N ∗ M)

Tactic:
simp only [MonoidHom.comp_apply, map_of, Sum.swap_inl, mk_of_inr, map_one]

Premises used: Monoid.Coprod.mk_of_inr, map_one, FreeMonoid.map_of, Sum.swap_inl, MonoidHom.comp_apply