case mk
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)) ≫ g = prod.map f f ≫ σ
⊢ σ ≫ f = prod.map f f ≫ σ
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
⊢ σ ≫ f = prod.map f f ≫ σ
obtain ⟨g, hg⟩ :=
  CokernelCofork.IsColimit.desc' isColimitσ (Limits.prod.map f f ≫ σ) (by
    rw [prod.diag_map_assoc, diag_σ, comp_zero])
case mk
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)) ≫ g = prod.map f f ≫ σ
hfg : f = g
⊢ σ ≫ f = prod.map f f ≫ σ

case hfg
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)) ≫ g = prod.map f f ≫ σ
⊢ f = g
case mk
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)) ≫ g = prod.map f f ≫ σ
⊢ σ ≫ f = prod.map f f ≫ σ
suffices hfg : f = g
no goals
case hfg
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)) ≫ g = prod.map f f ≫ σ
⊢ f = g
calc
  f = f ≫ prod.lift (𝟙 Y) 0 ≫ σ := by rw [lift_σ, Category.comp_id]
  _ = prod.lift (𝟙 X) 0 ≫ Limits.prod.map f f ≫ σ := by rw [lift_map_assoc]
  _ = prod.lift (𝟙 X) 0 ≫ σ ≫ g := by rw [← hg, CokernelCofork.π_ofπ]
  _ = g := by rw [← Category.assoc, lift_σ, Category.id_comp]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
⊢ diag X ≫ prod.map f f ≫ σ = 0
rw [prod.diag_map_assoc, diag_σ, comp_zero]
no goals
case mk
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)) ≫ g = prod.map f f ≫ σ
hfg : f = g
⊢ σ ≫ f = prod.map f f ≫ σ
rw [← hg, Cofork.π_ofπ, hfg]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)) ≫ g = prod.map f f ≫ σ
⊢ f = f ≫ prod.lift (𝟙 Y) 0 ≫ σ
rw [lift_σ, Category.comp_id]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)) ≫ g = prod.map f f ≫ σ
⊢ f ≫ prod.lift (𝟙 Y) 0 ≫ σ = prod.lift (𝟙 X) 0 ≫ prod.map f f ≫ σ
rw [lift_map_assoc]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)) ≫ g = prod.map f f ≫ σ
⊢ prod.lift (𝟙 X) 0 ≫ prod.map f f ≫ σ = prod.lift (𝟙 X) 0 ≫ σ ≫ g
rw [← hg, CokernelCofork.π_ofπ]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ (_ : diag X ≫ σ = 0)) ≫ g = prod.map f f ≫ σ
⊢ prod.lift (𝟙 X) 0 ≫ σ ≫ g = g
rw [← Category.assoc, lift_σ, Category.id_comp]