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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
huv :
  Eq (α := Y ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) (pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
hvu :
  Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
huu :
  Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
s : Cofork f g
⊢ CategoryStruct.comp (Y := coprod.{v_1, u_1} Y X) coprod.inl (coprod.desc (𝟙 Y) f ≫ s.π) =
    CategoryStruct.comp (Y := coprod.{v_1, u_1} Y X) coprod.inl (coprod.desc (𝟙 Y) g ≫ s.π)

Tactic:
simp only [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 : C
f g : X ⟶ Y
huv :
  Eq (α := Y ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) (pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
hvu :
  Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
huu :
  Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
s : Cofork f g
⊢ CategoryStruct.comp (Y := coprod.{v_1, u_1} Y X) coprod.inr (coprod.desc (𝟙 Y) f ≫ s.π) =
    CategoryStruct.comp (Y := coprod.{v_1, u_1} Y X) coprod.inr (coprod.desc (𝟙 Y) g ≫ s.π)

Tactic:
simp only [coprod.desc_comp, Cofork.condition s]

Premises used: CategoryTheory.Limits.Cofork.condition, CategoryTheory.Limits.coprod.desc_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 : C
f g : X ⟶ Y
huv :
  Eq (α := Y ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) (pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
hvu :
  Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
huu :
  Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
s : Cofork f g
⊢ (Cofork.ofπ (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) huu).π ≫
      (fun (s : Cofork f g) ↦
          (pushout.desc s.π s.π ⋯ :
            pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) ⟶ s.pt))
        s =
    s.π

Tactic:
simp only [pushout.inl_desc, Cofork.π_ofπ]

Premises used: CategoryTheory.Limits.Cofork.π_ofπ, CategoryTheory.Limits.pushout.inl_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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
huv :
  Eq (α := Y ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) (pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
hvu :
  Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
huu :
  Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
s : Cofork f g
m : (Cofork.ofπ (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) huu).pt ⟶ s.pt
h : (Cofork.ofπ (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) huu).π ≫ m = s.π
⊢ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) ≫ m =
    CategoryStruct.comp (Y := pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
      (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
      ((fun (s : Cofork f g) ↦
          (pushout.desc s.π s.π ⋯ :
            pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) ⟶ s.pt))
        s)

Tactic:
simpa only [pushout.inl_desc] using h

Premises used: CategoryTheory.Limits.pushout.inl_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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
huv :
  Eq (α := Y ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) (pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
hvu :
  Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
huu :
  Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
s : Cofork f g
m : (Cofork.ofπ (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) huu).pt ⟶ s.pt
h : (Cofork.ofπ (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) huu).π ≫ m = s.π
⊢ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) ≫ m =
    CategoryStruct.comp (Y := pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
      (pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
      ((fun (s : Cofork f g) ↦
          (pushout.desc s.π s.π ⋯ :
            pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) ⟶ s.pt))
        s)

Tactic:
simpa only [huv.symm, pushout.inl_desc] using h

Premises used: CategoryTheory.Limits.pushout.inl_desc, 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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
⊢ HasCoequalizers.{v_1, u_1} C

Tactic:
hasCoequalizers_of_hasColimit_parallelPair _

Premises used: CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair
-- 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 : C
f : X ⟶ Y
Z : C
⊢ Eq (α := Z ⟶ Y) (0 ≫ f) 0

Tactic:
simp
-- 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 : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
obtain :
  ∀ (W : C) (w : W ⟶ X) (hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0)
    (hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)), u = v
⊢ u = v

Tactic:
obtain ⟨W, w, hw, hl⟩ := normalEpiOfEpi (coequalizer.π u v)

Premises used: CategoryTheory.normalEpiOfEpi, CategoryTheory.Limits.coequalizer.π
-- 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 : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
obtain : ∀ (m : coequalizer u v ⟶ Y) (hm : coequalizer.π u v ≫ m = f), u = v
⊢ u = v

Tactic:
obtain ⟨m, hm⟩ := coequalizer.desc' f huv

Premises used: CategoryTheory.Limits.coequalizer.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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W_1 : C
w : W_1 ⟶ X
hw : Eq (α := W_1 ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
W : C
h : coequalizer u v ⟶ W
rw : (w ≫ coequalizer.π u v) ≫ h = 0 ≫ h
rw₁ rw₂ : Eq (α := W_1 ⟶ W) (0 ≫ h) (0 ≫ h)
⊢ w ≫ coequalizer.π u v ≫ h = 0 ≫ h

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

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 : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
⊢ ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h

Tactic:
have reassoced {W : C} (h : coequalizer u v ⟶ W) : w ≫ coequalizer.π u v ≫ h = 0 ≫ h := by
      rw [← Category.assoc, eq_whisker hw]
-- 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 : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
rw : w ≫ coequalizer.π u v ≫ m = 0
rw₁ : Eq (α := W ⟶ Y) (0 ≫ m) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := W ⟶ Y) 0 0
⊢ w ≫ f = 0

Tactic:
rw [← hm, reassoced, zero_comp]

Premises used: 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 : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
⊢ w ≫ f = 0

Tactic:
have hwf : w ≫ f = 0 := by rw [← hm, reassoced, 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 : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
obtain :
  ∀ (n : W ⟶ Cone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯))
    (hn : n ≫ Fork.ι (KernelFork.ofι (Z := Z) 0 ⋯) = w), u = v
⊢ u = v

Tactic:
obtain ⟨n, hn⟩ := KernelFork.IsLimit.lift' l _ hwf

Premises used: CategoryTheory.Limits.KernelFork.IsLimit.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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
n : W ⟶ Cone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
hn : n ≫ Fork.ι (KernelFork.ofι (Z := Z) 0 ⋯) = w
⊢ 0 = w

Tactic:
rw [Fork.ι_ofι, HasZeroMorphisms.comp_zero] at hn

Premises used: CategoryTheory.Limits.Fork.ι_ofι, CategoryTheory.Limits.HasZeroMorphisms.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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
n : W ⟶ Cone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
hn : 0 = w
⊢ IsIso (Y := coequalizer u v) (coequalizer.π u v)

Tactic:
apply isIso_colimit_cocone_parallelPair_of_eq hn.symm hl

Premises used: CategoryTheory.Limits.isIso_colimit_cocone_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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
n : W ⟶ Cone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
hn : 0 = w
⊢ IsIso (Y := coequalizer u v) (coequalizer.π u v)

Tactic:
have : IsIso (coequalizer.π u v) := by
      apply isIso_colimit_cocone_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 : HasFiniteCoproducts.{v_1, u_1} C
inst_3 : HasCokernels.{v_1, u_1} C
inst_4 : IsNormalEpiCategory.{v_1, u_1} C
X Y : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
n : W ⟶ Cone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
hn : 0 = w
this : IsIso (Y := coequalizer u v) (coequalizer.π u v)
apply : Eq (α := Z_1 ⟶ coequalizer u v) (u ≫ coequalizer.π u v) (v ≫ coequalizer.π u v)
⊢ u = v

Tactic:
apply (cancel_mono (coequalizer.π u v)).1

Premises used: CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.Limits.coequalizer.π
-- 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 : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
n : W ⟶ Cone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
hn : 0 = w
this : IsIso (Y := coequalizer u v) (coequalizer.π u v)
⊢ Eq (α := Z_1 ⟶ coequalizer u v) (u ≫ coequalizer.π u v) (v ≫ coequalizer.π u v)

Tactic:
coequalizer.condition _ _

Premises used: CategoryTheory.Limits.coequalizer.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 : C
f : X ⟶ Y
Z : C
l : IsLimit.{0, v_1, 0, u_1} (C := C) (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
Z_1 : C
u v : Z_1 ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : Eq (α := W ⟶ coequalizer u v) (w ≫ coequalizer.π u v) 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
n : W ⟶ Cone.pt.{0, v_1, 0, u_1} (F := parallelPair f 0) (KernelFork.ofι (Z := Z) 0 ⋯)
hn : 0 = w
this : IsIso (Y := coequalizer u v) (coequalizer.π u v)
⊢ Eq (α := Z_1 ⟶ coequalizer u v) (u ≫ coequalizer.π u v) (v ≫ coequalizer.π u v)

Tactic:
exact coequalizer.condition _ _

Premises used: CategoryTheory.Limits.coequalizer.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
inst_5 : HasZeroObject.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
⊢ Mono f

Tactic:
mono_of_zero_kernel f 0 <| zeroKernelOfCancelZero f hf

Premises used: CategoryTheory.Limits.zeroKernelOfCancelZero, OfNat.ofNat, CategoryTheory.NormalEpiCategory.mono_of_zero_kernel
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasCoequalizers.{v₁, u₁} C
⊢ HasEqualizers.{v₁, u₁} Cᵒᵖ

Tactic:
haveI : HasColimitsOfShape WalkingParallelPairᵒᵖ C :=
    hasColimitsOfShape_of_equivalence walkingParallelPairOpEquiv
  hasLimitsOfShape_op_of_hasColimitsOfShape

Premises used: CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasEqualizers.{v₁, u₁} C
⊢ HasCoequalizers.{v₁, u₁} Cᵒᵖ

Tactic:
haveI : HasLimitsOfShape WalkingParallelPairᵒᵖ C :=
    hasLimitsOfShape_of_equivalence walkingParallelPairOpEquiv
  hasColimitsOfShape_op_of_hasLimitsOfShape

Premises used: CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f_1 g : X ⟶ Y
f : WalkingParallelPair.one ⟶ WalkingParallelPair.zero
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one ⟶
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj WalkingParallelPair.zero)
    (map (parallelPair f_1.op g.op) f ≫
      Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x))
          WalkingParallelPair.zero))
    (Iso.hom
        ((fun (x : WalkingParallelPair) ↦
            (match (motive :=
                (x : WalkingParallelPair) →
                  obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                    (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x)
                x with
              | WalkingParallelPair.zero =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.zero)
              | WalkingParallelPair.one =>
                Iso.refl (obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) WalkingParallelPair.one) :
              obj.{0, v₁, 0, u₁} (parallelPair f_1.op g.op) x ≅
                (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).obj x))
          WalkingParallelPair.one) ≫
      (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f_1 g).op).map f)

Tactic:
cases f