-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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_2 : ∀ (n : ℤ), Injective.{u_2, u_1} ((kernel p).X n)
this : (kernel p).IsKInjective
⊢ sq.HasLift
have obtain : ∀ (α : Cochain (cokernel i) (kernel p) 0) (hα : δ 0 1 α = (↑β : Cochain (cokernel i) (kernel p) 1)), sq.HasLift
Tactic: obtain ⟨α, hα⟩ : ∃ (α : Cochain (cokernel i) (kernel p) 0), δ 0 1 α = β.1 := by
      cases hip
      · refine IsKInjective.eq_δ_of_cocycle β ?_ 0 (by simp)
        have : (ShortComplex.mk _ _ (cokernel.condition i)).ShortExact :=
          { exact := ShortComplex.exact_cokernel i }
        exact this.acyclic_X₃ (by dsimp; infer_instance)
      · refine IsKInjective.eq_δ_of_cocycle' β ?_ 0 (by simp)
        have := hp.epi
        have : (ShortComplex.mk _ _ (kernel.condition p)).ShortExact :=
          { exact := ShortComplex.exact_kernel p }
        exact this.acyclic_X₁ (by dsimp; infer_instance)