awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
⊢ Eq (α := FreeGroup α →* Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
    (MonoidHom.comp (N := FreeGroup (α ⊕ β))
      ((FreeGroup.lift :
          (a : α ⊕ β → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)) →
            FreeGroup (α ⊕ β) →* Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂))
        (toCoprod rels₁ rels₂))
      (FreeGroup.map Sum.inl))
    (MonoidHom.comp Monoid.Coprod.inl (mk rels₁))

Tactic:
FreeGroup.ext_hom _ _ fun _ ↦ rfl

Premises used: FreeGroup.ext_hom, rfl
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
⊢ Eq (α := FreeGroup β →* Monoid.Coprod.{u_1, u_2} (PresentedGroup rels₁) (PresentedGroup rels₂))
    (MonoidHom.comp (N := FreeGroup (α ⊕ β))
      ((FreeGroup.lift :
          (a : α ⊕ β → Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂)) →
            FreeGroup (α ⊕ β) →* Monoid.Coprod (PresentedGroup rels₁) (PresentedGroup rels₂))
        (toCoprod rels₁ rels₂))
      (FreeGroup.map Sum.inr))
    (MonoidHom.comp Monoid.Coprod.inr (mk rels₂))

Tactic:
FreeGroup.ext_hom _ _ fun _ ↦ rfl

Premises used: FreeGroup.ext_hom, rfl
-- Module: Mathlib.GroupTheory.PresentedGroup
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₂))
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₂))
⊢ 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₂))

Tactic:
obtain ⟨r, hr, rfl⟩ | ⟨r, hr, rfl⟩ := hr

Premises used: rfl
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
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:
simp [← MonoidHom.comp_apply, one_of_mem hr]

Premises used: PresentedGroup.one_of_mem, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
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:
simp [← MonoidHom.comp_apply, one_of_mem hr]

Premises used: PresentedGroup.one_of_mem, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.PushoutI
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)
⊢ Mul (con (G := G) φ).Quotient

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.PushoutI
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)
⊢ One (con (G := G) φ).Quotient

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.PushoutI
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 : ι
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) φ)
⊢ MonoidHom.comp (of (G := G) i) (φ i) = base (G := G) φ

Tactic:
ext x
-- Module: Mathlib.GroupTheory.PushoutI
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
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)
⊢ 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:
apply (Con.eq _).2

Premises used: Iff.mpr, Con.eq
-- Module: Mathlib.GroupTheory.PushoutI
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)

Tactic:
ConGen.Rel.of _ _ ?_

Premises used: ConGen.Rel.of
-- Module: Mathlib.GroupTheory.PushoutI
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
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)
⊢ (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:
refine ConGen.Rel.of _ _ ?_

Premises used: ConGen.Rel.of
-- Module: Mathlib.GroupTheory.PushoutI
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
⊢ ∃ (i_1 : ι) (x' : H),
    Eq (α := CoprodI G ∗ H)
        ((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)
        ((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:
⟨_, _, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.PushoutI
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
⊢ ∃ (i_1 : ι) (x' : H),
    Eq (α := CoprodI G ∗ H)
        ((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)
        ((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:
exact ⟨_, _, rfl, rfl⟩
-- Module: Mathlib.GroupTheory.PushoutI
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) φ)
rw₁ 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) φ)
⊢ 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) φ)

Tactic:
rw [← MonoidHom.comp_apply, of_comp_eq_base]

Premises used: Monoid.PushoutI.of_comp_eq_base, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.PushoutI
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
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
⊢ 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)

Tactic:
apply Con.conGen_le fun x y => ?_

Premises used: Con.conGen_le
-- Module: Mathlib.GroupTheory.PushoutI
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
⊢ ∀ (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

Premises used: MonoidHom.coe_comp, DFunLike.ext_iff, Function.comp_apply
-- Module: Mathlib.GroupTheory.PushoutI
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
i : ι
x' : H
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)
⊢ (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')

Tactic:
simp [hf]
-- Module: Mathlib.GroupTheory.PushoutI
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
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) ⋯ :
          (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)
⊢ 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)

Tactic:
delta PushoutI lift of

Premises used: Monoid.PushoutI.lift, Monoid.PushoutI, Monoid.PushoutI.of
-- Module: Mathlib.GroupTheory.PushoutI
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)
    (((con (G := G) φ).lift (Coprod.lift ((CoprodI.lift (M := G) : (a : (i : ι) → G i →* K) → CoprodI G →* K) f) k) ⋯ :
          (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:
simp only [MonoidHom.coe_comp, Con.coe_mk', comp_apply, Con.lift_coe,
    lift_apply_inl, CoprodI.lift_of]

Premises used: Monoid.CoprodI.lift_of, MonoidHom.coe_comp, Monoid.Coprod.lift_apply_inl, Con.coe_mk', Con.lift_coe, Function.comp_apply
-- Module: Mathlib.GroupTheory.PushoutI
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
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) ⋯ :
          (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)
⊢ 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)

Tactic:
delta PushoutI lift base

Premises used: Monoid.PushoutI.base, Monoid.PushoutI.lift, Monoid.PushoutI
-- Module: Mathlib.GroupTheory.PushoutI
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)
    (((con (G := G) φ).lift (Coprod.lift ((CoprodI.lift (M := G) : (a : (i : ι) → G i →* K) → CoprodI G →* K) f) k) ⋯ :
          (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:
simp only [MonoidHom.coe_comp, Con.coe_mk', comp_apply, Con.lift_coe, lift_apply_inr]

Premises used: Monoid.Coprod.lift_apply_inr, MonoidHom.coe_comp, Con.coe_mk', Con.lift_coe, Function.comp_apply
-- Module: Mathlib.GroupTheory.PushoutI
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)
hbase : f.comp (base (G := G) φ) = g.comp (base (G := G) φ)
⊢ f = g

Tactic:
(MonoidHom.cancel_right Con.mk'_surjective).mp <|
    Coprod.hom_ext
      (CoprodI.ext_hom _ _ h)
      hbase

Premises used: Con.mk'_surjective, Monoid.PushoutI, Iff.mp, Monoid.CoprodI.ext_hom, Monoid.Coprod.hom_ext, MonoidHom.cancel_right
-- Module: Mathlib.GroupTheory.PushoutI
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 : ι
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)
⊢ f.comp (base (G := G) φ) = g.comp (base (G := G) φ)

Tactic:
ext
-- Module: Mathlib.GroupTheory.PushoutI
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)
intro₃ 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)
⊢ 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:
rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]

Premises used: Monoid.PushoutI.of_comp_eq_base, MonoidHom.comp_assoc
-- Module: Mathlib.GroupTheory.PushoutI
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)
intro : ∀ (i : ι), f.comp (base (G := G) φ) = g.comp (base (G := G) φ)
⊢ 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]

Premises used: MonoidHom.comp_assoc
-- Module: Mathlib.GroupTheory.PushoutI
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
rw₁ rw₂ : f.comp (base (G := G) φ) = (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

Tactic:
rw [MonoidHom.comp_assoc, of_comp_eq_base]

Premises used: Monoid.PushoutI.of_comp_eq_base, MonoidHom.comp_assoc
-- Module: Mathlib.GroupTheory.PushoutI
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)
x : PushoutI (G := G) φ →* K
⊢ ∀ (i : ι),
    MonoidHom.comp (N := PushoutI (G := G) φ)
        ((fun (f : { f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K) // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }) ↦
            lift (G := G) (↑f : ((i : ι) → G i →* K) × (H →* K)).1 (↑f : ((i : ι) → G i →* K) × (H →* K)).2 ⋯)
          ((fun (f : PushoutI (G := G) φ →* K) ↦
              (Subtype.mk (p := fun (f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K)) ↦
                  ∀ (i : ι), (f.1 i).comp (φ i) = f.2) (fun (i : ι) ↦ f.comp (of (G := G) i), f.comp (base (G := G) φ))
                  ⋯ :
                { f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K) // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }))
            x))
        (of (G := G) i) =
      x.comp (of (G := G) i)

Tactic:
simp [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- Module: Mathlib.GroupTheory.PushoutI
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)
x : PushoutI (G := G) φ →* K
⊢ MonoidHom.comp
      ((fun (f : { f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K) // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }) ↦
          lift (G := G) (↑f : ((i : ι) → G i →* K) × (H →* K)).1 (↑f : ((i : ι) → G i →* K) × (H →* K)).2 ⋯)
        ((fun (f : PushoutI (G := G) φ →* K) ↦
            (Subtype.mk (p := fun (f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K)) ↦
                ∀ (i : ι), (f.1 i).comp (φ i) = f.2) (fun (i : ι) ↦ f.comp (of (G := G) i), f.comp (base (G := G) φ))
                ⋯ :
              { f : ((i : ι) → MonoidHom.{u_2, u_4} (G i) K) × (H →* K) // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }))
          x))
      (base (G := G) φ) =
    x.comp (base (G := G) φ)

Tactic:
simp [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff