C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (injectiveResolutions C ⋙
          mapHomotopyCategory F (ComplexShape.up ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      f =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).mapIso
            (HomotopyCategory.isoOfHomotopyEquiv
              (mapHomotopyEquiv F
                (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q))) ≪≫
          (HomotopyCategory.homologyFactors D (ComplexShape.up ℕ) n).app
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex)).hom ≫
      (homologyFunctor D (ComplexShape.up ℕ) n).map ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) ≫
        ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).mapIso
              (HomotopyCategory.isoOfHomotopyEquiv
                (mapHomotopyEquiv F
                  (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P))) ≪≫
            (HomotopyCategory.homologyFactors D (ComplexShape.up ℕ) n).app
              ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)).inv
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (rightDerived F n).map f =
    (rightDerivedObjIso F n Q).hom ≫
      (homologyFunctor D (ComplexShape.up ℕ) n).map ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) ≫
        (rightDerivedObjIso F n P).inv
dsimp only [Functor.rightDerived, Functor.rightDerivedObjIso]
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f)) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
              (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom)) ≫
        𝟙
          ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).obj
            ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj
              ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex)))) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n =
              0)
          (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n)
          (HomologicalComplex.Hom.sqFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n)
          (_ :
            (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n).right =
              (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n).right) ≫
        𝟙 (HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
            ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
              ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
                (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (injectiveResolutions C ⋙
          mapHomotopyCategory F (ComplexShape.up ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      f =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).mapIso
            (HomotopyCategory.isoOfHomotopyEquiv
              (mapHomotopyEquiv F
                (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q))) ≪≫
          (HomotopyCategory.homologyFactors D (ComplexShape.up ℕ) n).app
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex)).hom ≫
      (homologyFunctor D (ComplexShape.up ℕ) n).map ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) ≫
        ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).mapIso
              (HomotopyCategory.isoOfHomotopyEquiv
                (mapHomotopyEquiv F
                  (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P))) ≪≫
            (HomotopyCategory.homologyFactors D (ComplexShape.up ℕ) n).app
              ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)).inv
dsimp
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
          ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
            (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom)) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n =
              0)
          (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n)
          (HomologicalComplex.Hom.sqFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n)
          (_ :
            (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n).right =
              (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n).right) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
              (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f)) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
              (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom)) ≫
        𝟙
          ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).obj
            ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj
              ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex)))) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n =
              0)
          (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n)
          (HomologicalComplex.Hom.sqFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n)
          (_ :
            (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n).right =
              (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n).right) ≫
        𝟙 (HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
            ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
              ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
                (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
simp only [Category.comp_id, Category.id_comp]
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
          ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
            (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom)) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
              (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
          ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
            (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom)) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n =
              0)
          (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n)
          (HomologicalComplex.Hom.sqFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n)
          (_ :
            (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n).right =
              (HomologicalComplex.Hom.sqTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g) n).right) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
              (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
rw [← homologyFunctor_map, HomotopyCategory.homologyFunctor_map_factors]
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
          ((InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom ≫
            g ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv)))
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
          ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
            (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom)) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map g)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
              (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
simp only [← Functor.map_comp]
case e_a
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (mapHomotopyCategory F (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f) =
    (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
      ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
        ((InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom ≫
          g ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((mapHomotopyCategory F (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
          ((InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom ≫
            g ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv)))
congr 1
case e_a.h
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ Homotopy ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (injectiveResolution.desc f))
    ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
      ((InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom ≫
        g ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
case e_a
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (mapHomotopyCategory F (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f) =
    (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
      ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
        ((InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom ≫
          g ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
apply HomotopyCategory.eq_of_homotopy
case e_a.h.h
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ Homotopy (injectiveResolution.desc f)
    ((InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom ≫
      g ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv)
case e_a.h
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ Homotopy ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (injectiveResolution.desc f))
    ((mapHomologicalComplex F (ComplexShape.up ℕ)).map
      ((InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom ≫
        g ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
apply Functor.mapHomotopy
case e_a.h.h.g_comm
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (Nonempty.some (_ : Nonempty (InjectiveResolution Y))).ι ≫ injectiveResolution.desc f =
    (CochainComplex.single₀ C).map f ≫ (Nonempty.some (_ : Nonempty (InjectiveResolution X))).ι

case e_a.h.h.h_comm
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (Nonempty.some (_ : Nonempty (InjectiveResolution Y))).ι ≫
      (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom ≫
        g ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv =
    (CochainComplex.single₀ C).map f ≫ (Nonempty.some (_ : Nonempty (InjectiveResolution X))).ι
case e_a.h.h
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ Homotopy (injectiveResolution.desc f)
    ((InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom ≫
      g ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv)
apply InjectiveResolution.descHomotopy f
no goals
case e_a.h.h.g_comm
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (Nonempty.some (_ : Nonempty (InjectiveResolution Y))).ι ≫ injectiveResolution.desc f =
    (CochainComplex.single₀ C).map f ≫ (Nonempty.some (_ : Nonempty (InjectiveResolution X))).ι
simp
case e_a.h.h.h_comm
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ Q.ι ≫ g ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv =
    (CochainComplex.single₀ C).map f ≫ (Nonempty.some (_ : Nonempty (InjectiveResolution X))).ι
case e_a.h.h.h_comm
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (Nonempty.some (_ : Nonempty (InjectiveResolution Y))).ι ≫
      (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution Y))) Q).hom ≫
        g ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv =
    (CochainComplex.single₀ C).map f ≫ (Nonempty.some (_ : Nonempty (InjectiveResolution X))).ι
simp only [InjectiveResolution.homotopyEquiv_hom_ι_assoc]
case e_a.h.h.h_comm
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (CochainComplex.single₀ C).map f ≫
      P.ι ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv =
    (CochainComplex.single₀ C).map f ≫ (Nonempty.some (_ : Nonempty (InjectiveResolution X))).ι
case e_a.h.h.h_comm
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ Q.ι ≫ g ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv =
    (CochainComplex.single₀ C).map f ≫ (Nonempty.some (_ : Nonempty (InjectiveResolution X))).ι
rw [← Category.assoc, w, Category.assoc]
no goals
case e_a.h.h.h_comm
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Additive F
n : ℕ
X Y : C
f : Y ⟶ X
P : InjectiveResolution X
Q : InjectiveResolution Y
g : Q.cocomplex ⟶ P.cocomplex
w : Q.ι ≫ g = (CochainComplex.single₀ C).map f ≫ P.ι
⊢ (CochainComplex.single₀ C).map f ≫
      P.ι ≫ (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv =
    (CochainComplex.single₀ C).map f ≫ (Nonempty.some (_ : Nonempty (InjectiveResolution X))).ι
simp only [InjectiveResolution.homotopyEquiv_inv_ι]