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
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')
⊢ 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')))
            inr :
          (a : M') → M ∗ M')
        x :
      M ∗ M')
    ((MonoidHom.comp (MonoidHom.id (M ∗ M')) inr : (a : M') → M ∗ M') x : M ∗ M')
Tactic: ext
-- 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 (α := 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'))
have 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')
Tactic: ext
-- 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'
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')
⊢ 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'))
have 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')
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Monoid M
inst_1 : Monoid N
inst_2 : Monoid 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)))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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))
⊢ 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)))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Coprod.Basic (goal)
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))
⊢ 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)))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
f g : CoprodI M →* N
h : ∀ (i : ι), Eq (α := MonoidHom.{u_2, u_3} (M i) N) (f.comp (of (M := M))) (g.comp (of (M := M)))
x_1 : (i : ι) × M i
i : ι
x : M i
⊢ Eq.{u_3 + 1} (α := N)
    ((f.comp (Con.mk' (conGen (Rel M))) : (a : FreeMonoid ((i : ι) × M i)) → N)
        (FreeMonoid.of (Sigma.mk (β := fun (i : ι) ↦ M i) i x)) :
      N)
    ((g.comp (Con.mk' (conGen (Rel M))) : (a : FreeMonoid ((i : ι) × M i)) → N)
        (FreeMonoid.of (Sigma.mk (β := fun (i : ι) ↦ M i) i x)) :
      N)
have rw : Eq.{u_3 + 1} (α := N)
  ((f : (a : (conGen (Rel M)).Quotient) → N) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) : N)
  ((g : (a : (conGen (Rel M)).Quotient) → N) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) : N)
Tactic: rw [MonoidHom.comp_apply, MonoidHom.comp_apply, ← of_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
f g : CoprodI M →* N
h : ∀ (i : ι), Eq (α := MonoidHom.{u_2, u_3} (M i) N) (f.comp (of (M := M))) (g.comp (of (M := M)))
x_1 : (i : ι) × M i
i : ι
x : M i
⊢ Eq.{u_3 + 1} (α := N)
    ((f : (a : (conGen (Rel M)).Quotient) → N) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) : N)
    ((g : (a : (conGen (Rel M)).Quotient) → N) ((of (M := M) : (a : M i) → CoprodI M) x : CoprodI M) : N)
have unfold : Eq.{u_3 + 1} (α := N)
  ((f : (a : (conGen (Rel M)).Quotient) → N)
      ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
    N)
  ((g : (a : (conGen (Rel M)).Quotient) → N)
      ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
    N)
Tactic: unfold CoprodI
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
f g : CoprodI M →* N
h : ∀ (i : ι), Eq (α := MonoidHom.{u_2, u_3} (M i) N) (f.comp (of (M := M))) (g.comp (of (M := M)))
x_1 : (i : ι) × M i
i : ι
x : M i
⊢ Eq.{u_3 + 1} (α := N)
    ((f : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)
    ((g : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)
have rw : Eq.{u_3 + 1} (α := N) ((f.comp (of (M := M)) : (a : M i) → N) x : N)
  ((g : (a : (conGen (Rel M)).Quotient) → N)
      ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
    N)
Tactic: rw [← MonoidHom.comp_apply, ← MonoidHom.comp_apply, h]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
f g : CoprodI M →* N
h : ∀ (i : ι), Eq (α := MonoidHom.{u_2, u_3} (M i) N) (f.comp (of (M := M))) (g.comp (of (M := M)))
x_1 : (i : ι) × M i
i : ι
x : M i
rw :
  Eq.{u_3 + 1} (α := N) ((f.comp (of (M := M)) : (a : M i) → N) x : N)
    ((g : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)
⊢ Eq.{u_3 + 1} (α := N)
    ((f : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)
    ((g : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)
have rw₁ : Eq.{u_3 + 1} (α := N) ((f.comp (of (M := M)) : (a : M i) → N) x : N) ((g.comp (of (M := M)) : (a : M i) → N) x : N)
Tactic: rw [← MonoidHom.comp_apply, ← MonoidHom.comp_apply, h]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
f g : CoprodI M →* N
h : ∀ (i : ι), Eq (α := MonoidHom.{u_2, u_3} (M i) N) (f.comp (of (M := M))) (g.comp (of (M := M)))
x_1 : (i : ι) × M i
i : ι
x : M i
rw :
  Eq.{u_3 + 1} (α := N) ((f.comp (of (M := M)) : (a : M i) → N) x : N)
    ((g : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)
rw₁ :
  Eq.{u_3 + 1} (α := N) ((f.comp (of (M := M)) : (a : M i) → N) x : N) ((g.comp (of (M := M)) : (a : M i) → N) x : N)
⊢ Eq.{u_3 + 1} (α := N)
    ((f : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)
    ((g : (a : (conGen (Rel M)).Quotient) → N)
        ((of (M := M) : (a : M i) → (conGen (Rel M)).Quotient) x : Con.Quotient (conGen (Rel M))) :
      N)
have rw₂ : Eq.{u_3 + 1} (α := N) ((g.comp (of (M := M)) : (a : M i) → N) x : N) ((g.comp (of (M := M)) : (a : M i) → N) x : N)
Tactic: rw [← MonoidHom.comp_apply, ← MonoidHom.comp_apply, h]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N
⊢ (fun (f : CoprodI M →* N) (x : ι) ↦ (f.comp (of (M := M)) : MonoidHom.{u_2, u_3} (M x) N))
      ((fun (fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N) ↦
          Con.lift (conGen (Rel M))
            ((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N) fun (p : (i : ι) × M i) ↦
              (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)))
            ⋯)
        fi) =
    fi
have h : ∀ (i : ι) (x : M i),
  Eq.{u_3 + 1} (α := N)
    (((fun (f : CoprodI M →* N) (x : ι) ↦ (f.comp (of (M := M)) : MonoidHom.{u_2, u_3} (M x) N))
            ((fun (fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N) ↦
                Con.lift (conGen (Rel M))
                  ((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N)
                    fun (p : (i : ι) × M i) ↦
                    (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)))
                  sorry)
              fi)
            i :
          (a : M i) → N)
        x :
      N)
    ((fi i : (a : M i) → N) x : N)
Tactic: ext i x
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
f : CoprodI M →* N
⊢ (fun (fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N) ↦
        Con.lift (conGen (Rel M))
          ((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N) fun (p : (i : ι) × M i) ↦
            (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)))
          ⋯)
      ((fun (f : CoprodI M →* N) (x : ι) ↦ (f.comp (of (M := M)) : MonoidHom.{u_2, u_3} (M x) N)) f) =
    f
have h : ∀ (i : ι) (x : M i),
  Eq.{u_3 + 1} (α := N)
    ((MonoidHom.comp
            ((fun (fi : (i : ι) → MonoidHom.{u_2, u_3} (M i) N) ↦
                Con.lift (conGen (Rel M))
                  ((FreeMonoid.lift : (a : (i : ι) × M i → N) → FreeMonoid ((i : ι) × M i) →* N)
                    fun (p : (i : ι) × M i) ↦
                    (fi (p.fst (β := fun (i : ι) ↦ M i)) : (a : M p.fst) → N) (p.snd (β := fun (i : ι) ↦ M i)))
                  sorry)
              ((fun (f : CoprodI M →* N) (x : ι) ↦ (f.comp (of (M := M)) : MonoidHom.{u_2, u_3} (M x) N)) f))
            (of (M := M)) :
          (a : M i) → N)
        x :
      N)
    ((f.comp (of (M := M)) : (a : M i) → N) x : N)
Tactic: ext i x
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_4
inst_1 : Monoid N
f : (i : ι) → MonoidHom.{u_2, u_4} (M i) N
⊢ Eq (α := Submonoid N)
    (MonoidHom.mrange (F := CoprodI M →* N)
      ((lift (M := M) : (a : (i : ι) → M i →* N) → CoprodI M →* N) f : CoprodI M →* N))
    (⨆ (i : ι), MonoidHom.mrange (f i))
have rw : Eq.{u_4 + 1} (α := Submonoid N)
  (⨆ (i : ι),
    Submonoid.closure
      (range fun (b : M i) ↦
        (f ((Sigma.mk (β := fun (i : ι) ↦ M i) i b).fst (β := fun (i : ι) ↦ M i)) : (a : M ⟨i, b⟩.fst) → N)
          ((Sigma.mk (β := fun (i : ι) ↦ M i) i b).snd (β := fun (i : ι) ↦ M i))))
  (⨆ (i : ι), MonoidHom.mrange (f i))
Tactic: rw [lift, Equiv.coe_fn_mk, Con.lift_range, FreeMonoid.mrange_lift,
    range_sigma_eq_iUnion_range, Submonoid.closure_iUnion]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul :
  ∀ {i : ι} (m : M i) (x : CoprodI M),
    motive x → motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) x)
x : CoprodI M
hx : Membership.mem (γ := Set (CoprodI M)) (⋃ (i : ι), range (ι := M i) (⇑(of (M := M)) : (a : M i) → CoprodI M)) x
y : CoprodI M
ihy : motive y
⊢ motive (x * y)
have mul_left : ∀ (i : ι) (m : M i)
  (hx :
    Membership.mem (α := CoprodI M) (γ := Set (CoprodI M))
      (⋃ (i : ι), range (ι := M i) (⇑(of (M := M)) : (a : M i) → CoprodI M))
      ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M)),
  motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) y)
Tactic: obtain ⟨i, m, rfl⟩ : ∃ (i : ι) (m : M i), of m = x := by simpa using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
m : CoprodI M
one : motive 1
mul :
  ∀ {i : ι} (m : M i) (x : CoprodI M),
    motive x → motive (HMul.hMul (α := CoprodI M) ((of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) x)
one₁ : motive 1
⊢ motive m
have mul_left : ∀ (x : CoprodI M)
  (hx : Membership.mem (γ := Set (CoprodI M)) (⋃ (i : ι), range (ι := M i) (⇑(of (M := M)) : (a : M i) → CoprodI M)) x)
  (y : CoprodI M) (ihy : motive y), motive (x * y)
Tactic: induction m using Submonoid.induction_of_closure_eq_top_left mclosure_iUnion_range_of with
  | one => exact one
  | mul_left x hx y ihy =>
    obtain ⟨i, m, rfl⟩ : ∃ (i : ι) (m : M i), of m = x := by simpa using hx
    exact mul m y ihy
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
m : CoprodI G
⊢ m⁻¹ * m = 1
have rw : MulOpposite.unop
      (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
            MonoidHom.comp (N := (G i)ᵐᵒᵖ)
              ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
              (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
          (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
        m) *
    m =
  1
Tactic: rw [inv_def]
-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
⊢ HMul.hMul (α := CoprodI G)
      (MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          1))
      1 =
    1
have one : HMul.hMul (α := CoprodI G) (MulOpposite.unop 1) 1 = 1
Tactic: rw [map_one, MulOpposite.unop_one, one_mul]