[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (leftDerived F n).map f =
    (leftDerivedObjIso F n P).hom ≫
      (homologyFunctor D (ComplexShape.down ℕ) n).map ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) ≫
        (leftDerivedObjIso F n Q).inv
[PROOFSTEP]
dsimp only [Functor.leftDerived, Functor.leftDerivedObjIso]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (projectiveResolutions C ⋙
          mapHomotopyCategory F (ComplexShape.down ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      f =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).mapIso
            (HomotopyCategory.isoOfHomotopyEquiv
              (mapHomotopyEquiv F (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P))) ≪≫
          (HomotopyCategory.homologyFactors D (ComplexShape.down ℕ) n).app
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)).hom ≫
      (homologyFunctor D (ComplexShape.down ℕ) n).map ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) ≫
        ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).mapIso
              (HomotopyCategory.isoOfHomotopyEquiv
                (mapHomotopyEquiv F (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q))) ≪≫
            (HomotopyCategory.homologyFactors D (ComplexShape.down ℕ) n).app
              ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex)).inv
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.down ℕ)).map ((projectiveResolutions C).map f)) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom)) ≫
        𝟙
          ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).obj
            ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
              ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)))) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) n =
              0)
          (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n)
          (HomologicalComplex.Hom.sqFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n)
          (_ :
            (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n).right =
              (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n).right) ≫
        𝟙 (HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) n) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
            ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
              ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
                (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv))
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.down ℕ)).map ((projectiveResolutions C).map f)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
            (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom)) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) n =
              0)
          (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n)
          (HomologicalComplex.Hom.sqFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n)
          (_ :
            (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n).right =
              (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g) n).right) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv))
[PROOFSTEP]
rw [← homologyFunctor_map, HomotopyCategory.homologyFunctor_map_factors]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.down ℕ)).map ((projectiveResolutions C).map f)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
            (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom)) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).map g)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv))
[PROOFSTEP]
simp only [← Functor.map_comp]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.down ℕ)).map ((projectiveResolutions C).map f)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
          ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
            g ≫ (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv)))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (mapHomotopyCategory F (ComplexShape.down ℕ)).map ((projectiveResolutions C).map f) =
    (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
      ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
        ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
          g ≫ (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv))
[PROOFSTEP]
apply HomotopyCategory.eq_of_homotopy
[GOAL]
case e_a.h
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ Homotopy ((mapHomologicalComplex F (ComplexShape.down ℕ)).map (projectiveResolution.lift f))
    ((mapHomologicalComplex F (ComplexShape.down ℕ)).map
      ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
        g ≫ (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv))
[PROOFSTEP]
apply Functor.mapHomotopy
[GOAL]
case e_a.h.h
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ Homotopy (projectiveResolution.lift f)
    ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
      g ≫ (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv)
[PROOFSTEP]
apply ProjectiveResolution.liftHomotopy f
[GOAL]
case e_a.h.h.g_comm
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ projectiveResolution.lift f ≫ (projectiveResolution Y).π = (projectiveResolution X).π ≫ (ChainComplex.single₀ C).map f
[PROOFSTEP]
simp
[GOAL]
case e_a.h.h.h_comm
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
        g ≫ (ProjectiveResolution.homotopyEquiv (projectiveResolution Y) Q).inv) ≫
      (projectiveResolution Y).π =
    (projectiveResolution X).π ≫ (ChainComplex.single₀ C).map f
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Functor.Additive F
n : ℕ
⊢ leftDerived (𝟙 F) n = 𝟙 (Functor.leftDerived F n)
[PROOFSTEP]
simp [NatTrans.leftDerived]
[GOAL]
C : Type u
inst✝¹² : Category.{v, u} C
D : Type u_1
inst✝¹¹ : Category.{u_2, u_1} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Functor.Additive F
n : ℕ
⊢ 𝟙
      (projectiveResolutions C ⋙
        Functor.mapHomotopyCategory F (ComplexShape.down ℕ) ⋙
          HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) =
    𝟙 (Functor.leftDerived F n)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹⁴ : Category.{v, u} C
D : Type u_1
inst✝¹³ : Category.{u_2, u_1} D
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasEqualizers C
inst✝⁹ : HasImages C
inst✝⁸ : HasProjectiveResolutions C
inst✝⁷ : Preadditive D
inst✝⁶ : HasEqualizers D
inst✝⁵ : HasCokernels D
inst✝⁴ : HasImages D
inst✝³ : HasImageMaps D
F G H : C ⥤ D
inst✝² : Functor.Additive F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Additive H
α : F ⟶ G
β : G ⟶ H
n : ℕ
⊢ leftDerived (α ≫ β) n = leftDerived α n ≫ leftDerived β n
[PROOFSTEP]
simp [NatTrans.leftDerived]
[GOAL]
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ app (leftDerived α n) X =
    (Functor.leftDerivedObjIso F n P).hom ≫
      (homologyFunctor D (ComplexShape.down ℕ) n).map (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) ≫
        (Functor.leftDerivedObjIso G n P).inv
[PROOFSTEP]
symm
[GOAL]
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ (Functor.leftDerivedObjIso F n P).hom ≫
      (homologyFunctor D (ComplexShape.down ℕ) n).map (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) ≫
        (Functor.leftDerivedObjIso G n P).inv =
    app (leftDerived α n) X
[PROOFSTEP]
dsimp [NatTrans.leftDerived, Functor.leftDerivedObjIso]
[GOAL]
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom)) ≫
        𝟙
          ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).obj
            ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
              ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)))) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n ≫
                HomologicalComplex.dFrom ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj P.complex) n ≫
                HomologicalComplex.dFrom ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj P.complex) n =
              0)
          (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n)
          (HomologicalComplex.Hom.sqFrom (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n)
          (_ :
            (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n).right =
              (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n).right) ≫
        𝟙 (HomologicalComplex.homology ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj P.complex) n) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
            ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
              ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
                (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as))
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp]
[GOAL]
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map
            (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom)) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n ≫
                HomologicalComplex.dFrom ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj P.complex) n ≫
                HomologicalComplex.dFrom ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj P.complex) n =
              0)
          (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n)
          (HomologicalComplex.Hom.sqFrom (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n)
          (_ :
            (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n).right =
              (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) n).right) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as))
[PROOFSTEP]
rw [← homologyFunctor_map, HomotopyCategory.homologyFunctor_map_factors]
[GOAL]
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map
            (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom)) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            (app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as))
[PROOFSTEP]
simp only [← Functor.map_comp]
[GOAL]
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map
            (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
          app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex ≫
            (Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
              (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
      ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map
          (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
        app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex ≫
          (Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
            (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv) =
    (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
      (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as)
[PROOFSTEP]
apply HomotopyCategory.eq_of_homotopy
[GOAL]
case e_a.h
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ Homotopy
    ((Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map
        (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
      app (mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex ≫
        (Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
          (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv)
    (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as)
[PROOFSTEP]
simp only [NatTrans.mapHomologicalComplex_naturality_assoc, ← Functor.map_comp]
[GOAL]
case e_a.h
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ Homotopy
    (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as ≫
      (Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
        ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
          (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv))
    (app (mapHomologicalComplex α (ComplexShape.down ℕ)) ((projectiveResolutions C).obj X).as)
[PROOFSTEP]
apply Homotopy.compLeftId
[GOAL]
case e_a.h.h
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ Homotopy
    ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map
      ((ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).hom ≫
        (ProjectiveResolution.homotopyEquiv (projectiveResolution X) P).inv))
    (𝟙 ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as))
[PROOFSTEP]
refine' (Functor.mapHomotopy _ (HomotopyEquiv.homotopyHomInvId _)).trans _
[GOAL]
case e_a.h.h
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ Homotopy ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map (𝟙 ((projectiveResolutions C).obj X).as))
    (𝟙 ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as))
[PROOFSTEP]
apply Homotopy.ofEq
[GOAL]
case e_a.h.h.h
C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u_1
inst✝¹² : Category.{u_2, u_1} D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasEqualizers C
inst✝⁸ : HasImages C
inst✝⁷ : HasProjectiveResolutions C
inst✝⁶ : Preadditive D
inst✝⁵ : HasEqualizers D
inst✝⁴ : HasCokernels D
inst✝³ : HasImages D
inst✝² : HasImageMaps D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : ProjectiveResolution X
⊢ (Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).map (𝟙 ((projectiveResolutions C).obj X).as) =
    𝟙 ((Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as)
[PROOFSTEP]
simp only [Functor.map_id]
