-- Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean
@[reassoc]
lemma ProjectiveResolution.iso_inv_naturality {X Y : C} (f : X ⟶ Y)
    (P : ProjectiveResolution X) (Q : ProjectiveResolution Y)
    (φ : P.complex ⟶ Q.complex) (comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f) :
    P.iso.inv ≫ (projectiveResolutions C).map f =
      (HomotopyCategory.quotient _ _).map φ ≫ Q.iso.inv

Proof state:
case h.g_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ (((projectiveResolution X).homotopyEquiv P).inv ≫ lift f (projectiveResolution X) (projectiveResolution Y)) ≫
      (projectiveResolution Y).π =
    P.π ≫ (ChainComplex.single₀ C).map f

case h.h_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ (φ ≫ ((projectiveResolution Y).homotopyEquiv Q).inv) ≫ (projectiveResolution Y).π =
    P.π ≫ (ChainComplex.single₀ C).map f

Tactic:
all_goals
  aesop_cat

Result:
no goals

Proof state:
case h.h_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ (φ ≫ ((projectiveResolution Y).homotopyEquiv Q).inv) ≫ (projectiveResolution Y).π =
    P.π ≫ (ChainComplex.single₀ C).map f

Tactic:
aesop_cat

Result:
no goals

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ Homotopy (((projectiveResolution X).homotopyEquiv P).inv ≫ lift f (projectiveResolution X) (projectiveResolution Y))
    (φ ≫ ((projectiveResolution Y).homotopyEquiv Q).inv)

Tactic:
apply liftHomotopy f

Result:
case h.g_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ (((projectiveResolution X).homotopyEquiv P).inv ≫ lift f (projectiveResolution X) (projectiveResolution Y)) ≫
      (projectiveResolution Y).π =
    P.π ≫ (ChainComplex.single₀ C).map f

case h.h_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ (φ ≫ ((projectiveResolution Y).homotopyEquiv Q).inv) ≫ (projectiveResolution Y).π =
    P.π ≫ (ChainComplex.single₀ C).map f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ P.iso.inv ≫ (projectiveResolutions C).map f = (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ ≫ Q.iso.inv

Tactic:
apply HomotopyCategory.eq_of_homotopy

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ Homotopy (((projectiveResolution X).homotopyEquiv P).inv ≫ lift f (projectiveResolution X) (projectiveResolution Y))
    (φ ≫ ((projectiveResolution Y).homotopyEquiv Q).inv)