-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
refine_1 :
  Eq (α := (mappingCone (𝟙 (I K))).X n ⟶ L.X n)
    (CategoryStruct.comp (Y := (mappingCone (𝟙 (I K)) ⊞ L).X n) (HomologicalComplex.Hom.f biprod.inl n)
      (HomologicalComplex.Hom.f (p K L) n))
    0
refine_2 :
  ShortComplex.f
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯) ≫
      HomologicalComplex.Hom.f biprod.fst n =
    𝟙
      (ShortComplex.X₁
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯))
refine_3 :
  CategoryStruct.comp (Y :=
      ShortComplex.X₂
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯))
      (HomologicalComplex.Hom.f biprod.inr n)
      (ShortComplex.g
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯)) =
    𝟙
      (ShortComplex.X₃
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯))
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n) (w :
    f ≫ HomologicalComplex.Hom.f (p K L) n = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n, X₃ := L.X n, f := f,
          g := HomologicalComplex.Hom.f (p K L) n, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
have refine_4 : HAdd.hAdd (α :=
    ShortComplex.X₂
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry) ⟶
      ShortComplex.X₂
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry))
    (β :=
    ShortComplex.X₂
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry) ⟶
      ShortComplex.X₂
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry))
    (CategoryStruct.comp (Y :=
      ShortComplex.X₁
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry))
      (HomologicalComplex.Hom.f biprod.fst n : (mappingCone (𝟙 (I K)) ⊞ L).X n ⟶ (mappingCone (𝟙 (I K))).X n)
      (ShortComplex.f
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry)))
    (ShortComplex.g
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry) ≫
      HomologicalComplex.Hom.f biprod.inr n) =
  𝟙
    (ShortComplex.X₂
      (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
        (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry))
Tactic: refine ⟨(mappingCone (𝟙 (I K))).X n, inferInstance,
    (biprod.inl :_ ⟶ (mappingCone (𝟙 (I K))) ⊞ L).f n, ?_,
    (biprod.fst : (mappingCone (𝟙 (I K))) ⊞ L ⟶ _).f n,
    (biprod.inr :_ ⟶ (mappingCone (𝟙 (I K))) ⊞ L).f n, ?_, ?_, ?_⟩