awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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
⊢ a ≫
      a' ≫
        (fun (s : PushoutCocone a b) ↦
            (cokernel.desc (coprod.desc f g) (b ≫ s.inr) ⋯ :
              cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ s.pt))
          s =
    a ≫ s.inl
have rw : ∀ (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' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)) (s : PushoutCocone a b),
  a ≫
      a' ≫
        (fun (s : PushoutCocone a b) ↦
            (cokernel.desc (coprod.desc f g) (b ≫ s.inr) sorry :
              cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ s.pt))
          s =
    a ≫ s.inl
Tactic: rw [CokernelCofork.π_ofπ] at ha'
Cleared hypotheses: ha', b', hb', s
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
W : C
h : cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ W
⊢ a ≫ a' ≫ h = cokernel.π (coprod.desc f g) ≫ h
have rw : (a ≫ a') ≫ h = cokernel.π (coprod.desc f g) ≫ h
Tactic: rw [← Category.assoc, eq_whisker ha']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
W : C
h : cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ W
rw : (a ≫ a') ≫ h = cokernel.π (coprod.desc f g) ≫ h
⊢ a ≫ a' ≫ h = cokernel.π (coprod.desc f g) ≫ h
have rw₁ : cokernel.π (coprod.desc f g) ≫ h = cokernel.π (coprod.desc f g) ≫ h
Tactic: rw [← Category.assoc, eq_whisker ha']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (hypothesis)
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' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ a ≫
      a' ≫
        (fun (s : PushoutCocone a b) ↦
            (cokernel.desc (coprod.desc f g) (b ≫ s.inr) ⋯ :
              cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ s.pt))
          s =
    a ≫ s.inl
have reassoced : ∀ {W : C} (h : cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ W),
  a ≫ a' ≫ h = cokernel.π (coprod.desc f g) ≫ h
Tactic: have reassoced {W : C} (h : cokernel (coprod.desc f g) ⟶ W) : a ≫ a' ≫ h
                = cokernel.π (coprod.desc f g) ≫ h := by rw [← Category.assoc, eq_whisker ha']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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
⊢ b ≫
      b' ≫
        (fun (s : PushoutCocone a b) ↦
            (cokernel.desc (coprod.desc f g) (b ≫ s.inr) ⋯ :
              cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ s.pt))
          s =
    b ≫ s.inr
have rw : ∀ (hb' : b ≫ b' = cokernel.π (coprod.desc f g)) (s : PushoutCocone a b),
  b ≫
      b' ≫
        (fun (s : PushoutCocone a b) ↦
            (cokernel.desc (coprod.desc f g) (b ≫ s.inr) sorry :
              cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ s.pt))
          s =
    b ≫ s.inr
Tactic: rw [CokernelCofork.π_ofπ] at hb'
Cleared hypotheses: hb', s
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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' : b ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
W : C
h : cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ W
⊢ b ≫ b' ≫ h = cokernel.π (coprod.desc f g) ≫ h
have rw : (b ≫ b') ≫ h = cokernel.π (coprod.desc f g) ≫ h
Tactic: rw [← Category.assoc, eq_whisker hb']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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' : b ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
W : C
h : cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ W
rw : (b ≫ b') ≫ h = cokernel.π (coprod.desc f g) ≫ h
⊢ b ≫ b' ≫ h = cokernel.π (coprod.desc f g) ≫ h
have rw₁ : cokernel.π (coprod.desc f g) ≫ h = cokernel.π (coprod.desc f g) ≫ h
Tactic: rw [← Category.assoc, eq_whisker hb']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (hypothesis)
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' : b ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ b ≫
      b' ≫
        (fun (s : PushoutCocone a b) ↦
            (cokernel.desc (coprod.desc f g) (b ≫ s.inr) ⋯ :
              cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ s.pt))
          s =
    b ≫ s.inr
have reassoced' : ∀ {W : C} (h : cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ W),
  b ≫ b' ≫ h = cokernel.π (coprod.desc f g) ≫ h
Tactic: have reassoced' {W : C} (h : cokernel (coprod.desc f g) ⟶ W) : b ≫ b' ≫ h
                = cokernel.π (coprod.desc f g) ≫ h := by rw [← Category.assoc, eq_whisker hb']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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
m : cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ s.pt
h₁ : a' ≫ m = s.inl
h : b' ≫ m = s.inr
⊢ cokernel.π (coprod.desc f g) ≫ m = (a ≫ a') ≫ m
have e_a : cokernel.π (coprod.desc f g) = a ≫ a'
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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
m : cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ s.pt
h₁ : a' ≫ m = s.inl
h : b' ≫ m = s.inr
⊢ (a ≫ a') ≫ m = a ≫ s.inl
have rw : a ≫ a' ≫ m = a ≫ s.inl
Tactic: rw [Category.assoc, h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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
m : cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ s.pt
h₁ : a' ≫ m = s.inl
h : b' ≫ m = s.inr
rw : a ≫ a' ≫ m = a ≫ s.inl
⊢ (a ≫ a') ≫ m = a ≫ s.inl
have rw₁ : a ≫ s.inl = a ≫ s.inl
Tactic: rw [Category.assoc, h₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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
m : cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g) ⟶ s.pt
h₁ : a' ≫ m = s.inl
h : b' ≫ m = s.inr
⊢ b ≫ s.inr =
    CategoryStruct.comp (Y := cokernel (X := coprod.{v_1, u_1} P Q) (coprod.desc f g)) (cokernel.π (coprod.desc f g))
      (cokernel.desc (coprod.desc f g) (b ≫ s.inr) ⋯)
have rw : b ≫ s.inr = b ≫ s.inr
Tactic: rw [cokernel.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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
⊢ Eq (α := Y ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (𝟙 Y ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} Y X) coprod.inl (coprod.desc (𝟙 Y) f) ≫
      pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
have rw : Eq (α := Y ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
  (𝟙 Y ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
  (𝟙 Y ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
Tactic: rw [coprod.inl_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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
⊢ Eq (α := Y ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} Y X) coprod.inl (coprod.desc (𝟙 Y) g) ≫
      pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
have rw : Eq (α := Y ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
  (𝟙 Y ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
  (pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
Tactic: rw [coprod.inl_desc, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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
rw :
  Eq (α := Y ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (𝟙 Y ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
⊢ Eq (α := Y ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} Y X) coprod.inl (coprod.desc (𝟙 Y) g) ≫
      pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
have rw₁ : Eq (α := 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)) (pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
Tactic: rw [coprod.inl_desc, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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))
⊢ 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))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} Y X) coprod.inr (coprod.desc (𝟙 Y) f) ≫
      pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
have rw : 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))
  (f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
Tactic: rw [coprod.inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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))
⊢ Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (CategoryStruct.comp (Y := coprod.{v_1, u_1} Y X) coprod.inr (coprod.desc (𝟙 Y) g) ≫
      pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
have rw : Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
  (g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
  (g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
Tactic: rw [coprod.inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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))
⊢ 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))
have rw : Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
  (g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
  (g ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
Tactic: rw [hvu, huv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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))
rw :
  Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
    (g ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
⊢ 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))
have rw₁ : Eq (α := X ⟶ pushout (X := coprod.{v_1, u_1} Y X) (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
  (g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
  (g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))
Tactic: rw [hvu, huv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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
⊢ u = v
have 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
Tactic: obtain ⟨W, w, hw, hl⟩ := normalEpiOfEpi (coequalizer.π u v)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers (goal)
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)
⊢ u = v
have obtain : ∀ (m : coequalizer u v ⟶ Y) (hm : coequalizer.π u v ≫ m = f), u = v
Tactic: obtain ⟨m, hm⟩ := coequalizer.desc' f huv