-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem σ_comp {X Y : C} (f : X ⟶ Y) : σ ≫ f = Limits.prod.map f f ≫ σ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
⊢ f ≫ prod.lift (𝟙 Y) 0 ≫ σ = prod.lift (𝟙 X) 0 ≫ prod.map f f ≫ σ

Tactic:
rw [lift_map_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
hfg : f = g
⊢ σ ≫ f = prod.map f f ≫ σ

Tactic:
rw [← hg, Cofork.π_ofπ, hfg]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
⊢ prod.lift (𝟙 X) 0 ≫ prod.map f f ≫ σ = prod.lift (𝟙 X) 0 ≫ σ ≫ g

Tactic:
rw [← hg, CokernelCofork.π_ofπ]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
⊢ f = f ≫ prod.lift (𝟙 Y) 0 ≫ σ

Tactic:
rw [lift_σ, Category.comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
⊢ σ ≫ f = prod.map f f ≫ σ

Tactic:
obtain ⟨g, hg⟩ :=
  CokernelCofork.IsColimit.desc' isColimitσ (Limits.prod.map f f ≫ σ) (by
    rw [prod.diag_map_assoc, diag_σ, comp_zero])

Result:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
⊢ σ ≫ f = prod.map f f ≫ σ

Proof state:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
⊢ f = g

Tactic:
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]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
⊢ diag X ≫ prod.map f f ≫ σ = 0

Tactic:
rw [prod.diag_map_assoc, diag_σ, comp_zero]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
⊢ prod.lift (𝟙 X) 0 ≫ σ ≫ g = g

Tactic:
rw [← Category.assoc, lift_σ, Category.id_comp]

Result:
no goals

Proof state:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
⊢ σ ≫ f = prod.map f f ≫ σ

Tactic:
suffices hfg : f = g by rw [← hg, Cofork.π_ofπ, hfg]

Result:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
⊢ f = g