[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} 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
[PROOFSTEP]
dsimp only [Functor.rightDerived, Functor.rightDerivedObjIso]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} 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
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} 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))
[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✝³ : 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))
[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✝³ : 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))
[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✝³ : 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)))
[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✝³ : 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))
[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✝³ : 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))
[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✝³ : 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)
[PROOFSTEP]
apply InjectiveResolution.descHomotopy 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✝³ : 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))).ι
[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✝³ : 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))).ι
[PROOFSTEP]
simp only [InjectiveResolution.homotopyEquiv_hom_ι_assoc]
[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✝³ : 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))).ι
[PROOFSTEP]
rw [← Category.assoc, w, Category.assoc]
[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✝³ : 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))).ι
[PROOFSTEP]
simp only [InjectiveResolution.homotopyEquiv_inv_ι]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Functor.Additive F
n : ℕ
⊢ rightDerived (𝟙 F) n = 𝟙 (Functor.rightDerived F n)
[PROOFSTEP]
simp [NatTrans.rightDerived]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Functor.Additive F
n : ℕ
⊢ 𝟙
      (injectiveResolutions C ⋙
        Functor.mapHomotopyCategory F (ComplexShape.up ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) =
    𝟙 (Functor.rightDerived 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✝⁵ : Abelian C
inst✝⁴ : HasInjectiveResolutions C
inst✝³ : Abelian D
F G H : C ⥤ D
inst✝² : Functor.Additive F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Additive H
α : F ⟶ G
β : G ⟶ H
n : ℕ
⊢ rightDerived (α ≫ β) n = rightDerived α n ≫ rightDerived β n
[PROOFSTEP]
simp [NatTrans.rightDerived]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : InjectiveResolution X
⊢ app (rightDerived α n) X =
    (Functor.rightDerivedObjIso F n P).hom ≫
      (homologyFunctor D (ComplexShape.up ℕ) n).map (app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) ≫
        (Functor.rightDerivedObjIso 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✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : InjectiveResolution X
⊢ (Functor.rightDerivedObjIso F n P).hom ≫
      (homologyFunctor D (ComplexShape.up ℕ) n).map (app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) ≫
        (Functor.rightDerivedObjIso G n P).inv =
    app (rightDerived α n) X
[PROOFSTEP]
dsimp [NatTrans.rightDerived, Functor.rightDerivedObjIso]
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : InjectiveResolution X
⊢ ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map
              (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).hom)) ≫
        𝟙
          ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).obj
            ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj
              ((Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)))) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n ≫
                HomologicalComplex.dFrom ((Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).obj P.cocomplex) n ≫
                HomologicalComplex.dFrom ((Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).obj P.cocomplex) n =
              0)
          (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) n)
          (HomologicalComplex.Hom.sqFrom (app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) n)
          (_ :
            (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) n).right =
              (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) n).right) ≫
        𝟙 (HomologicalComplex.homology ((Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).obj P.cocomplex) n) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
            ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
              ((Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).map
                (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        (app (mapHomologicalComplex α (ComplexShape.up ℕ)) ((injectiveResolutions 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✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : InjectiveResolution X
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
          ((Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map
            (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).hom)) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n ≫
                HomologicalComplex.dFrom ((Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) n =
              0)
          (_ :
            HomologicalComplex.dTo ((Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).obj P.cocomplex) n ≫
                HomologicalComplex.dFrom ((Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).obj P.cocomplex) n =
              0)
          (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) n)
          (HomologicalComplex.Hom.sqFrom (app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) n)
          (_ :
            (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) n).right =
              (HomologicalComplex.Hom.sqTo (app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) n).right) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).map
              (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        (app (mapHomologicalComplex α (ComplexShape.up ℕ)) ((injectiveResolutions 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✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : InjectiveResolution X
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
          ((Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map
            (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).hom)) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            (app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
            ((Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).map
              (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        (app (mapHomologicalComplex α (ComplexShape.up ℕ)) ((injectiveResolutions 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✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : InjectiveResolution X
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map
            (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).hom ≫
          app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex ≫
            (Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).map
              (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv)) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
      ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        (app (mapHomologicalComplex α (ComplexShape.up ℕ)) ((injectiveResolutions 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✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : InjectiveResolution X
⊢ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
      ((Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map
          (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).hom ≫
        app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex ≫
          (Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).map
            (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv) =
    (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
      (app (mapHomologicalComplex α (ComplexShape.up ℕ)) ((injectiveResolutions 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✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : InjectiveResolution X
⊢ Homotopy
    ((Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map
        (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).hom ≫
      app (mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex ≫
        (Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).map
          (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv)
    (app (mapHomologicalComplex α (ComplexShape.up ℕ)) ((injectiveResolutions 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✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : InjectiveResolution X
⊢ Homotopy
    (app (mapHomologicalComplex α (ComplexShape.up ℕ)) ((injectiveResolutions C).obj X).as ≫
      (Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).map
        ((InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).hom ≫
          (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
    (app (mapHomologicalComplex α (ComplexShape.up ℕ)) ((injectiveResolutions 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✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : InjectiveResolution X
⊢ Homotopy
    ((Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).map
      ((InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).hom ≫
        (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
    (𝟙 ((Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).obj ((injectiveResolutions C).obj X).as))
[PROOFSTEP]
rw [← Functor.map_id]
[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✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : InjectiveResolution X
⊢ Homotopy
    ((Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).map
      ((InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).hom ≫
        (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv))
    ((Functor.mapHomologicalComplex G (ComplexShape.up ℕ)).map (𝟙 ((injectiveResolutions C).obj X).as))
[PROOFSTEP]
apply Functor.mapHomotopy
[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✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
n : ℕ
X : C
P : InjectiveResolution X
⊢ Homotopy
    ((InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).hom ≫
      (InjectiveResolution.homotopyEquiv (Nonempty.some (_ : Nonempty (InjectiveResolution X))) P).inv)
    (𝟙 ((injectiveResolutions C).obj X).as)
[PROOFSTEP]
apply HomotopyEquiv.homotopyHomInvId
[GOAL]
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : PreservesFiniteLimits F
inst✝ : Mono f
ex : Exact f g
⊢ F.map f ≫ F.map g = 0
[PROOFSTEP]
simp [← Functor.map_comp, ex.w]
[GOAL]
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
P : InjectiveResolution X
inst✝ : PreservesFiniteLimits F
⊢ (Iso.refl (F.obj (HomologicalComplex.X ((CochainComplex.single₀ C).obj X) 0))).hom ≫
      F.map (HomologicalComplex.Hom.f P.ι 0) =
    F.map (HomologicalComplex.Hom.f P.ι 0) ≫ (Iso.refl (F.obj (HomologicalComplex.X P.cocomplex 0))).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
P : InjectiveResolution X
inst✝ : PreservesFiniteLimits F
⊢ (Iso.refl (F.obj (HomologicalComplex.X P.cocomplex 0))).hom ≫
      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
    F.map (HomologicalComplex.d P.cocomplex 0 1) ≫
      (HomologicalComplex.xNextIso ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
            (_ : 0 + 1 = 0 + 1)).symm.hom
[PROOFSTEP]
rw [Iso.refl_hom, Category.id_comp, Iso.symm_hom, HomologicalComplex.dFrom_eq]
[GOAL]
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
P : InjectiveResolution X
inst✝ : PreservesFiniteLimits F
⊢ HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ?j ≫
      (HomologicalComplex.xNextIso ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) ?r).inv =
    F.map (HomologicalComplex.d P.cocomplex 0 1) ≫
      (HomologicalComplex.xNextIso ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
          (_ : 0 + 1 = 0 + 1)).inv
[PROOFSTEP]
congr
[GOAL]
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
      𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
    0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0) ≫
      𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
    cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
        (_ :
          HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
              𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
            0) ≫
      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ coequalizer.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) 0 ≫
      cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
          (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0) ≫
        𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
    coequalizer.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) 0 ≫
      cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
          (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
          (_ :
            HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                  (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
              0) ≫
        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) ≫
      cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0) ≫
        𝟙 (F.obj (HomologicalComplex.X P.cocomplex (ComplexShape.next (ComplexShape.up ℕ) 0))) =
    cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) ≫
      cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
          (_ :
            F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0) ≫
                𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
              0) ≫
        F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0))
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X : C
P : InjectiveResolution X
⊢ (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
        cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
      cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0) =
    0
[PROOFSTEP]
have : (ComplexShape.up ℕ).Rel 0 1 := rfl
[GOAL]
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X : C
P : InjectiveResolution X
this : ComplexShape.Rel (ComplexShape.up ℕ) 0 1
⊢ (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
        cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
      cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0) =
    0
[PROOFSTEP]
rw [Category.assoc, cokernel.π_desc, HomologicalComplex.dFrom_eq _ this, mapHomologicalComplex_obj_d, ← Category.assoc,
  ← Functor.map_comp]
[GOAL]
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X : C
P : InjectiveResolution X
this : ComplexShape.Rel (ComplexShape.up ℕ) 0 1
⊢ F.map (HomologicalComplex.Hom.f P.ι 0 ≫ HomologicalComplex.d P.cocomplex 0 1) ≫
      (HomologicalComplex.xNextIso ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) this).inv =
    0
[PROOFSTEP]
simp only [InjectiveResolution.ι_f_zero_comp_complex_d, Functor.map_zero, zero_comp]
[GOAL]
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ rightDerivedZeroToSelfApp F P ≫ rightDerivedZeroToSelfAppInv F P = 𝟙 ((rightDerived F 0).obj X)
[PROOFSTEP]
dsimp [rightDerivedZeroToSelfApp, rightDerivedZeroToSelfAppInv]
[GOAL]
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ ((rightDerivedObjIso F 0 P).hom ≫
        (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                  0)).hom ≫
          kernel.map
              (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
                (_ :
                  HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                        (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                      𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                    0))
              (𝟙 (F.obj (HomologicalComplex.X P.cocomplex (ComplexShape.next (ComplexShape.up ℕ) 0))))
              (_ :
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (_ :
                        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                          0) ≫
                    𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
                  cokernel.desc
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
                      (_ :
                        HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                              (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                            𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                          0) ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
            inv
              (kernel.lift (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                (F.map (HomologicalComplex.Hom.f P.ι 0))
                (_ :
                  F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                      F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)) =
                    0))) ≫
      homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0) =
              0) ≫
        (rightDerivedObjIso F 0 P).inv =
    𝟙 ((rightDerived F 0).obj X)
[PROOFSTEP]
rw [← Category.assoc, Iso.comp_inv_eq, Category.id_comp, Category.assoc, Category.assoc, ← Iso.eq_inv_comp,
  Iso.inv_hom_id]
  -- Porting note: broken ext
[GOAL]
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)).hom ≫
      (kernel.map
            (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                  0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
              (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
              (_ :
                HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                      (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                    𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                  0))
            (𝟙 (F.obj (HomologicalComplex.X P.cocomplex (ComplexShape.next (ComplexShape.up ℕ) 0))))
            (_ :
              cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                    (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                    (_ :
                      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                          HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                        0) ≫
                  𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                    (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
                    (_ :
                      HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                            (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                          𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                        0) ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
          inv
            (kernel.lift (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (F.map (HomologicalComplex.Hom.f P.ι 0))
              (_ :
                F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                    F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)) =
                  0))) ≫
        homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0) =
              0) =
    𝟙 (HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
[PROOFSTEP]
apply homology.hom_to_ext
[GOAL]
case h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ ((homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0)).hom ≫
        (kernel.map
              (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
                (_ :
                  HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                        (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                      𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                    0))
              (𝟙 (F.obj (HomologicalComplex.X P.cocomplex (ComplexShape.next (ComplexShape.up ℕ) 0))))
              (_ :
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (_ :
                        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                          0) ≫
                    𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
                  cokernel.desc
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
                      (_ :
                        HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                              (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                            𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                          0) ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
            inv
              (kernel.lift (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                (F.map (HomologicalComplex.Hom.f P.ι 0))
                (_ :
                  F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                      F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)) =
                    0))) ≫
          homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0)
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
              cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
            (_ :
              (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                    cokernel.π
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                  cokernel.desc
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                    (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                    (_ :
                      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                          HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                        0) =
                0)) ≫
      homology.ι (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0) =
    𝟙 (HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
      homology.ι (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0)
[PROOFSTEP]
apply homology.hom_from_ext
[GOAL]
case h.h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ homology.π' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0) ≫
      ((homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                  0)).hom ≫
          (kernel.map
                (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                  (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0))
                (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                  (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
                  (_ :
                    HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                          (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                        𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                      0))
                (𝟙 (F.obj (HomologicalComplex.X P.cocomplex (ComplexShape.next (ComplexShape.up ℕ) 0))))
                (_ :
                  cokernel.desc
                        (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                        (_ :
                          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                                0 =
                            0) ≫
                      𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
                    cokernel.desc
                        (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                        (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
                        (_ :
                          HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                                (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                              𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                            0) ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
              inv
                (kernel.lift (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                  (F.map (HomologicalComplex.Hom.f P.ι 0))
                  (_ :
                    F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                        F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)) =
                      0))) ≫
            homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                  0)
              (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
              (_ :
                (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                      cokernel.π
                        (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                    cokernel.desc
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (_ :
                        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                          0) =
                  0)) ≫
        homology.ι (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0) =
    homology.π' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0) ≫
      𝟙 (HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
        homology.ι (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)
[PROOFSTEP]
rw [Category.assoc, Category.assoc, homology.lift_ι, Category.id_comp]
[GOAL]
case h.h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ homology.π' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0) ≫
      (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0)).hom ≫
        (kernel.map
              (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
                (_ :
                  HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                        (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                      𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                    0))
              (𝟙 (F.obj (HomologicalComplex.X P.cocomplex (ComplexShape.next (ComplexShape.up ℕ) 0))))
              (_ :
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (_ :
                        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                          0) ≫
                    𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
                  cokernel.desc
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
                      (_ :
                        HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                              (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                            𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                          0) ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
            inv
              (kernel.lift (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                (F.map (HomologicalComplex.Hom.f P.ι 0))
                (_ :
                  F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                      F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)) =
                    0))) ≫
          F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    homology.π' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0) ≫
      homology.ι (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0)
[PROOFSTEP]
erw [homology.π'_ι]
  -- Porting note: had to insist
[GOAL]
case h.h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ homology.π' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0) ≫
      (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0)).hom ≫
        (kernel.map
              (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
                (_ :
                  HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                        (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                      𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                    0))
              (𝟙 (F.obj (HomologicalComplex.X P.cocomplex (ComplexShape.next (ComplexShape.up ℕ) 0))))
              (_ :
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (_ :
                        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                          0) ≫
                    𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
                  cokernel.desc
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
                      (_ :
                        HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                              (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                            𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                          0) ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
            inv
              (kernel.lift (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                (F.map (HomologicalComplex.Hom.f P.ι 0))
                (_ :
                  F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                      F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)) =
                    0))) ≫
          F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
      cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
[PROOFSTEP]
rw [Category.assoc, ← Category.assoc _ _ (cokernel.π _), Abelian.kernel.lift.inv, ← Category.assoc, ←
  Category.assoc _ (kernel.ι _), Limits.kernel.lift_ι, Category.assoc, Category.assoc, ←
  Category.assoc (homologyIsoKernelDesc _ _ _).hom _ _, ← homology.ι, ← Category.assoc]
[GOAL]
case h.h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ (homology.π' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
          (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0) ≫
        homology.ι (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)) ≫
      cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
          (_ :
            HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                  (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
              0) ≫
        cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
      cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
case h.h.ex
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ Exact (F.map (HomologicalComplex.Hom.f P.ι 0))
    (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
[PROOFSTEP]
erw [homology.π'_ι]
  -- Porting note: had to insist
[GOAL]
case h.h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ (kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
        cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
      cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
          (_ :
            HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                  (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
              0) ≫
        cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
      cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
case h.h.ex
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ Exact (F.map (HomologicalComplex.Hom.f P.ι 0))
    (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
[PROOFSTEP]
rw [Category.assoc, ← Category.assoc (cokernel.π _)]
[GOAL]
case h.h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
      (cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
          cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
            (_ :
              HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                    (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                  𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                0)) ≫
        cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
      cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
case h.h.ex
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ Exact (F.map (HomologicalComplex.Hom.f P.ι 0))
    (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
[PROOFSTEP]
erw [cokernel.π_desc]
  -- Porting note: had to insist
[GOAL]
case h.h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
      𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) ≫
        cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
      cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
case h.h.ex
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ Exact (F.map (HomologicalComplex.Hom.f P.ι 0))
    (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
[PROOFSTEP]
rw [whisker_eq]
[GOAL]
case h.h.w
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ 𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) ≫
      cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
case h.h.ex
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ Exact (F.map (HomologicalComplex.Hom.f P.ι 0))
    (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
[PROOFSTEP]
dsimp
[GOAL]
case h.h.w
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ 𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) ≫
      cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
case h.h.ex
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ Exact (F.map (HomologicalComplex.Hom.f P.ι 0))
    (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
[PROOFSTEP]
simp
  -- Porting note: was convert
[GOAL]
case h.h.ex
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ Exact (F.map (HomologicalComplex.Hom.f P.ι 0))
    (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
[PROOFSTEP]
apply exact_of_map_injectiveResolution
[GOAL]
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ rightDerivedZeroToSelfAppInv F P ≫ rightDerivedZeroToSelfApp F P = 𝟙 (F.obj X)
[PROOFSTEP]
dsimp [rightDerivedZeroToSelfApp, rightDerivedZeroToSelfAppInv]
[GOAL]
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ (homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0) =
              0) ≫
        (rightDerivedObjIso F 0 P).inv) ≫
      (rightDerivedObjIso F 0 P).hom ≫
        (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                  0)).hom ≫
          kernel.map
              (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
                (_ :
                  HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                        (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                      𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                    0))
              (𝟙 (F.obj (HomologicalComplex.X P.cocomplex (ComplexShape.next (ComplexShape.up ℕ) 0))))
              (_ :
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (_ :
                        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                          0) ≫
                    𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
                  cokernel.desc
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                      (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
                      (_ :
                        HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                              (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                            𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                          0) ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) ≫
            inv
              (kernel.lift (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                (F.map (HomologicalComplex.Hom.f P.ι 0))
                (_ :
                  F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                      F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)) =
                    0)) =
    𝟙 (F.obj X)
[PROOFSTEP]
rw [← Category.assoc _ (F.rightDerivedObjIso 0 P).hom, Category.assoc _ _ (F.rightDerivedObjIso 0 P).hom,
  Iso.inv_hom_id, Category.comp_id, ← Category.assoc, ← Category.assoc]
  -- Porting note: this IsIso instance used to be filled automatically
[GOAL]
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ ((homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0)
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
              cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
            (_ :
              (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                    cokernel.π
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                  cokernel.desc
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                    (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                    (_ :
                      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                          HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                        0) =
                0) ≫
          (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                  0)).hom) ≫
        kernel.map
          (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
            (_ :
              HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                    (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                  𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                0))
          (𝟙 (F.obj (HomologicalComplex.X P.cocomplex (ComplexShape.next (ComplexShape.up ℕ) 0))))
          (_ :
            cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0) ≫
                𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
              cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
                  (_ :
                    HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                          (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                        𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                      0) ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
      inv
        (kernel.lift (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (F.map (HomologicalComplex.Hom.f P.ι 0))
          (_ :
            F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)) =
              0)) =
    𝟙 (F.obj X)
[PROOFSTEP]
apply (@IsIso.comp_inv_eq D _ _ _ _ _ ?_ _ _).mpr
[GOAL]
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ (homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0) =
              0) ≫
        (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0)).hom) ≫
      kernel.map
        (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0))
        (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
          (_ :
            HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                  (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
              0))
        (𝟙 (F.obj (HomologicalComplex.X P.cocomplex (ComplexShape.next (ComplexShape.up ℕ) 0))))
        (_ :
          cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0) ≫
              𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
            cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
                (_ :
                  HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                        (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                      𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                    0) ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
    𝟙 (F.obj X) ≫
      kernel.lift (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (F.map (HomologicalComplex.Hom.f P.ι 0))
        (_ :
          F.map (HomologicalComplex.Hom.f P.ι 0) ≫
              F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)) =
            0)
[PROOFSTEP]
rw [Category.id_comp]
[GOAL]
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ (homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0) =
              0) ≫
        (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0)).hom) ≫
      kernel.map
        (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0))
        (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
          (_ :
            HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                  (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
              0))
        (𝟙 (F.obj (HomologicalComplex.X P.cocomplex (ComplexShape.next (ComplexShape.up ℕ) 0))))
        (_ :
          cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0) ≫
              𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
            cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
                (_ :
                  HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                        (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                      𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                    0) ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
    kernel.lift (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
      (F.map (HomologicalComplex.Hom.f P.ι 0))
      (_ :
        F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)) =
          0)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ ((homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0)
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
              cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
            (_ :
              (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                    cokernel.π
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                  cokernel.desc
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                    (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                    (_ :
                      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                          HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                        0) =
                0) ≫
          (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                  0)).hom) ≫
        kernel.map
          (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
            (_ :
              HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                    (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                  𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                0))
          (𝟙 (F.obj (HomologicalComplex.X P.cocomplex (ComplexShape.next (ComplexShape.up ℕ) 0))))
          (_ :
            cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0) ≫
                𝟙 (HomologicalComplex.xNext ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0) =
              cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0))
                  (_ :
                    HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                          (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                        𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                      0) ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
      equalizer.ι (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0))) 0 =
    kernel.lift (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (F.map (HomologicalComplex.Hom.f P.ι 0))
        (_ :
          F.map (HomologicalComplex.Hom.f P.ι 0) ≫
              F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)) =
            0) ≫
      equalizer.ι (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0))) 0
[PROOFSTEP]
simp only [Limits.kernel.lift_ι_assoc, Category.assoc, Limits.kernel.lift_ι, homology.lift]
[GOAL]
case h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ kernel.lift
        (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0))
        (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
          cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
        (_ :
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
              cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0) =
            0) ≫
      (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0)).inv ≫
        (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                  0)).hom ≫
          kernel.ι
              (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
                (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0)) ≫
            cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
              (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
              (_ :
                HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                      (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                    𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
                  0) =
    F.map (HomologicalComplex.Hom.f P.ι 0)
[PROOFSTEP]
rw [← Category.assoc, ← Category.assoc, Category.assoc _ _ (homologyIsoKernelDesc _ _ _).hom]
[GOAL]
case h
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ (kernel.lift
          (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0))
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0) =
              0) ≫
        (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                  0)).inv ≫
          (homologyIsoKernelDesc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                  0)).hom) ≫
      kernel.ι
          (cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                0)) ≫
        cokernel.desc (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)))
          (_ :
            HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex)
                  (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 ≫
                𝟙 (F.obj (HomologicalComplex.X P.cocomplex 0)) =
              0) =
    F.map (HomologicalComplex.Hom.f P.ι 0)
[PROOFSTEP]
simp
  -- Porting note: this used to be an instance in ML3
[GOAL]
C : Type u
inst✝⁶ : Category.{w, u} C
D : Type u
inst✝⁵ : Category.{w, u} D
F : C ⥤ D
X✝ Y Z : C
f : X✝ ⟶ Y
g : Y ⟶ Z
inst✝⁴ : Abelian C
inst✝³ : Abelian D
inst✝² : Functor.Additive F
inst✝¹ : EnoughInjectives C
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ IsIso
    (kernel.lift (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
      (F.map (HomologicalComplex.Hom.f P.ι 0))
      (_ :
        F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)) =
          0))
[PROOFSTEP]
apply isIso_kernel_lift_of_exact_of_mono _ _ (exact_of_map_injectiveResolution F P)
[GOAL]
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ F.map f ≫ rightDerivedZeroToSelfAppInv F Q = rightDerivedZeroToSelfAppInv F P ≫ (rightDerived F 0).map f
[PROOFSTEP]
dsimp [rightDerivedZeroToSelfAppInv]
[GOAL]
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ F.map f ≫
      homology.lift (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d Q.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
              0)
          (F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
                      0) =
              0) ≫
        (rightDerivedObjIso F 0 Q).inv =
    (homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0) =
              0) ≫
        (rightDerivedObjIso F 0 P).inv) ≫
      (rightDerived F 0).map f
[PROOFSTEP]
simp only [CategoryTheory.Functor.map_id, Category.id_comp, ← Category.assoc]
[GOAL]
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ (F.map f ≫
        homology.lift (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d Q.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
              0)
          (F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
                      0) =
              0)) ≫
      (rightDerivedObjIso F 0 Q).inv =
    (homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0) =
              0) ≫
        (rightDerivedObjIso F 0 P).inv) ≫
      (rightDerived F 0).map f
[PROOFSTEP]
rw [Iso.comp_inv_eq, rightDerived_map_eq F 0 f (InjectiveResolution.desc f Q P) (by simp), Category.assoc,
  Category.assoc, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id, ←
  Category.assoc (F.rightDerivedObjIso 0 P).inv, Iso.inv_hom_id, Category.id_comp]
[GOAL]
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ P.ι ≫ InjectiveResolution.desc f Q P = (CochainComplex.single₀ C).map f ≫ Q.ι
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ F.map f ≫
      homology.lift (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
        (F.map (HomologicalComplex.d Q.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
            0)
        (F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
          cokernel.π (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
        (_ :
          (F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
                cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)) ≫
              cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
                (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
                    0) =
            0) =
    homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0)
        (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
          cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
        (_ :
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
              cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0) =
            0) ≫
      (homologyFunctor D (ComplexShape.up ℕ) 0).map
        ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P))
[PROOFSTEP]
dsimp only [homologyFunctor_map]
  -- Porting note: broken ext
[GOAL]
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ F.map f ≫
      homology.lift (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
        (F.map (HomologicalComplex.d Q.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
            0)
        (F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
          cokernel.π (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
        (_ :
          (F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
                cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)) ≫
              cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
                (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
                    0) =
            0) =
    homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0)
        (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
          cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
        (_ :
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
              cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0) =
            0) ≫
      homology.map
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
            0)
        (HomologicalComplex.Hom.sqTo
          ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0)
        (HomologicalComplex.Hom.sqFrom
          ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0)
        (_ :
          (HomologicalComplex.Hom.sqTo
                ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).right =
            (HomologicalComplex.Hom.sqTo
                ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).right)
[PROOFSTEP]
apply homology.hom_to_ext
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ (F.map f ≫
        homology.lift (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d Q.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
              0)
          (F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
                      0) =
              0)) ≫
      homology.ι (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
        (F.map (HomologicalComplex.d Q.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
            0) =
    (homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0) =
              0) ≫
        homology.map
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
              0)
          (HomologicalComplex.Hom.sqTo
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0)
          (HomologicalComplex.Hom.sqFrom
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0)
          (_ :
            (HomologicalComplex.Hom.sqTo
                  ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).right =
              (HomologicalComplex.Hom.sqTo
                  ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).right)) ≫
      homology.ι (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
        (F.map (HomologicalComplex.d Q.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
            0)
[PROOFSTEP]
rw [Category.assoc, homology.lift_ι, Category.assoc]
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ F.map f ≫
      F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
        cokernel.π (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0)
        (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
          cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
        (_ :
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
              cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0) =
            0) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
              0)
          (HomologicalComplex.Hom.sqTo
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0)
          (HomologicalComplex.Hom.sqFrom
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0)
          (_ :
            (HomologicalComplex.Hom.sqTo
                  ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).right =
              (HomologicalComplex.Hom.sqTo
                  ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).right) ≫
        homology.ι (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d Q.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0 =
              0)
[PROOFSTEP]
erw [homology.map_ι]
  -- Porting note: need to insist
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ F.map f ≫
      F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
        cokernel.π (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
            0)
        (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
          cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
        (_ :
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
              cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                    0) =
            0) ≫
      homology.ι (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
          (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0) ≫
        cokernel.map (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
          (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
          (HomologicalComplex.Hom.sqTo
              ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left
          (HomologicalComplex.Hom.sqFrom
              ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                (HomologicalComplex.Hom.sqFrom
                    ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left =
              (HomologicalComplex.Hom.sqTo
                    ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left ≫
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
[PROOFSTEP]
rw [← Category.assoc (homology.lift _ _ _ _ _) _ _]
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ F.map f ≫
      F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
        cokernel.π (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    (homology.lift (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.cocomplex 0 (ComplexShape.next (ComplexShape.up ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)
          (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
            cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)))
          (_ :
            (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
                  cokernel.π
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)) ≫
                cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
                      0) =
              0) ≫
        homology.ι (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
          (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 =
              0)) ≫
      cokernel.map (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
        (HomologicalComplex.Hom.sqTo
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left
        (HomologicalComplex.Hom.sqFrom
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              (HomologicalComplex.Hom.sqFrom
                  ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left =
            (HomologicalComplex.Hom.sqTo
                  ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left ≫
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
[PROOFSTEP]
erw [homology.lift_ι]
  -- Porting note: need to insist
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ F.map f ≫
      F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
        cokernel.π (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    (F.map (HomologicalComplex.Hom.f P.ι 0) ≫
        cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))) ≫
      cokernel.map (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
        (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
        (HomologicalComplex.Hom.sqTo
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left
        (HomologicalComplex.Hom.sqFrom
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
              (HomologicalComplex.Hom.sqFrom
                  ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left =
            (HomologicalComplex.Hom.sqTo
                  ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left ≫
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ F.map f ≫
      F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
        cokernel.π (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    F.map (HomologicalComplex.Hom.f P.ι 0) ≫
      cokernel.π (F.map (HomologicalComplex.d P.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) ≫
        cokernel.map (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0)
          (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
          (HomologicalComplex.Hom.sqTo
              ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left
          (HomologicalComplex.Hom.sqFrom
              ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj P.cocomplex) 0 ≫
                (HomologicalComplex.Hom.sqFrom
                    ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left =
              (HomologicalComplex.Hom.sqTo
                    ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left ≫
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
[PROOFSTEP]
erw [cokernel.π_desc]
  -- Porting note: need to insist
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ F.map f ≫
      F.map (HomologicalComplex.Hom.f Q.ι 0) ≫
        cokernel.π (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    F.map (HomologicalComplex.Hom.f P.ι 0) ≫
      (HomologicalComplex.Hom.sqFrom
            ((mapHomologicalComplex F (ComplexShape.up ℕ)).map (InjectiveResolution.desc f Q P)) 0).left ≫
        cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
[PROOFSTEP]
rw [← Category.assoc, ← Functor.map_comp, ← Category.assoc, HomologicalComplex.Hom.sqFrom_left,
  mapHomologicalComplex_map_f, ← Functor.map_comp,
  show f ≫ Q.ι.f 0 = P.ι.f 0 ≫ (InjectiveResolution.desc f Q P).f 0 from
    HomologicalComplex.congr_hom (InjectiveResolution.desc_commutes f Q P).symm 0]
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{w, u} C
D : Type u
inst✝⁴ : Category.{w, u} D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
inst✝³ : Abelian C
inst✝² : Abelian D
inst✝¹ : Functor.Additive F
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
⊢ F.map (HomologicalComplex.Hom.f P.ι 0 ≫ HomologicalComplex.Hom.f (InjectiveResolution.desc f Q P) 0) ≫
      cokernel.π (F.map (HomologicalComplex.d Q.cocomplex (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)) =
    F.map (HomologicalComplex.Hom.f P.ι 0 ≫ HomologicalComplex.Hom.f (InjectiveResolution.desc f Q P) 0) ≫
      cokernel.π (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.up ℕ)).obj Q.cocomplex) 0)
[PROOFSTEP]
rfl
  -- Porting note: extra rfl
