-- Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean
@[reassoc]
lemma InjectiveResolution.iso_hom_naturality {X Y : C} (f : X ⟶ Y)
    (I : InjectiveResolution X) (J : InjectiveResolution Y)
    (φ : I.cocomplex ⟶ J.cocomplex) (comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0) :
    (injectiveResolutions C).map f ≫ J.iso.hom =
      I.iso.hom ≫ (HomotopyCategory.quotient _ _).map φ

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ Homotopy (desc f (injectiveResolution Y) (injectiveResolution X) ≫ ((injectiveResolution Y).homotopyEquiv J).hom)
    (((injectiveResolution X).homotopyEquiv I).hom ≫ φ)

Tactic:
apply descHomotopy f

Result:
case h.g_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ (injectiveResolution X).ι ≫
      desc f (injectiveResolution Y) (injectiveResolution X) ≫ ((injectiveResolution Y).homotopyEquiv J).hom =
    (CochainComplex.single₀ C).map f ≫ J.ι

case h.h_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ (injectiveResolution X).ι ≫ ((injectiveResolution X).homotopyEquiv I).hom ≫ φ = (CochainComplex.single₀ C).map f ≫ J.ι

Proof state:
case h.g_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ (injectiveResolution X).ι ≫
      desc f (injectiveResolution Y) (injectiveResolution X) ≫ ((injectiveResolution Y).homotopyEquiv J).hom =
    (CochainComplex.single₀ C).map f ≫ J.ι

case h.h_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ (injectiveResolution X).ι ≫ ((injectiveResolution X).homotopyEquiv I).hom ≫ φ = (CochainComplex.single₀ C).map f ≫ J.ι

Tactic:
all_goals aesop

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ (injectiveResolutions C).map f ≫ J.iso.hom = I.iso.hom ≫ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ

Tactic:
apply HomotopyCategory.eq_of_homotopy

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ Homotopy (desc f (injectiveResolution Y) (injectiveResolution X) ≫ ((injectiveResolution Y).homotopyEquiv J).hom)
    (((injectiveResolution X).homotopyEquiv I).hom ≫ φ)

Proof state:
case h.h_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ (injectiveResolution X).ι ≫ ((injectiveResolution X).homotopyEquiv I).hom ≫ φ = (CochainComplex.single₀ C).map f ≫ J.ι

Tactic:
aesop

Result:
no goals