awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
obtain :
  ∀ (W : C) (w : Y ⟶ W) (hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0)
    (hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)), u = v
⊢ u = v

Tactic:
obtain ⟨W, w, hw, hl⟩ := normalMonoOfMono (equalizer.ι u v)

Premises used: CategoryTheory.Limits.equalizer.ι, CategoryTheory.normalMonoOfMono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
obtain : ∀ (m : X ⟶ equalizer u v) (hm : m ≫ equalizer.ι u v = f), u = v
⊢ u = v

Tactic:
obtain ⟨m, hm⟩ := equalizer.lift' f huv

Premises used: CategoryTheory.Limits.equalizer.lift'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
rw : (m ≫ equalizer.ι u v) ≫ w = 0
rw₁ : m ≫ equalizer.ι u v ≫ w = 0
rw₂ : Eq (α := X ⟶ W) (m ≫ 0) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := X ⟶ W) 0 0
⊢ f ≫ w = 0

Tactic:
rw [← hm, Category.assoc, hw, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
⊢ f ≫ w = 0

Tactic:
have hwf : f ≫ w = 0 := by rw [← hm, Category.assoc, hw, comp_zero]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
obtain :
  ∀ (n : Cocone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯) ⟶ W)
    (hn : Cofork.π (CokernelCofork.ofπ (Z := Z) 0 ⋯) ≫ n = w), u = v
⊢ u = v

Tactic:
obtain ⟨n, hn⟩ := CokernelCofork.IsColimit.desc' l _ hwf

Premises used: CategoryTheory.Limits.CokernelCofork.IsColimit.desc'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
n : Cocone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯) ⟶ W
hn : Cofork.π (CokernelCofork.ofπ (Z := Z) 0 ⋯) ≫ n = w
⊢ 0 = w

Tactic:
rw [Cofork.π_ofπ, zero_comp] at hn

Premises used: CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.Cofork.π_ofπ
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
n : Cocone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯) ⟶ W
hn : 0 = w
⊢ IsIso (X := equalizer u v) (equalizer.ι u v)

Tactic:
apply isIso_limit_cone_parallelPair_of_eq hn.symm hl

Premises used: CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
n : Cocone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯) ⟶ W
hn : 0 = w
⊢ IsIso (X := equalizer u v) (equalizer.ι u v)

Tactic:
have : IsIso (equalizer.ι u v) := by apply isIso_limit_cone_parallelPair_of_eq hn.symm hl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
n : Cocone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯) ⟶ W
hn : 0 = w
this : IsIso (X := equalizer u v) (equalizer.ι u v)
apply : Eq (α := equalizer u v ⟶ Z_1) (equalizer.ι u v ≫ u) (equalizer.ι u v ≫ v)
⊢ u = v

Tactic:
apply (cancel_epi (equalizer.ι u v)).1

Premises used: CategoryTheory.Limits.equalizer.ι, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
n : Cocone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯) ⟶ W
hn : 0 = w
this : IsIso (X := equalizer u v) (equalizer.ι u v)
⊢ Eq (α := equalizer u v ⟶ Z_1) (equalizer.ι u v ≫ u) (equalizer.ι u v ≫ v)

Tactic:
equalizer.condition _ _

Premises used: CategoryTheory.Limits.equalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯)
Z_1 : C
u v : Y ⟶ Z_1
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : Eq (α := equalizer u v ⟶ W) (equalizer.ι u v ≫ w) 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
n : Cocone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := Z) 0 ⋯) ⟶ W
hn : 0 = w
this : IsIso (X := equalizer u v) (equalizer.ι u v)
⊢ Eq (α := equalizer u v ⟶ Z_1) (equalizer.ι u v ≫ u) (equalizer.ι u v ≫ v)

Tactic:
exact equalizer.condition _ _

Premises used: CategoryTheory.Limits.equalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteProducts.{v_1, u_1} C
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : IsNormalMonoCategory.{v_1, u_1} C
inst_5 : HasZeroObject.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0
⊢ Epi f

Tactic:
epi_of_zero_cokernel f 0 <| zeroCokernelOfZeroCancel f hf

Premises used: CategoryTheory.NormalMonoCategory.epi_of_zero_cokernel, CategoryTheory.Limits.zeroCokernelOfZeroCancel, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
rw rw₁ :
  Eq (α := P ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)) (f ≫ cokernel.π (coprod.desc f g))
    (f ≫ cokernel.π (coprod.desc f g))
⊢ Eq (α := P ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)) (f ≫ cokernel.π (coprod.desc f g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl (coprod.desc f g ≫ cokernel.π (coprod.desc f g)))

Tactic:
rw [coprod.inl_desc_assoc]

Premises used: CategoryTheory.Limits.coprod.inl_desc_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
rw rw₁ :
  Eq.{v_1 + 1} (α := P ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl 0)
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl 0)
⊢ Eq (α := P ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl (coprod.desc f g ≫ cokernel.π (coprod.desc f g)))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl 0)

Tactic:
rw [cokernel.condition]

Premises used: CategoryTheory.Limits.cokernel.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
rw rw₁ :
  Eq (α := Q ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)) (g ≫ cokernel.π (coprod.desc f g))
    (g ≫ cokernel.π (coprod.desc f g))
⊢ Eq (α := Q ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)) (g ≫ cokernel.π (coprod.desc f g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr (coprod.desc f g ≫ cokernel.π (coprod.desc f g)))

Tactic:
rw [coprod.inr_desc_assoc]

Premises used: CategoryTheory.Limits.coprod.inr_desc_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
rw rw₁ :
  Eq.{v_1 + 1} (α := Q ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr 0)
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr 0)
⊢ Eq (α := Q ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr (coprod.desc f g ≫ cokernel.π (coprod.desc f g)))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr 0)

Tactic:
rw [cokernel.condition]

Premises used: CategoryTheory.Limits.cokernel.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : a ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : b ≫ b' = cokernel.π (coprod.desc f g)
rw : cokernel.π (coprod.desc f g) = b ≫ b'
rw₁ rw₂ :
  Eq (α := X ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)) (cokernel.π (coprod.desc f g))
    (cokernel.π (coprod.desc f g))
⊢ a ≫ a' = b ≫ b'

Tactic:
rw [ha', hb']
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
rw rw₁ : f ≫ b ≫ s.inr = f ≫ b ≫ s.inr
⊢ CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl (coprod.desc f g ≫ b ≫ s.inr) = f ≫ b ≫ s.inr

Tactic:
rw [coprod.inl_desc_assoc]

Premises used: CategoryTheory.Limits.coprod.inl_desc_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
rw rw₁ : f ≫ b ≫ s.inr = f ≫ b ≫ s.inr
⊢ f ≫ b ≫ s.inr = f ≫ a ≫ s.inl

Tactic:
rw [PushoutCocone.condition]

Premises used: CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
rw : (f ≫ a) ≫ s.inl = 0 ≫ s.inl
rw₁ rw₂ : Eq (α := P ⟶ s.pt) (0 ≫ s.inl) (0 ≫ s.inl)
⊢ f ≫ a ≫ s.inl = 0 ≫ s.inl

Tactic:
rw [← Category.assoc, eq_whisker hfa]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
rw : Eq (α := P ⟶ s.pt) (0 ≫ s.inl) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := P ⟶ s.pt) 0 0
⊢ Eq (α := P ⟶ s.pt) (0 ≫ s.inl) (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inl 0)

Tactic:
rw [comp_zero, zero_comp]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
rw rw₁ : g ≫ b ≫ s.inr = g ≫ b ≫ s.inr
⊢ CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr (coprod.desc f g ≫ b ≫ s.inr) = g ≫ b ≫ s.inr

Tactic:
rw [coprod.inr_desc_assoc]

Premises used: CategoryTheory.Limits.coprod.inr_desc_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
rw : (g ≫ b) ≫ s.inr = 0 ≫ s.inr
rw₁ rw₂ : Eq (α := Q ⟶ s.pt) (0 ≫ s.inr) (0 ≫ s.inr)
⊢ g ≫ b ≫ s.inr = 0 ≫ s.inr

Tactic:
rw [← Category.assoc, eq_whisker hgb]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst_5 : Epi a
inst_6 : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
rw : Eq (α := Q ⟶ s.pt) (0 ≫ s.inr) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := Q ⟶ s.pt) 0 0
⊢ Eq (α := Q ⟶ s.pt) (0 ≫ s.inr) (CategoryStruct.comp (Y := coprod.{v_1, u_1} P Q) coprod.inr 0)

Tactic:
rw [comp_zero, zero_comp]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp