-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
X Y : C
a b c d : X ⟶ Y
h₂ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
      (prod.lift (prod.lift a b) (prod.lift c d) :
        X ⟶ Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
      (σ ≫ prod.snd : Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y) ⟶ Y) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
      (prod.lift
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a c : X ⟶ Limits.prod.{v, u} Y Y)
          (σ : Limits.prod.{v, u} Y Y ⟶ Y))
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
          (σ : Limits.prod.{v, u} Y Y ⟶ Y)))
      prod.snd
h₃ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
      (prod.lift (prod.lift a b) (prod.lift c d))
      (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
        (prod.map prod.snd prod.snd :
          Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y) ⟶ Limits.prod.{v, u} Y Y)
        (σ : Limits.prod.{v, u} Y Y ⟶ Y)) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
      (prod.lift
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a c : X ⟶ Limits.prod.{v, u} Y Y)
          (σ : Limits.prod.{v, u} Y Y ⟶ Y))
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
          (σ : Limits.prod.{v, u} Y Y ⟶ Y)))
      prod.snd
h₄ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
      (prod.lift (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a b) prod.snd)
          (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift c d) prod.snd) :
        X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
      (prod.lift
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a c : X ⟶ Limits.prod.{v, u} Y Y)
          (σ : Limits.prod.{v, u} Y Y ⟶ Y))
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
          (σ : Limits.prod.{v, u} Y Y ⟶ Y)))
      prod.snd
h₅ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
      (prod.lift b (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift c d) prod.snd) :
        X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
      (prod.lift
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a c : X ⟶ Limits.prod.{v, u} Y Y)
          (σ : Limits.prod.{v, u} Y Y ⟶ Y))
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
          (σ : Limits.prod.{v, u} Y Y ⟶ Y)))
      prod.snd
h₆ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
      (prod.lift
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a c : X ⟶ Limits.prod.{v, u} Y Y)
          (σ : Limits.prod.{v, u} Y Y ⟶ Y))
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
          (σ : Limits.prod.{v, u} Y Y ⟶ Y)))
      prod.snd
h₇ h₈ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y) =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
      (σ : Limits.prod.{v, u} Y Y ⟶ Y)
⊢ CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
      (CategoryStruct.comp (Y := Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
        (prod.lift (prod.lift a b) (prod.lift c d) :
          X ⟶ Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y))
        (σ : Limits.prod.{v, u} (Limits.prod.{v, u} Y Y) (Limits.prod.{v, u} Y Y) ⟶ Limits.prod.{v, u} Y Y))
      prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
      (prod.lift
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift a c : X ⟶ Limits.prod.{v, u} Y Y)
          (σ : Limits.prod.{v, u} Y Y ⟶ Y))
        (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift b d : X ⟶ Limits.prod.{v, u} Y Y)
          (σ : Limits.prod.{v, u} Y Y ⟶ Y)))
      prod.snd

Tactic:
rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_snd, prod.lift_snd, prod.lift_snd]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NonPreadditiveAbelian.σ_comp, CategoryTheory.Limits.prod.lift_map_assoc, CategoryTheory.Limits.prod.lift_snd