-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
rw :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f) (Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
      (Functor.map (injectiveResolutions C) f ≫ Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₂ :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
      (Iso.hom I.iso ≫ Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₃ :
  Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₄ :
  Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ =
    Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫
      CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y) (Iso.inv J.iso) (Iso.hom J.iso)
rw₅ :
  Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ =
    Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫
      𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) J.cocomplex)
rw₆ rw₇ :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) J.cocomplex)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex ⟶ Functor.obj (injectiveResolutions C) Y)
    (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso)

Tactic:
rw [← cancel_mono (J.iso).hom, Category.assoc, iso_hom_naturality f I J φ comm,
    Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.InjectiveResolution.iso_hom_naturality, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.InjectiveResolution.iso, CategoryTheory.Iso.hom