-- 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.fst : 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.fst
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.fst prod.fst :
          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.fst
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.fst)
          (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift c d) prod.fst) :
        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.fst
h₄ :
  CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y)
      (prod.lift a (CategoryStruct.comp (Y := Limits.prod.{v, u} Y Y) (prod.lift c d) prod.fst) :
        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.fst
h₅ :
  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
        (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.fst
h₆ h₇ :
  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 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)
      (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.fst =
    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.fst

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

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