Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
          ((ShiftedHom.map
                (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
                DerivedCategory.Q).comp
            (ShiftedHom.mk₀ 0 ⋯
              (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
            ⋯)
          ⋯).comp
      (ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm
              (Cocycle.fromSingleMk ((f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          (inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
        ⋯)
      ⋯

Tactic:
rw [Cocycle.fromSingleMk_postcomp _ (zero_add _) _ (by lia)
      (by simp [R.cochainComplex_d _ _ _ _ rfl rfl, reassoc_of% hf]),
    Cocycle.equivHomShift_symm_postcomp,
    ← ShiftedHom.comp_mk₀ _ 0 rfl, ShiftedHom.map_comp,
    ShiftedHom.comp_assoc _ _ _ _ (zero_add _) (by simp),
    ShiftedHom.comp_assoc _ _ _ _ (zero_add _) (by simp),
    ShiftedHom.comp_assoc _ _ _ _ (zero_add _) (by simp),
    ShiftedHom.map_mk₀, ShiftedHom.mk₀_comp_mk₀, ShiftedHom.mk₀_comp_mk₀]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          ((inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y) ≫
            (DerivedCategory.singleFunctor C 0).map g))
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          (DerivedCategory.Q.map φ.hom' ≫
            inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
        ⋯)
      ⋯