Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A B X Y : Plus C
i : A ⟶ B
p : X ⟶ Y
inst✝¹ : Mono i
inst✝ : Fibration p
hip : WeakEquivalence i ∨ WeakEquivalence p
t : A ⟶ X
b : B ⟶ Y
sq : CommSq t i p b
⊢ sq.HasLift

Tactic:
by
    /- The proof is similar in both cases (whether `i` or `p` is a quasi-isomorphism).
    We first transform the variables so as to get a commutative square in `CochainComplex C ℤ`
    instead of the full subcategory `CochainComplex.Plus C`. -/
    obtain ⟨A, hA⟩ := A
    obtain ⟨B, hB⟩ := B
    obtain ⟨X, hX⟩ := X
    obtain ⟨Y, hY⟩ := Y
    have hi : Mono i.hom := inferInstance
    have hp : degreewiseEpiWithInjectiveKernel p.hom :=
      (fibration_iff p).1 inferInstance
    obtain ⟨i, rfl⟩ := ObjectProperty.homMk_surjective i
    obtain ⟨p, rfl⟩ := ObjectProperty.homMk_surjective p
    obtain ⟨t, rfl⟩ := ObjectProperty.homMk_surjective t
    obtain ⟨b, rfl⟩ := ObjectProperty.homMk_surjective b
    dsimp at i p t b hp hi
    have hip : QuasiIso i ∨ QuasiIso p := by
      simpa only [weakEquivalence_iff] using! hip
    replace sq : CommSq t i p b := sq.map (ObjectProperty.ι _)
    suffices sq.HasLift from ⟨⟨{ l := ObjectProperty.homMk sq.lift }⟩⟩
    have sq' (n : ℤ) : CommSq (t.f n) (i.f n) (p.f n) (b.f n) :=
      (sq.map (HomologicalComplex.eval _ _ n))
    /- The commutative square in `C` obtained by evaluating in a degree `n`
    admits a lifting because `i.f n` is a monomorphism and `p.f n` is
    an epimorphism with injective kernel. -/
    have (n : ℤ) : (sq' n).HasLift := by
      have := (hp n).hasLiftingProperty (i.f n)
      infer_instance
    /- In order to obtain a lifting in the original square, the obstruction
    lies in a cocycle `β : Cocycle (cokernel i) (kernel p) 1`. Thanks to the
    lemma `CochainComplex.Lifting.hasLift`, it suffices to show that `β`
    is a coboundary. -/
    let β : Cocycle (cokernel i) (kernel p) 1 :=
      Lifting.cocycle₁ sq (fun n ↦ { l := (sq' n).lift })
        (cokernelIsCokernel i) (kernelIsKernel p) (hπ := by simp) (hι := by simp)
    have (n : ℤ) : Injective ((kernel p).X n) :=
      Injective.of_iso
        (asIso (kernelComparison p (HomologicalComplex.eval _ _ n))).symm (hp n).2
    have : (kernel p).IsKInjective := by
      obtain ⟨d, hd⟩ := hX
      have : (kernel p).IsStrictlyGE d := by
        rw [isStrictlyGE_iff]
        intro i hi
        rw [IsZero.iff_id_eq_zero, ← cancel_mono ((kernel.ι p).f i)]
        apply (X.isZero_of_isStrictlyGE d i).eq_of_tgt
      exact isKInjective_of_injective _ d
    /- The cocycle `β` is a coboundary when `i` or `p` is a quasi-isomorphism. -/
    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)
    exact Lifting.hasLift sq _ (cokernelIsCokernel _) (kernelIsKernel _) α hα

Goal state after: