-- 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.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
⊢ 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
have 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
Tactic: rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_snd, prod.lift_snd, prod.lift_snd]