-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
h₀ :
  (biprod.inl ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
              f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s),
              g := g₁ ≫ g₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.f ≫
          HAdd.hAdd (α :=
            { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₂ ⟶
              biprod.{v_1, u_1}
                { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₁
                { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₁)
            (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.fst =
    (biprod.inl ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
              f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s),
              g := g₁ ≫ g₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁) ≫
      biprod.fst
⊢ { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
          f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
          zero := ⋯ : ShortComplex.{v_1, u_1} C }.f ≫
      HAdd.hAdd (α :=
        { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₂ ⟶
          biprod.{v_1, u_1} { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₁
            { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₁)
        (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr) =
    𝟙
      { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
          f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
          zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁
have h₁ : (biprod.inl ≫
      { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
            f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
            zero := sorry : ShortComplex.{v_1, u_1} C }.f ≫
        HAdd.hAdd (α :=
          { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₂ ⟶
            biprod.{v_1, u_1}
              { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₁
              { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₁)
          (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
    biprod.snd =
  (biprod.inl ≫
      𝟙
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
            f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
            zero := sorry : ShortComplex.{v_1, u_1} C }.X₁) ≫
    biprod.snd
Tactic: ext