-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
A : CochainComplex.{u_2, u_1, 0} C ℤ
hA : CochainComplex.plus C A
B : CochainComplex.{u_2, u_1, 0} C ℤ
hB : CochainComplex.plus C B
X : CochainComplex.{u_2, u_1, 0} C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex.{u_2, u_1, 0} C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst_2 :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
hi : Mono i
p : X ⟶ Y
inst_3 :
  Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p)
hp : degreewiseEpiWithInjectiveKernel p
hip_1 :
  WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
      (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
    WeakEquivalence (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
      (ObjectProperty.homMk (P := CochainComplex.plus C) p)
t : A ⟶ X
b : B ⟶ Y
sq_1 :
  CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X hX) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
    (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
    (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)
hip : QuasiIso i ∨ QuasiIso p
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this_1 : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq fun (n : ℤ) ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ } (hπ := ⋯) (cokernelIsCokernel i)
    (hι := ⋯) (kernelIsKernel p)
this : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
obtain :
  ∀ (d : ℤ) (hd : X.IsStrictlyGE d)
    [Fibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X ⋯) (Y :=
        ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
        (ObjectProperty.homMk (P := CochainComplex.plus C) p)]
    (hip :
      WeakEquivalence (C := Plus.{u_2, u_1} C) (X :=
          ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (Y :=
          ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB)
          (ObjectProperty.homMk (P := CochainComplex.plus C) i) ∨
        WeakEquivalence (C := Plus.{u_2, u_1} C) (X :=
          ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X ⋯) (Y :=
          ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
          (ObjectProperty.homMk (P := CochainComplex.plus C) p))
    (sq :
      CommSq (C := Plus.{u_2, u_1} C) (W := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) A hA) (X :=
        ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) X ⋯) (Y :=
        ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) B hB) (Z :=
        ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) Y hY)
        (ObjectProperty.homMk (P := CochainComplex.plus C) t) (ObjectProperty.homMk (P := CochainComplex.plus C) i)
        (ObjectProperty.homMk (P := CochainComplex.plus C) p) (ObjectProperty.homMk (P := CochainComplex.plus C) b)),
    (kernel p).IsKInjective
⊢ (kernel p).IsKInjective

Tactic:
obtain ⟨d, hd⟩ := hX