-- Module: Mathlib.Algebra.Homology.Factorizations.CM5b
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) ⋯))
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) ⋯) ⟶
        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) ⋯))
      (β :=
      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) ⋯) ⟶
        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) ⋯))
      (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.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) ⋯)))
      (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) ⋯) ≫
        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) ⋯))
⊢ ∃ (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

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, ?_, ?_, ?_⟩