awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (goal)
Goal:
α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
r : FreeGroup (α ⊕ β)
hr :
  Membership.mem (γ := Set (FreeGroup (α ⊕ β)))
    ((⇑(FreeGroup.map Sum.inl) : (a : FreeGroup α) → FreeGroup (α ⊕ β)) '' rels₁ ∪
      (⇑(FreeGroup.map Sum.inr) : (a : FreeGroup β) → FreeGroup (α ⊕ β)) '' rels₂)
    r
⊢ Eq (α := Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
    ((((FreeGroup.lift :
                (a : α ⊕ β → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)) →
                  FreeGroup (α ⊕ β) →* Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂))
              (toCoprod rels₁ rels₂) :
            FreeGroup (α ⊕ β) →* Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂)) :
          (a : FreeGroup (α ⊕ β)) → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂))
        r :
      Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
    (1 : Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
have inl : ∀ (r : FreeGroup α) (hr : r ∈ rels₁),
  Eq (α := Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
    ((((FreeGroup.lift :
                (a : α ⊕ β → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)) →
                  FreeGroup (α ⊕ β) →* Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂))
              (toCoprod rels₁ rels₂) :
            FreeGroup (α ⊕ β) →* Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂)) :
          (a : FreeGroup (α ⊕ β)) → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂))
        ((FreeGroup.map Sum.inl : (a : FreeGroup α) → FreeGroup (α ⊕ β)) r) :
      Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
    (1 : Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
Tactic: obtain ⟨r, hr, rfl⟩ | ⟨r, hr, rfl⟩ := hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.GroupTheory.PresentedGroup (goal)
Goal:
α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
r : FreeGroup (α ⊕ β)
hr :
  Membership.mem (γ := Set (FreeGroup (α ⊕ β)))
    ((⇑(FreeGroup.map Sum.inl) : (a : FreeGroup α) → FreeGroup (α ⊕ β)) '' rels₁ ∪
      (⇑(FreeGroup.map Sum.inr) : (a : FreeGroup β) → FreeGroup (α ⊕ β)) '' rels₂)
    r
inl :
  ∀ (r : FreeGroup α) (hr : r ∈ rels₁),
    Eq (α := Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
      ((((FreeGroup.lift :
                  (a : α ⊕ β → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)) →
                    FreeGroup (α ⊕ β) →* Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂))
                (toCoprod rels₁ rels₂) :
              FreeGroup (α ⊕ β) →* Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂)) :
            (a : FreeGroup (α ⊕ β)) → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂))
          ((FreeGroup.map Sum.inl : (a : FreeGroup α) → FreeGroup (α ⊕ β)) r) :
        Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
      (1 : Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
⊢ Eq (α := Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
    ((((FreeGroup.lift :
                (a : α ⊕ β → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)) →
                  FreeGroup (α ⊕ β) →* Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂))
              (toCoprod rels₁ rels₂) :
            FreeGroup (α ⊕ β) →* Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂)) :
          (a : FreeGroup (α ⊕ β)) → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂))
        r :
      Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
    (1 : Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
have inr : ∀ (r : FreeGroup β) (hr : r ∈ rels₂),
  Eq (α := Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
    ((((FreeGroup.lift :
                (a : α ⊕ β → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)) →
                  FreeGroup (α ⊕ β) →* Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂))
              (toCoprod rels₁ rels₂) :
            FreeGroup (α ⊕ β) →* Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂)) :
          (a : FreeGroup (α ⊕ β)) → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂))
        ((FreeGroup.map Sum.inr : (a : FreeGroup β) → FreeGroup (α ⊕ β)) r) :
      Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
    (1 : Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
Tactic: obtain ⟨r, hr, rfl⟩ | ⟨r, hr, rfl⟩ := hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
i : ι
⊢ MonoidHom.comp (of (G := G) i) (φ i) = base (G := G) φ
have h : ∀ (x : H),
  Eq (α := PushoutI (G := G) φ) ((MonoidHom.comp (of (G := G) i) (φ i) : (a : H) → PushoutI φ) x : PushoutI (G := G) φ)
    ((base (G := G) φ : (a : H) → PushoutI φ) x : PushoutI (G := G) φ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
i : ι
x : H
⊢ Eq (α := PushoutI (G := G) φ) ((MonoidHom.comp (of (G := G) i) (φ i) : (a : H) → PushoutI φ) x : PushoutI (G := G) φ)
    ((base (G := G) φ : (a : H) → PushoutI φ) x : PushoutI (G := G) φ)
have h : (con (G := G) φ : (a : CoprodI G ∗ H) → CoprodI G ∗ H → Prop)
  ((MonoidHom.comp inl (CoprodI.of (M := G)) : (a : G i) → CoprodI G ∗ H) ((φ i : (a : H) → G i) x) : CoprodI G ∗ H)
  ((inr : (a : H) → CoprodI G ∗ H) x)
Tactic: apply (Con.eq _).2
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
i : ι
x : H
⊢ (con (G := G) φ : (a : CoprodI G ∗ H) → CoprodI G ∗ H → Prop)
    ((MonoidHom.comp inl (CoprodI.of (M := G)) : (a : G i) → CoprodI G ∗ H) ((φ i : (a : H) → G i) x) : CoprodI G ∗ H)
    ((inr : (a : H) → CoprodI G ∗ H) x)
have h : ∃ (i_1 : ι) (x' : H),
  Eq (α := CoprodI G ∗ H)
      ((MonoidHom.comp inl (CoprodI.of (M := G)) : (a : G i) → CoprodI G ∗ H) ((φ i : (a : H) → G i) x) : CoprodI G ∗ H)
      ((inl : (a : CoprodI G) → CoprodI G ∗ H)
          ((CoprodI.of (M := G) : (a : G i_1) → CoprodI G) ((φ i_1 : (a : H) → G i_1) x')) :
        CoprodI G ∗ H) ∧
    Eq (α := CoprodI G ∗ H) ((inr : (a : H) → CoprodI G ∗ H) x : CoprodI G ∗ H)
      ((inr : (a : H) → CoprodI G ∗ H) x' : CoprodI G ∗ H)
Tactic: refine ConGen.Rel.of _ _ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
i : ι
x : H
⊢ Eq (α := PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) x) : PushoutI (G := G) φ)
    ((base (G := G) φ : (a : H) → PushoutI φ) x : PushoutI (G := G) φ)
have rw : Eq (α := PushoutI (G := G) φ) ((MonoidHom.comp (of (G := G) i) (φ i) : (a : H) → PushoutI φ) x : PushoutI (G := G) φ)
  ((base (G := G) φ : (a : H) → PushoutI φ) x : PushoutI (G := G) φ)
Tactic: rw [← MonoidHom.comp_apply, of_comp_eq_base]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
i : ι
x : H
rw :
  Eq (α := PushoutI (G := G) φ) ((MonoidHom.comp (of (G := G) i) (φ i) : (a : H) → PushoutI φ) x : PushoutI (G := G) φ)
    ((base (G := G) φ : (a : H) → PushoutI φ) x : PushoutI (G := G) φ)
⊢ Eq (α := PushoutI (G := G) φ)
    ((of (G := G) i : (a : G i) → PushoutI φ) ((φ i : (a : H) → G i) x) : PushoutI (G := G) φ)
    ((base (G := G) φ : (a : H) → PushoutI φ) x : PushoutI (G := G) φ)
have rw₁ : Eq (α := PushoutI (G := G) φ) ((base (G := G) φ : (a : H) → PushoutI φ) x : PushoutI (G := G) φ)
  ((base (G := G) φ : (a : H) → PushoutI φ) x : PushoutI (G := G) φ)
Tactic: rw [← MonoidHom.comp_apply, of_comp_eq_base]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
f : (i : ι) → MonoidHom.{u_2, u_4} (G i) K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
⊢ con (G := G) φ ≤
    Con.ker (F := CoprodI G ∗ H →* K)
      (Coprod.lift ((CoprodI.lift (M := G) : (a : (i : ι) → G i →* K) → CoprodI G →* K) f) k)
have apply : ∀ (x y : CoprodI G ∗ H),
  (∃ (i : ι) (x' : H),
      x =
          (inl : (a : CoprodI G) → CoprodI G ∗ H)
            ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) x')) ∧
        y = (inr : (a : H) → CoprodI G ∗ H) x') →
    (Con.ker (F := CoprodI G ∗ H →* K)
          (Coprod.lift ((CoprodI.lift (M := G) : (a : (i : ι) → G i →* K) → CoprodI G →* K) f) k) :
        (a : CoprodI G ∗ H) → CoprodI G ∗ H → Prop)
      x y
Tactic: apply Con.conGen_le fun x y => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (hypothesis)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
f : (i : ι) → MonoidHom.{u_2, u_4} (G i) K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
i : ι
x' : H
⊢ (Con.ker (F := CoprodI G ∗ H →* K)
        (Coprod.lift ((CoprodI.lift (M := G) : (a : (i : ι) → G i →* K) → CoprodI G →* K) f) k) :
      (a : CoprodI G ∗ H) → CoprodI G ∗ H → Prop)
    ((inl : (a : CoprodI G) → CoprodI G ∗ H)
        ((CoprodI.of (M := G) : (a : G i) → CoprodI G) ((φ i : (a : H) → G i) x')) :
      CoprodI G ∗ H)
    ((inr : (a : H) → CoprodI G ∗ H) x')
have hf₁ : ∀ (i : ι) (x : H),
  Eq.{u_4 + 1} (α := K) ((f i : (a : G i) → K) ((φ i : (a : H) → G i) x : G i) : K) ((k : (a : H) → K) x : K)
Tactic: simp only [DFunLike.ext_iff, MonoidHom.coe_comp, comp_apply] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
f : (i : ι) → MonoidHom.{u_2, u_4} (G i) K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
i : ι
g : G i
⊢ Eq.{u_4 + 1} (α := K)
    ((lift (G := G) f k hf : (a : PushoutI φ) → K) ((of (G := G) i : (a : G i) → PushoutI φ) g : PushoutI (G := G) φ) :
      K)
    ((f i : (a : G i) → K) g : K)
have delta : Eq.{u_4 + 1} (α := K)
  (((con (G := G) φ).lift (Coprod.lift ((CoprodI.lift (M := G) : (a : (i : ι) → G i →* K) → CoprodI G →* K) f) k) sorry :
        (a : (con φ).Quotient) → K)
      (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g :
        (con (G := G) φ).Quotient) :
    K)
  ((f i : (a : G i) → K) g : K)
Tactic: delta PushoutI lift of
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
f : (i : ι) → MonoidHom.{u_2, u_4} (G i) K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
g : H
⊢ Eq.{u_4 + 1} (α := K)
    ((lift (G := G) f k hf : (a : PushoutI φ) → K) ((base (G := G) φ : (a : H) → PushoutI φ) g : PushoutI (G := G) φ) :
      K)
    ((k : (a : H) → K) g : K)
have delta : Eq.{u_4 + 1} (α := K)
  (((con (G := G) φ).lift (Coprod.lift ((CoprodI.lift (M := G) : (a : (i : ι) → G i →* K) → CoprodI G →* K) f) k) sorry :
        (a : (con φ).Quotient) → K)
      (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) g : (con (G := G) φ).Quotient) :
    K)
  ((k : (a : H) → K) g : K)
Tactic: delta PushoutI lift base
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
f g : PushoutI (G := G) φ →* K
h : ∀ (i : ι), f.comp (of (G := G) i) = g.comp (of (G := G) i)
i : ι
⊢ f.comp (base (G := G) φ) = g.comp (base (G := G) φ)
have intro : ∀ (x : H),
  Eq.{u_4 + 1} (α := K) ((f.comp (base (G := G) φ) : (a : H) → K) x : K)
    ((g.comp (base (G := G) φ) : (a : H) → K) x : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
f g : PushoutI (G := G) φ →* K
h : ∀ (i : ι), f.comp (of (G := G) i) = g.comp (of (G := G) i)
i : ι
x : H
⊢ Eq.{u_4 + 1} (α := K) ((f.comp (base (G := G) φ) : (a : H) → K) x : K)
    ((g.comp (base (G := G) φ) : (a : H) → K) x : K)
have intro : Eq.{u_4 + 1} (α := K) ((f.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
  ((g.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
Tactic: rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
f g : PushoutI (G := G) φ →* K
h : ∀ (i : ι), f.comp (of (G := G) i) = g.comp (of (G := G) i)
i : ι
x : H
intro :
  Eq.{u_4 + 1} (α := K) ((f.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
    ((g.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
⊢ Eq.{u_4 + 1} (α := K) ((f.comp (base (G := G) φ) : (a : H) → K) x : K)
    ((g.comp (base (G := G) φ) : (a : H) → K) x : K)
have intro₁ : Eq.{u_4 + 1} (α := K) (((f.comp (of (G := G) i)).comp (φ i) : (a : H) → K) x : K)
  ((g.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
Tactic: rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
f g : PushoutI (G := G) φ →* K
h : ∀ (i : ι), f.comp (of (G := G) i) = g.comp (of (G := G) i)
i : ι
x : H
intro :
  Eq.{u_4 + 1} (α := K) ((f.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
    ((g.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
intro₁ :
  Eq.{u_4 + 1} (α := K) (((f.comp (of (G := G) i)).comp (φ i) : (a : H) → K) x : K)
    ((g.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
⊢ Eq.{u_4 + 1} (α := K) ((f.comp (base (G := G) φ) : (a : H) → K) x : K)
    ((g.comp (base (G := G) φ) : (a : H) → K) x : K)
have intro₂ : Eq.{u_4 + 1} (α := K) (((g.comp (of (G := G) i)).comp (φ i) : (a : H) → K) x : K)
  ((g.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
Tactic: rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
f g : PushoutI (G := G) φ →* K
h : ∀ (i : ι), f.comp (of (G := G) i) = g.comp (of (G := G) i)
i : ι
x : H
intro :
  Eq.{u_4 + 1} (α := K) ((f.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
    ((g.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
intro₁ :
  Eq.{u_4 + 1} (α := K) (((f.comp (of (G := G) i)).comp (φ i) : (a : H) → K) x : K)
    ((g.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
intro₂ :
  Eq.{u_4 + 1} (α := K) (((g.comp (of (G := G) i)).comp (φ i) : (a : H) → K) x : K)
    ((g.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
⊢ Eq.{u_4 + 1} (α := K) ((f.comp (base (G := G) φ) : (a : H) → K) x : K)
    ((g.comp (base (G := G) φ) : (a : H) → K) x : K)
have intro₃ : Eq.{u_4 + 1} (α := K) ((g.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
  ((g.comp (MonoidHom.comp (of (G := G) i) (φ i)) : (a : H) → K) x : K)
Tactic: rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hn : Nonempty ι
f g : PushoutI (G := G) φ →* K
h : ∀ (i : ι), f.comp (of (G := G) i) = g.comp (of (G := G) i)
⊢ f.comp (base (G := G) φ) = g.comp (base (G := G) φ)
have intro : ∀ (i : ι), f.comp (base (G := G) φ) = g.comp (base (G := G) φ)
Tactic: cases hn with
    | intro i =>
      ext
      rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
f : PushoutI (G := G) φ →* K
i : ι
⊢ MonoidHom.comp ((fun (i : ι) ↦ f.comp (of (G := G) i), f.comp (base (G := G) φ)).1 i) (φ i) =
    (fun (i : ι) ↦ f.comp (of (G := G) i), f.comp (base (G := G) φ)).2
have rw : f.comp (MonoidHom.comp (of (G := G) i) (φ i)) = (fun (i : ι) ↦ f.comp (of (G := G) i), f.comp (base (G := G) φ)).2
Tactic: rw [MonoidHom.comp_assoc, of_comp_eq_base]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Monoid (G i)
inst_2 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
f : PushoutI (G := G) φ →* K
i : ι
rw : f.comp (MonoidHom.comp (of (G := G) i) (φ i)) = (fun (i : ι) ↦ f.comp (of (G := G) i), f.comp (base (G := G) φ)).2
⊢ MonoidHom.comp ((fun (i : ι) ↦ f.comp (of (G := G) i), f.comp (base (G := G) φ)).1 i) (φ i) =
    (fun (i : ι) ↦ f.comp (of (G := G) i), f.comp (base (G := G) φ)).2
have rw₁ : f.comp (base (G := G) φ) = (fun (i : ι) ↦ f.comp (of (G := G) i), f.comp (base (G := G) φ)).2
Tactic: rw [MonoidHom.comp_assoc, of_comp_eq_base]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
x y : CoprodI G
ihx : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) x) : (con φ).Quotient)
ihy : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) y) : (con φ).Quotient)
⊢ motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) (x * y)) : (con φ).Quotient)
have H₁ : motive
  (↑(HMul.hMul (α := CoprodI G ∗ H) (β := CoprodI G ∗ H) ((inl : (a : CoprodI G) → CoprodI G ∗ H) x : CoprodI G ∗ H)
        ((inl : (a : CoprodI G) → CoprodI G ∗ H) y : CoprodI G ∗ H)) :
    (con φ).Quotient)
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
g : CoprodI G
⊢ motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) g) : (con φ).Quotient)
have H₁ : ∀ (i : ι) (g : G i),
  motive
    (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) ((CoprodI.of (M := G) : (a : G i) → CoprodI G) g)) : (con φ).Quotient)
Tactic: induction g using CoprodI.induction_on with
      | of i g => exact of i g
      | mul x y ihx ihy =>
        rw [map_mul]
        exact mul _ _ ihx ihy
      | one => simpa using base 1
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
g : CoprodI G
H₁ :
  ∀ (i : ι) (g : G i),
    motive
      (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) ((CoprodI.of (M := G) : (a : G i) → CoprodI G) g)) : (con φ).Quotient)
⊢ motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) g) : (con φ).Quotient)
have H₂ : ∀ (x y : CoprodI G) (ihx : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) x) : (con φ).Quotient))
  (ihy : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) y) : (con φ).Quotient)),
  motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) (x * y)) : (con φ).Quotient)
Tactic: induction g using CoprodI.induction_on with
      | of i g => exact of i g
      | mul x y ihx ihy =>
        rw [map_mul]
        exact mul _ _ ihx ihy
      | one => simpa using base 1
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Monoid (G i)
inst_1 : Monoid H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
motive : (con (G := G) φ).Quotient → Prop
of :
  ∀ (i : ι) (g : G i),
    motive (((con (G := G) φ).mk'.comp (MonoidHom.comp inl (CoprodI.of (M := G))) : (a : G i) → (con φ).Quotient) g)
base : ∀ (h : H), motive (((con (G := G) φ).mk'.comp inr : (a : H) → (con φ).Quotient) h)
mul : ∀ (x y : (con (G := G) φ).Quotient), motive x → motive y → motive (x * y)
g : CoprodI G
H₁ :
  ∀ (i : ι) (g : G i),
    motive
      (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) ((CoprodI.of (M := G) : (a : G i) → CoprodI G) g)) : (con φ).Quotient)
H₂ :
  ∀ (x y : CoprodI G) (ihx : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) x) : (con φ).Quotient))
    (ihy : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) y) : (con φ).Quotient)),
    motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) (x * y)) : (con φ).Quotient)
⊢ motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) g) : (con φ).Quotient)
have H₃ : motive (↑((inl : (a : CoprodI G) → CoprodI G ∗ H) 1) : (con φ).Quotient)
Tactic: induction g using CoprodI.induction_on with
      | of i g => exact of i g
      | mul x y ihx ihy =>
        rw [map_mul]
        exact mul _ _ ihx ihy
      | one => simpa using base 1
Cleared hypotheses: g