-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
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
⊢ 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
have 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
Tactic: rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_fst, prod.lift_fst, prod.lift_fst]