diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
index 8c6f447f1e8bf0..b42c9b10178816 100644
--- a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
+++ b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@@ -759,6 +759,16 @@ lemma δ_ofHom_comp {n : ℤ} (f : F ⟶ G) (z : Cochain G K n) (m : ℤ) :
       (Cochain.ofHom f).comp (δ n m z) (zero_add m) := by
   rw [← Cocycle.ofHom_coe, δ_zero_cocycle_comp]
 
+/-- The precomposition of a cocycle with a morphism of cochain complexes. -/
+@[simps!]
+def Cocycle.precomp {n : ℤ} (z : Cocycle G K n) (f : F ⟶ G) : Cocycle F K n :=
+  Cocycle.mk ((Cochain.ofHom f).comp z (zero_add n)) _ rfl (by simp)
+
+/-- The postcomposition of a cocycle with a morphism of cochain complexes. -/
+@[simps!]
+def Cocycle.postcomp {n : ℤ} (z : Cocycle F G n) (f : G ⟶ K) : Cocycle F K n :=
+  Cocycle.mk (z.1.comp (Cochain.ofHom f) (add_zero n)) _ rfl (by simp)
+
 namespace Cochain
 
 /-- Given two morphisms of complexes `φ₁ φ₂ : F ⟶ G`, the datum of a homotopy between `φ₁` and
diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
index 213c75e406f063..98dd4f969117c5 100644
--- a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
+++ b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@@ -555,6 +555,27 @@ def equivHomShift :
     (K ⟶ L⟦n⟧) ≃+ Cocycle K L n :=
   (equivHom _ _).trans (rightShiftAddEquiv _ _ _ (zero_add n)).symm
 
+lemma equivHomShift_comp {K' : CochainComplex C ℤ}
+    (g : K' ⟶ K) (f : K ⟶ L⟦n⟧) :
+    equivHomShift (g ≫ f) = Cocycle.precomp (equivHomShift f) g := by
+  ext p q hpq
+  simp [equivHomShift_apply, Cochain.rightUnshift_v _ _ _ _ _ _ _ (add_zero p)]
+
+lemma equivHomShift_symm_precomp
+    (z : Cocycle K L n) {K' : CochainComplex C ℤ} (g : K' ⟶ K) :
+    equivHomShift.symm (z.precomp g) = g ≫ equivHomShift.symm z :=
+  equivHomShift.injective (by simp [equivHomShift_comp])
+
+lemma equivHomShift_comp_shift (f : K ⟶ L⟦n⟧) {L' : CochainComplex C ℤ} (g : L ⟶ L') :
+    equivHomShift (f ≫ g⟦n⟧') = Cocycle.postcomp (equivHomShift f) g := by
+  ext p q rfl
+  simp [equivHomShift_apply, Cochain.rightUnshift_v _ _ _ _ _ _ _ (add_zero p)]
+
+lemma equivHomShift_symm_postcomp
+    (z : Cocycle K L n) {L' : CochainComplex C ℤ} (g : L ⟶ L') :
+    equivHomShift.symm (z.postcomp g) = equivHomShift.symm z ≫ g⟦n⟧' :=
+  equivHomShift.injective (by simp [equivHomShift_comp_shift])
+
 /-- The additive equivalence `Cocycle K L n ≃+ Cocycle K⟦a⟧ L n'` when `n + a = n'`. -/
 @[simps]
 def leftShiftAddEquiv (n a n' : ℤ) (hn' : n + a = n') :
diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean
index 2961901e8ae538..9f30a2eea13895 100644
--- a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean
+++ b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexSingle.lean
@@ -82,6 +82,11 @@ noncomputable def fromSingleEquiv {p q n : ℤ} (h : p + n = q) :
   right_inv f := by simp
   map_add' := by simp
 
+@[simp]
+lemma fromSingleEquiv_fromSingleMk {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) :
+    fromSingleEquiv h (fromSingleMk f h) = f := by
+  simp [fromSingleEquiv]
+
 @[simp]
 lemma fromSingleMk_add {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ} (h : p + n = q) :
     fromSingleMk (f + g) h = fromSingleMk f h + fromSingleMk g h :=
@@ -102,6 +107,13 @@ lemma fromSingleMk_surjective {p n : ℤ} (α : Cochain ((singleFunctor C p).obj
     ∃ (f : X ⟶ K.X q), fromSingleMk f h = α :=
   (fromSingleEquiv h).symm.surjective α
 
+lemma fromSingleMk_precomp
+    {X' : C} (g : X' ⟶ X) {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q) :
+    fromSingleMk (g ≫ f) h =
+      (Cochain.ofHom ((singleFunctor C p).map g)).comp (fromSingleMk f h) (zero_add n) := by
+  apply (fromSingleEquiv h).injective
+  simp [fromSingleEquiv, singleFunctor, singleFunctors, HomologicalComplex.single_map_f_self]
+
 /-- Constructor for cochains to a single complex. -/
 @[nolint unusedArguments]
 noncomputable def toSingleMk {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (_ : p + n = q) :
@@ -148,6 +160,11 @@ noncomputable def toSingleEquiv {p q n : ℤ} (h : p + n = q) :
   right_inv f := by simp
   map_add' := by simp
 
+@[simp]
+lemma toSingleEquiv_toSingleMk {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) :
+    toSingleEquiv h (toSingleMk f h) = f := by
+  simp [toSingleEquiv]
+
 @[simp]
 lemma toSingleMk_add {p q : ℤ} (f g : K.X p ⟶ X) {n : ℤ} (h : p + n = q) :
     toSingleMk (f + g) h = toSingleMk f h + toSingleMk g h :=
@@ -168,6 +185,13 @@ lemma toSingleMk_surjective {q n : ℤ} (α : Cochain K ((singleFunctor C q).obj
     ∃ (f : K.X p ⟶ X), toSingleMk f h = α :=
   (toSingleEquiv h).symm.surjective α
 
+lemma toSingleMk_postcomp
+    {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q) {X' : C} (g : X ⟶ X') :
+    toSingleMk (f ≫ g) h =
+      (toSingleMk f h).comp (.ofHom ((singleFunctor C q).map g)) (add_zero n) := by
+  apply (toSingleEquiv h).injective
+  simp [toSingleEquiv, singleFunctor, singleFunctors, HomologicalComplex.single_map_f_self]
+
 end Cochain
 
 namespace Cocycle
@@ -181,6 +205,13 @@ noncomputable def fromSingleMk {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p +
     rw [Cochain.δ_fromSingleMk _ _ _ q' (by lia), hf]
     simp)
 
+lemma fromSingleMk_precomp {X' : C} (g : X' ⟶ X) {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ} (h : p + n = q)
+    (q' : ℤ) (hq' : q + 1 = q') (hf : f ≫ K.d q q' = 0) :
+    fromSingleMk (g ≫ f) h q' hq' (by simp [hf]) =
+      (fromSingleMk f h q' hq' hf).precomp ((singleFunctor C p).map g) := by
+  ext : 1
+  exact (Cochain.fromSingleEquiv h).injective (by simp [Cochain.fromSingleMk_precomp])
+
 lemma fromSingleMk_surjective {p n : ℤ} (α : Cocycle ((singleFunctor C p).obj X) K n)
     (q : ℤ) (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') :
     ∃ (f : X ⟶ K.X q) (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α := by
@@ -238,6 +269,13 @@ noncomputable def toSingleMk {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n
     rw [Cochain.δ_toSingleMk _ _ _ p' (by lia), hf]
     simp)
 
+lemma toSingleMk_postcomp {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ} (h : p + n = q)
+    (p' : ℤ) (hp' : p' + 1 = p) (hf : K.d p' p ≫ f = 0) {X' : C} (g : X ⟶ X') :
+    toSingleMk (f ≫ g) h p' hp' (by simp [reassoc_of% hf]) =
+      (toSingleMk f h p' hp' hf).postcomp ((singleFunctor C q).map g) := by
+  ext : 1
+  exact (Cochain.toSingleEquiv h).injective (by simp [Cochain.toSingleMk_postcomp])
+
 lemma toSingleMk_surjective {q n : ℤ} (α : Cocycle K ((singleFunctor C q).obj X) n)
     (p : ℤ) (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) :
     ∃ (f : K.X p ⟶ X) (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α := by
diff --git a/Mathlib/CategoryTheory/Abelian/Injective/Ext.lean b/Mathlib/CategoryTheory/Abelian/Injective/Ext.lean
index e802ed8bf10893..ef434a7b9ea62f 100644
--- a/Mathlib/CategoryTheory/Abelian/Injective/Ext.lean
+++ b/Mathlib/CategoryTheory/Abelian/Injective/Ext.lean
@@ -20,7 +20,6 @@ we provide an API in order to construct elements in `Ext X Y n` in terms
 of the complex `R.cocomplex` and to make computations in the `Ext`-group.
 
 ## TODO
-* Functoriality in `X` for a given injective resolution `R`
 * Functoriality in `Y`: this would involve a morphism `Y ⟶ Y'`, injective
 resolutions `R` and `R'` of `Y` and `Y'`, a lift of `Y ⟶ Y'` as a morphism
 of cochain complexes `R.cocomplex ⟶ R'.cocomplex`; in this context,
@@ -54,10 +53,17 @@ noncomputable def extEquivCohomologyClass :
 lemma extEquivCohomologyClass_symm_mk_hom [HasDerivedCategory C]
     (x : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex n) :
     (R.extEquivCohomologyClass.symm (.mk x)).hom =
-      (ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
-        (.mk₀ _ rfl (inv (DerivedCategory.Q.map R.ι'))) (zero_add _) := by
+      (ShiftedHom.mk₀ _ rfl ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
+        ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
+        (.mk₀ _ rfl (inv (DerivedCategory.Q.map R.ι') ≫
+          (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) (zero_add _)) (add_zero _) := by
   change SmallShiftedHom.equiv _ _ ((CohomologyClass.mk x).toSmallShiftedHom.comp _ _) = _
-  simp [SmallShiftedHom.equiv_comp, isoOfHom]
+  simp only [SmallShiftedHom.equiv_comp, CohomologyClass.equiv_toSmallShiftedHom_mk,
+    SmallShiftedHom.equiv_mk₀Inv, isoOfHom, asIso_inv, Functor.comp_obj,
+    DerivedCategory.singleFunctorIsoCompQ, Iso.refl_hom, NatTrans.id_app, Iso.refl_inv,
+    ShiftedHom.mk₀_id_comp]
+  congr
+  cat_disch
 
 @[simp]
 lemma extEquivCohomologyClass_symm_add
@@ -200,4 +206,20 @@ lemma extMk_surjective (α : Ext X Y n) (m : ℕ) (hm : n + 1 = m) :
     by simpa [R.cochainComplex_d _ _ _ _ rfl rfl,
       ← cancel_mono (R.cochainComplexXIso m m rfl).inv] using hf, by simp [extMk]⟩
 
+lemma mk₀_comp_extMk {n : ℕ} (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m)
+    (hf : f ≫ R.cocomplex.d n m = 0) {X' : C} (g : X' ⟶ X) :
+    (Ext.mk₀ g).comp (R.extMk f m hm hf) (zero_add _) =
+      R.extMk (g ≫ f) m hm (by simp [hf]) := by
+  have := HasDerivedCategory.standard C
+  ext
+  simp only [extMk, Ext.comp_hom, Int.cast_ofNat_Int, Ext.mk₀_hom,
+    extEquivCohomologyClass_symm_mk_hom, Category.assoc]
+  rw [Cocycle.fromSingleMk_precomp g _ (zero_add _) _ (by lia) (by
+      simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf]),
+    Cocycle.equivHomShift_symm_precomp, ← ShiftedHom.mk₀_comp 0 rfl,
+    ShiftedHom.map_comp,
+    ShiftedHom.comp_assoc _ _ _ (add_zero _) (zero_add _) (by simp),
+    ← ShiftedHom.comp_assoc _ _ _ (add_zero _) (add_zero (n : ℤ)) (by simp)]
+  simp
+
 end CategoryTheory.InjectiveResolution
diff --git a/Mathlib/CategoryTheory/Abelian/Projective/Ext.lean b/Mathlib/CategoryTheory/Abelian/Projective/Ext.lean
index 256179cd70d501..2fcdd31f2986e6 100644
--- a/Mathlib/CategoryTheory/Abelian/Projective/Ext.lean
+++ b/Mathlib/CategoryTheory/Abelian/Projective/Ext.lean
@@ -20,7 +20,6 @@ we provide an API in order to construct elements in `Ext X Y n` in terms
 of the complex `R.complex` and to make computations in the `Ext`-group.
 
 ## TODO
-* Functoriality in `Y` for a given projective resolution `R`
 * Functoriality in `X`: this would involve a morphism `X ⟶ X'`, projective
 resolutions `R` and `R'` of `X` and `X'`, a lift of `X ⟶ X'` as a morphism
 of cochain complexes `R.complex ⟶ R'.complex`; in this context,
@@ -54,10 +53,18 @@ noncomputable def extEquivCohomologyClass :
 lemma extEquivCohomologyClass_symm_mk_hom [HasDerivedCategory C]
     (x : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) n) :
     (R.extEquivCohomologyClass.symm (.mk x)).hom =
-      (ShiftedHom.mk₀ _ rfl (inv (DerivedCategory.Q.map R.π'))).comp
-        (ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q) (add_zero _) := by
+    (ShiftedHom.mk₀ _ rfl ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫
+      inv (DerivedCategory.Q.map R.π'))).comp
+        ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
+          (.mk₀ _ rfl ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
+            (zero_add _)) (add_zero _) := by
   change SmallShiftedHom.equiv _ _ (.comp _ (CohomologyClass.mk x).toSmallShiftedHom _) = _
-  simp [SmallShiftedHom.equiv_comp, isoOfHom]
+  simp only [SmallShiftedHom.equiv_comp, SmallShiftedHom.equiv_mk₀Inv, isoOfHom, asIso_inv,
+    CohomologyClass.equiv_toSmallShiftedHom_mk, Functor.comp_obj,
+    DerivedCategory.singleFunctorIsoCompQ, Iso.refl_hom, NatTrans.id_app, Category.id_comp,
+    Iso.refl_inv]
+  congr
+  exact (ShiftedHom.comp_mk₀_id ..).symm
 
 @[simp]
 lemma extEquivCohomologyClass_symm_add
@@ -200,4 +207,24 @@ lemma extMk_surjective (α : Ext X Y n) (m : ℕ) (hm : n + 1 = m) :
   rw [← cancel_epi (R.cochainComplexXIso (-m) m rfl).hom]
   simpa [R.cochainComplex_d _ _ _ _ rfl rfl] using hf
 
+lemma extMk_comp_mk₀ {n : ℕ} (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m)
+    (hf : R.complex.d m n ≫ f = 0) {Y' : C} (g : Y ⟶ Y') :
+    (R.extMk f m hm hf).comp (Ext.mk₀ g) (add_zero _) =
+      R.extMk (f ≫ g) m hm (by simp [reassoc_of% hf]) := by
+  have := HasDerivedCategory.standard C
+  ext
+  simp only [extMk, Ext.comp_hom, Int.cast_ofNat_Int, Ext.mk₀_hom,
+    extEquivCohomologyClass_symm_mk_hom]
+  simp only [← Category.assoc]
+  rw [Cocycle.toSingleMk_postcomp _ _ _ _
+      (by simpa [cochainComplex_d _ _ _ m n rfl rfl]) g,
+    Cocycle.equivHomShift_symm_postcomp,
+    ← ShiftedHom.comp_mk₀ _ 0 rfl,
+    ShiftedHom.map_comp, ShiftedHom.map_mk₀,
+    ShiftedHom.comp_assoc _ _ _ (add_zero _) (zero_add _) (by simp),
+    ShiftedHom.comp_assoc _ _ _ (zero_add _) (zero_add _) (by simp),
+    ShiftedHom.comp_assoc _ _ _ (zero_add _) (zero_add _) (by simp),
+    ShiftedHom.mk₀_comp_mk₀, ShiftedHom.mk₀_comp_mk₀, ← NatTrans.naturality]
+  dsimp
+
 end CategoryTheory.ProjectiveResolution