C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b) (prod.lift c d) ≫ σ = prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ)
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift a b - prod.lift c d = prod.lift (a - c) (b - d)
simp only [sub_def]
case h₁
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ prod.fst =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.fst

case h₂
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ prod.snd =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.snd
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b) (prod.lift c d) ≫ σ = prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ)
apply prod.hom_ext
no goals
case h₁
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ prod.fst =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.fst
rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_fst, prod.lift_fst, prod.lift_fst]
no goals
case h₂
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ prod.snd =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.snd
rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_snd, prod.lift_snd, prod.lift_snd]