Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
h₂ :
  (P.isoLeftDerivedToHomotopyCategoryObj F).inv =
    (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
      (lift (𝟙 X) P (projectiveResolution X))
h₁ :
  HomologicalComplex.opcyclesMap
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) 0 ≫
      (projectiveResolution X).fromLeftDerivedZero' F =
    P.fromLeftDerivedZero' F
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (P.isoLeftDerivedToHomotopyCategoryObj F).inv ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as).homologyι 0 ≫
          (projectiveResolution X).fromLeftDerivedZero' F =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map
        ((P.isoLeftDerivedToHomotopyCategoryObj F).inv ≫ (P.isoLeftDerivedToHomotopyCategoryObj F).hom) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).homologyι 0 ≫ P.fromLeftDerivedZero' F

Tactic:
Iso.inv_hom_id,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
h₂ :
  (P.isoLeftDerivedToHomotopyCategoryObj F).inv =
    (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
      (lift (𝟙 X) P (projectiveResolution X))
h₁ :
  HomologicalComplex.opcyclesMap
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) 0 ≫
      (projectiveResolution X).fromLeftDerivedZero' F =
    P.fromLeftDerivedZero' F
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (P.isoLeftDerivedToHomotopyCategoryObj F).inv ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as).homologyι 0 ≫
          (projectiveResolution X).fromLeftDerivedZero' F =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map
        (𝟙
          ((F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
            P.complex)) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).homologyι 0 ≫ P.fromLeftDerivedZero' F