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 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 :
  ∀ (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
⊢ 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

Tactic:
rw [CokernelCofork.π_ofπ] at ha'

Premises used: CategoryTheory.Limits.CokernelCofork.π_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 : 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
rw₁ rw₂ : cokernel.π (coprod.desc f g) ≫ h = cokernel.π (coprod.desc f g) ≫ h
⊢ a ≫ a' ≫ h = cokernel.π (coprod.desc f g) ≫ h

Tactic:
rw [← Category.assoc, eq_whisker ha']

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' : 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

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']
-- 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' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
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
⊢ 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

Tactic:
simp [reassoced, PushoutCocone.condition s]

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 :
  ∀ (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
⊢ 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

Tactic:
rw [CokernelCofork.π_ofπ] at hb'

Premises used: CategoryTheory.Limits.CokernelCofork.π_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 : 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
rw₁ rw₂ : cokernel.π (coprod.desc f g) ≫ h = cokernel.π (coprod.desc f g) ≫ h
⊢ b ≫ b' ≫ h = cokernel.π (coprod.desc f g) ≫ h

Tactic:
rw [← Category.assoc, eq_whisker hb']

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' : 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

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']
-- 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' : b ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
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
⊢ 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

Tactic:
simp [reassoced']
-- 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
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
e_a : cokernel.π (coprod.desc f g) = a ≫ a'
⊢ cokernel.π (coprod.desc f g) ≫ m = (a ≫ a') ≫ m

Tactic:
congr
-- 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
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) = a ≫ a'

Tactic:
ha'.symm

Premises used: Eq.symm, CategoryTheory.Limits.Cofork.π
-- 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
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) = a ≫ a'

Tactic:
exact ha'.symm

Premises used: 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 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
rw₁ rw₂ : a ≫ s.inl = a ≫ s.inl
⊢ (a ≫ a') ≫ m = a ≫ s.inl

Tactic:
rw [Category.assoc, h₁]

Premises used: CategoryTheory.Category.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
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 rw₁ : b ≫ s.inr = b ≫ 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) ⋯)

Tactic:
rw [cokernel.π_desc]

Premises used: CategoryTheory.Limits.cokernel.π_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
rw 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))
⊢ 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))

Tactic:
rw [coprod.inl_desc]

Premises used: CategoryTheory.Limits.coprod.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
⊢ 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) f) ≫
      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) g) ≫
      pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))

Tactic:
simp only [Category.assoc, pushout.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pushout.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 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))
rw₁ 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))
⊢ 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))

Tactic:
rw [coprod.inl_desc, Category.id_comp]

Premises used: CategoryTheory.Limits.coprod.inl_desc, CategoryTheory.Category.id_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))
rw 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))
⊢ 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))

Tactic:
rw [coprod.inr_desc]

Premises used: CategoryTheory.Limits.coprod.inr_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))
⊢ 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) 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) g) ≫
      pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g))

Tactic:
simp only [Category.assoc, pushout.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pushout.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 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))
rw 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))
⊢ 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))

Tactic:
rw [coprod.inr_desc]

Premises used: CategoryTheory.Limits.coprod.inr_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))
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))
rw₁ 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))
⊢ 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))

Tactic:
rw [hvu, huv]