C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ prod.lift a 0 ≫ σ = a
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - 0 = a
rw [sub_def]
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ prod.lift (a ≫ 𝟙 Y) (a ≫ 0) ≫ σ = a
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ prod.lift a 0 ≫ σ = a
conv_lhs =>
  congr; congr; rw [← Category.comp_id a]
  case a.g => rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ prod.lift (a ≫ 𝟙 Y) (a ≫ 0) ≫ σ = a
rw [← prod.comp_lift, Category.assoc, lift_σ, Category.comp_id]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ 0 = a ≫ 0
simp