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 : 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))
⊢ C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) (of x * xs))
have mul_of₁ : ∀ (n : N), C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) (of (Sum.inr n) * xs))
Tactic: cases x with
    | inl m => simpa using inl_mul m _ ih
    | inr n => simpa using inr_mul n _ ih
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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)
⊢ C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) x)
have one₁ : C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) 1)
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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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)
⊢ C ((mk : (a : FreeMonoid (M ⊕ N)) → M ∗ N) x)
have 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))
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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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))) ⊤
have 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)))
Tactic: rw [← mrange_mk, MonoidHom.mrange_eq_map, ← closure_range_of, MonoidHom.map_mclosure,
    ← range_comp, Sum.range_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
⊢ Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr) ⊤
have 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)))
Tactic: rw [← mclosure_range_inl_union_inr, Submonoid.closure_union, ← MonoidHom.coe_mrange,
    ← MonoidHom.coe_mrange, Submonoid.closure_eq, Submonoid.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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)))
⊢ Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr) ⊤
have 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)))
Tactic: rw [← mclosure_range_inl_union_inr, Submonoid.closure_union, ← MonoidHom.coe_mrange,
    ← MonoidHom.coe_mrange, Submonoid.closure_eq, Submonoid.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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)))
⊢ Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr) ⊤
have 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)))
Tactic: rw [← mclosure_range_inl_union_inr, Submonoid.closure_union, ← MonoidHom.coe_mrange,
    ← MonoidHom.coe_mrange, Submonoid.closure_eq, Submonoid.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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)))
⊢ Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr) ⊤
have 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)))
Tactic: rw [← mclosure_range_inl_union_inr, Submonoid.closure_union, ← MonoidHom.coe_mrange,
    ← MonoidHom.coe_mrange, Submonoid.closure_eq, Submonoid.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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)))
⊢ Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr) ⊤
have 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)))
Tactic: rw [← mclosure_range_inl_union_inr, Submonoid.closure_union, ← MonoidHom.coe_mrange,
    ← MonoidHom.coe_mrange, Submonoid.closure_eq, Submonoid.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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)))
⊢ Eq (α := Submonoid (M ∗ N)) (MonoidHom.mrange (F := M →* M ∗ N) inl ⊔ MonoidHom.mrange (F := N →* M ∗ N) inr) ⊤
have 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)
Tactic: rw [← mclosure_range_inl_union_inr, Submonoid.closure_union, ← MonoidHom.coe_mrange,
    ← MonoidHom.coe_mrange, Submonoid.closure_eq, Submonoid.closure_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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
⊢ Eq (α := Submonoid P) (MonoidHom.mrange f) (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))
have rw : Eq (α := Submonoid P) (Submonoid.map 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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))
⊢ Eq (α := Submonoid P) (MonoidHom.mrange f) (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))
have 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))
Tactic: rw [MonoidHom.mrange_eq_map, ← mrange_inl_sup_mrange_inr, Submonoid.map_sup, MonoidHom.map_mrange,
    MonoidHom.map_mrange]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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))
⊢ Eq (α := Submonoid P) (MonoidHom.mrange f) (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))
have 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))
Tactic: rw [MonoidHom.mrange_eq_map, ← mrange_inl_sup_mrange_inr, Submonoid.map_sup, MonoidHom.map_mrange,
    MonoidHom.map_mrange]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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))
⊢ Eq (α := Submonoid P) (MonoidHom.mrange f) (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))
have 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))
Tactic: rw [MonoidHom.mrange_eq_map, ← mrange_inl_sup_mrange_inr, Submonoid.map_sup, MonoidHom.map_mrange,
    MonoidHom.map_mrange]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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))
⊢ Eq (α := Submonoid P) (MonoidHom.mrange f) (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))
have rw₄ : Eq (α := Submonoid P) (MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr))
  (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]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
P' : Type u_4
inst_3 : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
⊢ (f.comp (lift g₁ g₂)).comp inl = (lift (f.comp g₁) (f.comp g₂)).comp inl
have rw : f.comp ((lift g₁ g₂).comp inl) = (lift (f.comp g₁) (f.comp g₂)).comp inl
Tactic: rw [MonoidHom.comp_assoc, lift_comp_inl, lift_comp_inl]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
P' : Type u_4
inst_3 : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
rw : f.comp ((lift g₁ g₂).comp inl) = (lift (f.comp g₁) (f.comp g₂)).comp inl
⊢ (f.comp (lift g₁ g₂)).comp inl = (lift (f.comp g₁) (f.comp g₂)).comp inl
have rw₁ : f.comp g₁ = (lift (f.comp g₁) (f.comp g₂)).comp inl
Tactic: rw [MonoidHom.comp_assoc, lift_comp_inl, lift_comp_inl]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
P' : Type u_4
inst_3 : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
rw : f.comp ((lift g₁ g₂).comp inl) = (lift (f.comp g₁) (f.comp g₂)).comp inl
rw₁ : f.comp g₁ = (lift (f.comp g₁) (f.comp g₂)).comp inl
⊢ (f.comp (lift g₁ g₂)).comp inl = (lift (f.comp g₁) (f.comp g₂)).comp inl
have rw₂ : f.comp g₁ = f.comp g₁
Tactic: rw [MonoidHom.comp_assoc, lift_comp_inl, lift_comp_inl]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
P' : Type u_4
inst_3 : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
⊢ (f.comp (lift g₁ g₂)).comp inr = (lift (f.comp g₁) (f.comp g₂)).comp inr
have rw : f.comp ((lift g₁ g₂).comp inr) = (lift (f.comp g₁) (f.comp g₂)).comp inr
Tactic: rw [MonoidHom.comp_assoc, lift_comp_inr, lift_comp_inr]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
P' : Type u_4
inst_3 : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
rw : f.comp ((lift g₁ g₂).comp inr) = (lift (f.comp g₁) (f.comp g₂)).comp inr
⊢ (f.comp (lift g₁ g₂)).comp inr = (lift (f.comp g₁) (f.comp g₂)).comp inr
have rw₁ : f.comp g₂ = (lift (f.comp g₁) (f.comp g₂)).comp inr
Tactic: rw [MonoidHom.comp_assoc, lift_comp_inr, lift_comp_inr]
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : Monoid P
P' : Type u_4
inst_3 : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
rw : f.comp ((lift g₁ g₂).comp inr) = (lift (f.comp g₁) (f.comp g₂)).comp inr
rw₁ : f.comp g₂ = (lift (f.comp g₁) (f.comp g₂)).comp inr
⊢ (f.comp (lift g₁ g₂)).comp inr = (lift (f.comp g₁) (f.comp g₂)).comp inr
have rw₂ : f.comp g₂ = f.comp g₂
Tactic: rw [MonoidHom.comp_assoc, lift_comp_inr, lift_comp_inr]
-- 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
⊢ Eq (α := M ∗ N →* M × N) (MonoidHom.prod fst snd) toProd
have h₁ : Eq (α := M →* M × N) (MonoidHom.comp (MonoidHom.prod fst snd) inl) (MonoidHom.comp toProd inl)
Tactic: ext1
-- 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
h₁ : Eq (α := M →* M × N) (MonoidHom.comp (MonoidHom.prod fst snd) inl) (MonoidHom.comp toProd inl)
⊢ Eq (α := M ∗ N →* M × N) (MonoidHom.prod fst snd) toProd
have h₂ : Eq (α := N →* M × N) (MonoidHom.comp (MonoidHom.prod fst snd) inr) (MonoidHom.comp toProd inr)
Tactic: ext1
-- 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
⊢ Eq (α := M × N) (((fst : (a : M ∗ N) → M) x, (snd : (a : M ∗ N) → N) x) : M × N)
    ((toProd : (a : M ∗ N) → M × N) x : M × N)
have rw : Eq (α := M × N) (((fst : (a : M ∗ N) → M) x, (snd : (a : M ∗ N) → N) x) : M × N)
  ((MonoidHom.prod fst snd : (a : M ∗ N) → M × N) x : M × N)
Tactic: rw [← fst_prod_snd, MonoidHom.prod_apply]
-- 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 :
  Eq (α := M × N) (((fst : (a : M ∗ N) → M) x, (snd : (a : M ∗ N) → N) x) : M × N)
    ((MonoidHom.prod fst snd : (a : M ∗ N) → M × N) x : M × N)
⊢ Eq (α := M × N) (((fst : (a : M ∗ N) → M) x, (snd : (a : M ∗ N) → N) x) : M × N)
    ((toProd : (a : M ∗ N) → M × N) x : M × N)
have rw₁ : Eq (α := M × N) (((fst : (a : M ∗ N) → M) x, (snd : (a : M ∗ N) → N) x) : M × N)
  (((fst : (a : M ∗ N) → M) x, (snd : (a : M ∗ N) → N) x) : M × N)
Tactic: rw [← fst_prod_snd, MonoidHom.prod_apply]
-- 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
⊢ Eq (α := M ∗ N →* M) (MonoidHom.comp (MonoidHom.fst M N) toProd) fst
have rw : Eq (α := M ∗ N →* M) (MonoidHom.comp (MonoidHom.fst M N) (MonoidHom.prod fst snd)) fst
Tactic: rw [← fst_prod_snd, MonoidHom.fst_comp_prod]
-- 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
rw : Eq (α := M ∗ N →* M) (MonoidHom.comp (MonoidHom.fst M N) (MonoidHom.prod fst snd)) fst
⊢ Eq (α := M ∗ N →* M) (MonoidHom.comp (MonoidHom.fst M N) toProd) fst
have rw₁ : Eq (α := M ∗ N →* M) fst fst
Tactic: rw [← fst_prod_snd, MonoidHom.fst_comp_prod]
-- 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
⊢ Eq.{u_1 + 1} (α := M) (((toProd : (a : M ∗ N) → M × N) x).1 : M) ((fst : (a : M ∗ N) → M) x : M)
have rw : Eq.{u_1 + 1} (α := M) (((toProd : (a : M ∗ N) → M × N) x).1 : M)
  ((MonoidHom.comp (MonoidHom.fst M N) toProd : (a : M ∗ N) → M) x : M)
Tactic: rw [← fst_comp_toProd]
-- 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
⊢ Eq (α := M ∗ N →* N) (MonoidHom.comp (MonoidHom.snd M N) toProd) snd
have rw : Eq (α := M ∗ N →* N) (MonoidHom.comp (MonoidHom.snd M N) (MonoidHom.prod fst snd)) snd
Tactic: rw [← fst_prod_snd, MonoidHom.snd_comp_prod]
-- 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
rw : Eq (α := M ∗ N →* N) (MonoidHom.comp (MonoidHom.snd M N) (MonoidHom.prod fst snd)) snd
⊢ Eq (α := M ∗ N →* N) (MonoidHom.comp (MonoidHom.snd M N) toProd) snd
have rw₁ : Eq (α := M ∗ N →* N) snd snd
Tactic: rw [← fst_prod_snd, MonoidHom.snd_comp_prod]
-- 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
⊢ Eq.{u_2 + 1} (α := N) (((toProd : (a : M ∗ N) → M × N) x).2 : N) ((snd : (a : M ∗ N) → N) x : N)
have rw : Eq.{u_2 + 1} (α := N) (((toProd : (a : M ∗ N) → M × N) x).2 : N)
  ((MonoidHom.comp (MonoidHom.snd M N) toProd : (a : M ∗ N) → N) x : N)
Tactic: rw [← snd_comp_toProd]
-- 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
⊢ (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 : 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
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
⊢ (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₁ : 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
Tactic: rw [map_mul, toProd_apply_inl, toProd_apply_inr, Prod.fst_mul_snd]