diff --git a/Mathlib/Algebra/Homology/DerivedCategory/TStructure.lean b/Mathlib/Algebra/Homology/DerivedCategory/TStructure.lean
index ae92cb4c519546..085d7772a0baca 100644
--- a/Mathlib/Algebra/Homology/DerivedCategory/TStructure.lean
+++ b/Mathlib/Algebra/Homology/DerivedCategory/TStructure.lean
@@ -76,7 +76,7 @@ noncomputable def TStructure.t : TStructure (DerivedCategory C) where
       rw [id_comp]
       rfl
     · dsimp
-      rw [← Q.map_comp, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE,
+      rw [← Q.map_comp, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE ..,
         Iso.hom_inv_id_assoc]
 
 /-- Given `X : DerivedCategory C` and `n : ℤ`, this property means
diff --git a/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean b/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
index 800a7708629da9..ae06df80b4d34b 100644
--- a/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
+++ b/Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
@@ -431,19 +431,33 @@ lemma shortComplexTruncLE_shortExact (n : ℤ) :
     (K.shortComplexTruncLE n).ShortExact := by
   apply HomologicalComplex.shortComplexTruncLE_shortExact
 
-variable (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁)
+variable (n₀ n₁ : ℤ)
 
 /-- The canonical morphism `(K.shortComplexTruncLE n₀).X₃ ⟶ K.truncGE n₁`. -/
-noncomputable abbrev shortComplexTruncLEX₃ToTruncGE :
+noncomputable abbrev shortComplexTruncLEX₃ToTruncGE (h : n₀ + 1 = n₁ := by lia) :
     (K.shortComplexTruncLE n₀).X₃ ⟶ K.truncGE n₁ :=
   HomologicalComplex.shortComplexTruncLEX₃ToTruncGE K
     (Embedding.embeddingUpInt_areComplementary n₀ n₁ h)
 
 @[reassoc]
-lemma g_shortComplexTruncLEX₃ToTruncGE :
+lemma g_shortComplexTruncLEX₃ToTruncGE (h : n₀ + 1 = n₁ := by lia) :
     (K.shortComplexTruncLE n₀).g ≫ K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h = K.πTruncGE n₁ := by
   apply HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE
 
+lemma injective_opcycles [Injective (K.X n₀)] [Injective (K.X n₁)]
+    [K.IsStrictlyGE n₀] (hK : K.ExactAt n₀) (h : n₀ + 1 = n₁ := by lia) :
+    Injective (K.opcycles n₁) := by
+  let S : ShortComplex C := ShortComplex.mk (K.d n₀ n₁) (K.pOpcycles n₁) (by simp)
+  have : Mono S.f := by
+    let T := K.sc' (n₀ - 1) n₀ n₁
+    have hT : T.Exact := by
+      rwa [← K.exactAt_iff' (n₀ - 1) n₀ n₁ (by simp) (by simpa)]
+    exact hT.mono_g ((K.isZero_of_isStrictlyGE n₀ _).eq_of_src ..)
+  have hS : S.ShortExact :=
+    { exact := S.exact_of_g_is_cokernel (K.opcyclesIsCokernel n₀ n₁ (by simp [← h])) }
+  exact Retract.injective
+    { i := _, r := _, retract := (hS.splittingOfInjective).s_g }
+
 end Abelian
 
 end CochainComplex
diff --git a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
index 30242a2ebf1749..42fd1f3e186362 100644
--- a/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
+++ b/Mathlib/Algebra/Homology/Factorizations/CM5a.lean
@@ -5,10 +5,9 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
+public import Mathlib.Algebra.Homology.DerivedCategory.TStructure
 public import Mathlib.Algebra.Homology.Factorizations.CM5b
 public import Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant
-public import Mathlib.Algebra.Homology.Refinements
 public import Mathlib.Algebra.Homology.SingleHomology
 public import Mathlib.CategoryTheory.Category.Factorisation
 public import Mathlib.CategoryTheory.Functor.OfSequence
@@ -49,6 +48,7 @@ lemma `cm5a_cof`.
 
 -/
 
+
 open CategoryTheory Limits Opposite Abelian HomologicalComplex Pretriangulated
 
 variable {C : Type*} [Category* C] [Abelian C]
@@ -652,4 +652,43 @@ public lemma cm5a (n : ℤ) [K.IsStrictlyGE (n + 1)] [L.IsStrictlyGE n] :
   exact ⟨K', inferInstance, ι, π ≫ p, inferInstance, inferInstance,
     MorphismProperty.comp_mem _ _ _ hπ hp, by simp⟩
 
+open ZeroObject
+
+variable (K)
+
+public lemma exists_mono_quasiIso_injective (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁ := by lia)
+    [K.IsStrictlyGE n₁] :
+    ∃ (L : CochainComplex C ℤ) (i : K ⟶ L) (_hi : Mono i) (_hi' : QuasiIso i)
+      (_ : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n₀ := by
+  have : K.IsStrictlyGE (n₀ + 1) := by rw [h]; infer_instance
+  obtain ⟨L, hL, i, p, hi, hi', hp, _⟩ := cm5a (0 : K ⟶ 0) n₀
+  exact ⟨L, i, hi, hi', (degreewiseEpiWithInjectiveKernel_iff_of_isZero p
+    (Limits.isZero_zero _)).1 hp, hL⟩
+
+public lemma exists_quasiIso_injective (n : ℤ) [K.IsStrictlyGE n] :
+    ∃ (L : CochainComplex C ℤ) (i : K ⟶ L) (_hi' : QuasiIso i)
+      (_hL : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n := by
+  /- The proof proceeds by first applying `exists_mono_quasiIso_injective` in order to
+  obtain a monomorphism `K ⟶ L` that is also a quasi-isomorphism
+  with `L` consisting of injective objects and `L` lying in degrees `≥ n - 1`.
+  Then, as it is quasi-isomorphic to `K`, the cochain complex `L` is cohomologically
+  in degrees `≥ n`, so that the composition `K ⟶ L ⟶ L.truncGE n` is a quasi-isomorphism.
+  In order to conclude, one needs to show that `(L.truncGE n).X n` is injective,
+  i.e. that `L.opcycles n` is injective. -/
+  have : HasDerivedCategory C := MorphismProperty.HasLocalization.standard _
+  obtain ⟨L, i, _, _, hL, _⟩ := exists_mono_quasiIso_injective K (n - 1) n (by simp)
+  have : L.IsGE n := by
+    have hK : K.IsGE n := inferInstance
+    rw [← DerivedCategory.isGE_Q_obj_iff] at hK ⊢
+    exact DerivedCategory.TStructure.t.isGE_of_iso (asIso (DerivedCategory.Q.map i)) n
+  have : QuasiIso (L.πTruncGE n) := (L.quasiIso_πTruncGE_iff n).mpr inferInstance
+  have : Injective (L.opcycles n) :=
+    L.injective_opcycles (n - 1) n (L.exactAt_of_isGE n (n - 1))
+  -- note: this `i ≫ L.πTruncGE n` is a mono in degrees > n, but it may not be in degree n
+  refine ⟨L.truncGE n, i ≫ L.πTruncGE n, inferInstance, fun q ↦ ?_, inferInstance⟩
+  obtain h | rfl | h := lt_trichotomy q n
+  · exact (isZero_of_isStrictlyGE _ n _ h).injective
+  · exact Injective.of_iso (L.truncGEXIsoOpcycles q).symm inferInstance
+  · exact Injective.of_iso (L.truncGEXIso n q h).symm (hL q)
+
 end CochainComplex.Plus.modelCategoryQuillen