[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✝¹ : PreservesFiniteColimits F
inst✝ : Epi g
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 : ProjectiveResolution X
inst✝ : PreservesFiniteColimits F
⊢ (HomologicalComplex.xPrevIso ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
            (_ : 0 + 1 = 0 + 1)).symm.hom ≫
      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    F.map (HomologicalComplex.d P.complex 1 0) ≫ (Iso.refl (F.obj (HomologicalComplex.X P.complex 0))).hom
[PROOFSTEP]
simp only [Iso.symm_hom, HomologicalComplex.xPrevIso_comp_dTo]
[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 : ProjectiveResolution X
inst✝ : PreservesFiniteColimits F
⊢ HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) (0 + 1) 0 =
    F.map (HomologicalComplex.d P.complex 1 0) ≫ (Iso.refl (F.obj (HomologicalComplex.X P.complex 0))).hom
[PROOFSTEP]
simp only [mapHomologicalComplex_obj_d, Iso.refl_hom, Category.comp_id]
[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 : ProjectiveResolution X
inst✝ : PreservesFiniteColimits F
⊢ F.map (HomologicalComplex.d P.complex (0 + 1) 0) = F.map (HomologicalComplex.d P.complex 1 0)
[PROOFSTEP]
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
P : ProjectiveResolution X
inst✝ : PreservesFiniteColimits F
⊢ (Iso.refl (F.obj (HomologicalComplex.X P.complex 0))).hom ≫ F.map (HomologicalComplex.Hom.f P.π 0) =
    F.map (HomologicalComplex.Hom.f P.π 0) ≫
      (Iso.refl (F.obj (HomologicalComplex.X ((ChainComplex.single₀ C).obj X) 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
inst✝ : EnoughProjectives C
X : C
P : ProjectiveResolution X
⊢ kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0) ≫
      kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
        F.map (HomologicalComplex.Hom.f P.π 0) =
    0
[PROOFSTEP]
rw [kernel.lift_ι_assoc, HomologicalComplex.dTo_eq _ (by simp : (ComplexShape.down ℕ).Rel 1 0),
  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✝ : EnoughProjectives C
X : C
P : ProjectiveResolution X
⊢ ComplexShape.Rel (ComplexShape.down ℕ) 1 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✝ : EnoughProjectives C
X : C
P : ProjectiveResolution X
⊢ (HomologicalComplex.xPrevIso ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) (_ : 0 + 1 = 1)).hom ≫
      F.map (HomologicalComplex.d P.complex 1 0 ≫ HomologicalComplex.Hom.f P.π 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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ F.obj X ⟶ (leftDerived F 0).obj X
[PROOFSTEP]
have := isIso_cokernel_desc_of_exact_of_epi _ _ (exact_of_map_projectiveResolution 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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
this :
  IsIso
    (cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
      (F.map (HomologicalComplex.Hom.f P.π 0))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            F.map (HomologicalComplex.Hom.f P.π 0) =
          0))
⊢ F.obj X ⟶ (leftDerived F 0).obj X
[PROOFSTEP]
refine'
  (asIso (cokernel.desc _ _ (exact_of_map_projectiveResolution F P).w)).inv ≫
    _ ≫ (homologyIsoCokernelLift _ _ _).inv ≫ (leftDerivedObjIso F 0 P).inv
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
this :
  IsIso
    (cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
      (F.map (HomologicalComplex.Hom.f P.π 0))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            F.map (HomologicalComplex.Hom.f P.π 0) =
          0))
⊢ cokernel (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ⟶
    cokernel
      (kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0))
[PROOFSTEP]
refine' cokernel.map _ _ (𝟙 _) (kernel.lift _ (𝟙 _) (by 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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
this :
  IsIso
    (cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
      (F.map (HomologicalComplex.Hom.f P.π 0))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            F.map (HomologicalComplex.Hom.f P.π 0) =
          0))
⊢ 𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
this :
  IsIso
    (cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
      (F.map (HomologicalComplex.Hom.f P.π 0))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            F.map (HomologicalComplex.Hom.f P.π 0) =
          0))
⊢ HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
      kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0))
        (_ :
          𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
              HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0
                (ComplexShape.next (ComplexShape.down ℕ) 0) =
            0) =
    𝟙 (HomologicalComplex.xPrev ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
      kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)
[PROOFSTEP]
ext
  -- Porting note: this used to just be `simp`
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
this :
  IsIso
    (cokernel.desc (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
      (F.map (HomologicalComplex.Hom.f P.π 0))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            F.map (HomologicalComplex.Hom.f P.π 0) =
          0))
⊢ (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
        kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
          (𝟙 (HomologicalComplex.X ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0))
          (_ :
            𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                HomologicalComplex.d ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0
                  (ComplexShape.next (ComplexShape.down ℕ) 0) =
              0)) ≫
      equalizer.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) 0 =
    (𝟙 (HomologicalComplex.xPrev ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
        kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
          (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)) ≫
      equalizer.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) 0
[PROOFSTEP]
simp only [Category.assoc, kernel.lift_ι, Category.comp_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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ leftDerivedZeroToSelfApp F P ≫ leftDerivedZeroToSelfAppInv F P = 𝟙 ((leftDerived F 0).obj X)
[PROOFSTEP]
dsimp [leftDerivedZeroToSelfApp, leftDerivedZeroToSelfAppInv]
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ ((leftDerivedObjIso F 0 P).hom ≫
        homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)
          (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
            F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0) ≫
                kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
              0)) ≫
      inv
          (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.Hom.f P.π 0))
            (_ :
              F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
                0)) ≫
        cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0))
            (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
            (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
              (_ :
                𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                    F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                  0))
            (_ :
              F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                  kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                    (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                    (_ :
                      𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                          F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                        0) =
                𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                  kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                    (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                    (_ :
                      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                          HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                        0)) ≫
          (homologyIsoCokernelLift
                (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0)).inv ≫
            (leftDerivedObjIso F 0 P).inv =
    𝟙 ((leftDerived F 0).obj X)
[PROOFSTEP]
rw [← Category.assoc, ← Category.assoc, ← Category.assoc, Iso.comp_inv_eq]
  -- Porting note: working around 'motive is not type correct'
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ ((((leftDerivedObjIso F 0 P).hom ≫
            homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0)
              (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
                F.map (HomologicalComplex.Hom.f P.π 0))
              (_ :
                kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                      (_ :
                        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                          0) ≫
                    kernel.ι
                        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                      F.map (HomologicalComplex.Hom.f P.π 0) =
                  0)) ≫
          inv
            (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.Hom.f P.π 0))
              (_ :
                F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                    F.map (HomologicalComplex.Hom.f P.π 0) =
                  0))) ≫
        cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0))
          (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
            (_ :
              𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                  F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                  (_ :
                    𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                        F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                      0) =
              𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0))) ≫
      (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)).inv =
    𝟙 ((leftDerived F 0).obj X) ≫ (leftDerivedObjIso F 0 P).hom
[PROOFSTEP]
simp only [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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ ((((leftDerivedObjIso F 0 P).hom ≫
            homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0)
              (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
                F.map (HomologicalComplex.Hom.f P.π 0))
              (_ :
                kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                      (_ :
                        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                          0) ≫
                    kernel.ι
                        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                      F.map (HomologicalComplex.Hom.f P.π 0) =
                  0)) ≫
          inv
            (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.Hom.f P.π 0))
              (_ :
                F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                    F.map (HomologicalComplex.Hom.f P.π 0) =
                  0))) ≫
        cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0))
          (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
            (_ :
              𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                  F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                  (_ :
                    𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                        F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                      0) =
              𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0))) ≫
      (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)).inv =
    (leftDerivedObjIso F 0 P).hom
[PROOFSTEP]
rw [Category.assoc, Category.assoc, 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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ (leftDerivedObjIso F 0 P).hom ≫
      homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)
          (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
            F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0) ≫
                kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
              0) ≫
        inv
            (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.Hom.f P.π 0))
              (_ :
                F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                    F.map (HomologicalComplex.Hom.f P.π 0) =
                  0)) ≫
          cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0))
              (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
              (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                (_ :
                  𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                      F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                    0))
              (_ :
                F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                    kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                      (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                      (_ :
                        𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                            F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                          0) =
                  𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                    kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                      (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                      (_ :
                        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                          0)) ≫
            (homologyIsoCokernelLift
                (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0)).inv =
    (leftDerivedObjIso F 0 P).hom
[PROOFSTEP]
convert Category.comp_id (leftDerivedObjIso F 0 P).hom
[GOAL]
case h.e'_2.h.h.e'_7.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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
⊢ homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)
        (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
          F.map (HomologicalComplex.Hom.f P.π 0))
        (_ :
          kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0) ≫
              kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                F.map (HomologicalComplex.Hom.f P.π 0) =
            0) ≫
      inv
          (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.Hom.f P.π 0))
            (_ :
              F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
                0)) ≫
        cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0))
            (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
            (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
              (_ :
                𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                    F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                  0))
            (_ :
              F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                  kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                    (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                    (_ :
                      𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                          F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                        0) =
                𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                  kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                    (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                    (_ :
                      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                          HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                        0)) ≫
          (homologyIsoCokernelLift
              (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0)).inv =
    𝟙 ((homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
[PROOFSTEP]
rw [← Category.assoc, ← Category.assoc, Iso.comp_inv_eq]
  -- Porting note: broken ext
[GOAL]
case h.e'_2.h.h.e'_7.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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
⊢ (homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)
          (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
            F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0) ≫
                kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
              0) ≫
        inv
          (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.Hom.f P.π 0))
            (_ :
              F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
                0))) ≫
      cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0))
        (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
        (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
          (_ :
            𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
              0))
        (_ :
          F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
              kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                (_ :
                  𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                      F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                    0) =
            𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
              kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0)) =
    𝟙
        ((homologyFunctor D (ComplexShape.down ℕ) 0).obj
          ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)) ≫
      (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)).hom
[PROOFSTEP]
apply homology.hom_from_ext
[GOAL]
case h.e'_2.h.h.e'_7.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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
⊢ homology.π' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0) ≫
      (homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0)
            (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
              F.map (HomologicalComplex.Hom.f P.π 0))
            (_ :
              kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                    (_ :
                      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                          HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                        0) ≫
                  kernel.ι
                      (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                    F.map (HomologicalComplex.Hom.f P.π 0) =
                0) ≫
          inv
            (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.Hom.f P.π 0))
              (_ :
                F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                    F.map (HomologicalComplex.Hom.f P.π 0) =
                  0))) ≫
        cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0))
          (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
            (_ :
              𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                  F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                  (_ :
                    𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                        F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                      0) =
              𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0)) =
    homology.π' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0) ≫
      𝟙
          ((homologyFunctor D (ComplexShape.down ℕ) 0).obj
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)) ≫
        (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0)).hom
[PROOFSTEP]
simp only [← Category.assoc]
[GOAL]
case h.e'_2.h.h.e'_7.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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
⊢ ((homology.π' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
            (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0) ≫
          homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0)
            (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
              F.map (HomologicalComplex.Hom.f P.π 0))
            (_ :
              kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                    (_ :
                      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                          HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                        0) ≫
                  kernel.ι
                      (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                    F.map (HomologicalComplex.Hom.f P.π 0) =
                0)) ≫
        inv
          (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.Hom.f P.π 0))
            (_ :
              F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
                0))) ≫
      cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0))
        (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
        (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
          (_ :
            𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
              0))
        (_ :
          F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
              kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                (_ :
                  𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                      F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                    0) =
            𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
              kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0)) =
    (homology.π' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
          (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0) ≫
        𝟙
          ((homologyFunctor D (ComplexShape.down ℕ) 0).obj
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))) ≫
      (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)).hom
[PROOFSTEP]
erw [homology.π'_desc', Category.assoc, Category.assoc, ← Category.assoc (F.map _),
  Abelian.cokernel.desc.inv _ _ (exact_of_map_projectiveResolution F P), cokernel.π_desc, homology.π', Category.comp_id,
  Category.assoc (cokernel.π _), Iso.inv_hom_id, Category.comp_id, ← Category.assoc]
  -- Porting note: restructured proof to avoid `convert`
[GOAL]
case h.e'_2.h.h.e'_7.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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
⊢ (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
        kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
          (_ :
            𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
              0)) ≫
      cokernel.π
        (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)) =
    cokernel.π
      (kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0))
[PROOFSTEP]
conv_rhs => rw [← Category.id_comp (cokernel.π _)]
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
| cokernel.π
    (kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0))
[PROOFSTEP]
rw [← Category.id_comp (cokernel.π _)]
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
| cokernel.π
    (kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0))
[PROOFSTEP]
rw [← Category.id_comp (cokernel.π _)]
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
| cokernel.π
    (kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0))
[PROOFSTEP]
rw [← Category.id_comp (cokernel.π _)]
[GOAL]
case h.e'_2.h.h.e'_7.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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
⊢ (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
        kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
          (_ :
            𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
              0)) ≫
      cokernel.π
        (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)) =
    𝟙 (kernel (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)) ≫
      cokernel.π
        (kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
          (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0))
[PROOFSTEP]
congr
[GOAL]
case h.e'_2.h.h.e'_7.h.h.e_a
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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
⊢ kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
      kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
        (_ :
          𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
              F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
            0) =
    𝟙 (kernel (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0))
[PROOFSTEP]
ext
  -- Porting note: working around 'motive is not type correct'
[GOAL]
case h.e'_2.h.h.e'_7.h.h.e_a.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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
⊢ (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
        kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
          (_ :
            𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
              0)) ≫
      equalizer.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) 0 =
    𝟙 (kernel (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)) ≫
      equalizer.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) 0
[PROOFSTEP]
simp only [Category.id_comp]
[GOAL]
case h.e'_2.h.h.e'_7.h.h.e_a.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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
⊢ (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
        kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
          (_ :
            𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
              0)) ≫
      equalizer.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) 0 =
    equalizer.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) 0
[PROOFSTEP]
rw [Category.assoc, equalizer_as_kernel, kernel.lift_ι]
[GOAL]
case h.e'_2.h.h.e'_7.h.h.e_a.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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
e_1✝ :
  ((leftDerived F 0).obj X ⟶
      homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)) =
    ((leftDerived F 0).obj X ⟶
      (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex))
e_4✝ :
  HomologicalComplex.homology ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
e_5✝ :
  homology (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
          0) =
    (homologyFunctor D (ComplexShape.down ℕ) 0).obj ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
⊢ kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
      𝟙 (F.obj (HomologicalComplex.X P.complex 0)) =
    kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
[PROOFSTEP]
simp only [Category.comp_id]
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ leftDerivedZeroToSelfAppInv F P ≫ leftDerivedZeroToSelfApp F P = 𝟙 (F.obj X)
[PROOFSTEP]
dsimp [leftDerivedZeroToSelfApp, leftDerivedZeroToSelfAppInv]
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ (inv
          (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.Hom.f P.π 0))
            (_ :
              F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
                0)) ≫
        cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0))
            (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
            (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
              (_ :
                𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                    F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                  0))
            (_ :
              F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                  kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                    (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                    (_ :
                      𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                          F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                        0) =
                𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                  kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                    (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                    (_ :
                      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                          HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                        0)) ≫
          (homologyIsoCokernelLift
                (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0)).inv ≫
            (leftDerivedObjIso F 0 P).inv) ≫
      (leftDerivedObjIso F 0 P).hom ≫
        homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)
          (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
            F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0) ≫
                kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
              0) =
    𝟙 (F.obj X)
[PROOFSTEP]
rw [Category.assoc, Category.assoc]
  -- Porting note: working around 'motive is not type correct'
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ inv
        (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                F.map (HomologicalComplex.Hom.f P.π 0) =
              0)) ≫
      cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0))
          (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
            (_ :
              𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                  F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                  (_ :
                    𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                        F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                      0) =
              𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0)) ≫
        ((homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0)).inv ≫
            (leftDerivedObjIso F 0 P).inv) ≫
          (leftDerivedObjIso F 0 P).hom ≫
            homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0)
              (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
                F.map (HomologicalComplex.Hom.f P.π 0))
              (_ :
                kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                      (_ :
                        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                          0) ≫
                    kernel.ι
                        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                      F.map (HomologicalComplex.Hom.f P.π 0) =
                  0) =
    𝟙 (F.obj X)
[PROOFSTEP]
simp only [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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ inv
        (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                F.map (HomologicalComplex.Hom.f P.π 0) =
              0)) ≫
      cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0))
          (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
            (_ :
              𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                  F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                  (_ :
                    𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                        F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                      0) =
              𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0)) ≫
        (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0)).inv ≫
          (leftDerivedObjIso F 0 P).inv ≫
            (leftDerivedObjIso F 0 P).hom ≫
              homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0)
                (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0))
                (_ :
                  kernel.lift
                        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                        (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                        (_ :
                          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)
                                0 =
                            0) ≫
                      kernel.ι
                          (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                        F.map (HomologicalComplex.Hom.f P.π 0) =
                    0) =
    𝟙 (F.obj X)
[PROOFSTEP]
rw [← Category.assoc (F.leftDerivedObjIso 0 P).inv, Iso.inv_hom_id]
  -- Porting note: working around 'motive is not type correct'
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ inv
        (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                F.map (HomologicalComplex.Hom.f P.π 0) =
              0)) ≫
      cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0))
          (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
            (_ :
              𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                  F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                  (_ :
                    𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                        F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                      0) =
              𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0)) ≫
        (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0)).inv ≫
          𝟙
              ((homologyFunctor D (ComplexShape.down ℕ) 0).obj
                ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex)) ≫
            homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0)
              (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
                F.map (HomologicalComplex.Hom.f P.π 0))
              (_ :
                kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                      (_ :
                        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                          0) ≫
                    kernel.ι
                        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                      F.map (HomologicalComplex.Hom.f P.π 0) =
                  0) =
    𝟙 (F.obj X)
[PROOFSTEP]
simp only [Category.id_comp]
  -- Porting note: instance not found even though it is present in the goal
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ inv
        (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                F.map (HomologicalComplex.Hom.f P.π 0) =
              0)) ≫
      cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0))
          (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
            (_ :
              𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                  F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                  (_ :
                    𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                        F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                      0) =
              𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0)) ≫
        (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0)).inv ≫
          homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0)
            (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
              F.map (HomologicalComplex.Hom.f P.π 0))
            (_ :
              kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                    (_ :
                      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                          HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                        0) ≫
                  kernel.ι
                      (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                    F.map (HomologicalComplex.Hom.f P.π 0) =
                0) =
    𝟙 (F.obj X)
[PROOFSTEP]
have :
  IsIso
    (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.Hom.f P.π 0)) (exact_of_map_projectiveResolution F P).w) :=
  isIso_cokernel_desc_of_exact_of_epi _ _ (exact_of_map_projectiveResolution 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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
this :
  IsIso
    (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.Hom.f P.π 0))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            F.map (HomologicalComplex.Hom.f P.π 0) =
          0))
⊢ inv
        (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                F.map (HomologicalComplex.Hom.f P.π 0) =
              0)) ≫
      cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0))
          (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
            (_ :
              𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                  F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                  (_ :
                    𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                        F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                      0) =
              𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0)) ≫
        (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0)).inv ≫
          homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0)
            (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
              F.map (HomologicalComplex.Hom.f P.π 0))
            (_ :
              kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                    (_ :
                      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                          HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                        0) ≫
                  kernel.ι
                      (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                    F.map (HomologicalComplex.Hom.f P.π 0) =
                0) =
    𝟙 (F.obj X)
[PROOFSTEP]
rw [IsIso.inv_comp_eq]
  -- Porting note: working around 'motive is not type correct'
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
this :
  IsIso
    (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.Hom.f P.π 0))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            F.map (HomologicalComplex.Hom.f P.π 0) =
          0))
⊢ cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0))
        (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
        (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
          (_ :
            𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
              0))
        (_ :
          F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
              kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                (_ :
                  𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                      F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                    0) =
            𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
              kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0)) ≫
      (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0)).inv ≫
        homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)
          (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
            F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0) ≫
                kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
              0) =
    cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.Hom.f P.π 0))
        (_ :
          F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
              F.map (HomologicalComplex.Hom.f P.π 0) =
            0) ≫
      𝟙 (F.obj X)
[PROOFSTEP]
simp only [Category.comp_id]
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
this :
  IsIso
    (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.Hom.f P.π 0))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            F.map (HomologicalComplex.Hom.f P.π 0) =
          0))
⊢ cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0))
        (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
        (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
          (_ :
            𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
              0))
        (_ :
          F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
              kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                (_ :
                  𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                      F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                    0) =
            𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
              kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0)) ≫
      (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0)).inv ≫
        homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)
          (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
            F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0) ≫
                kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
              0) =
    cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.Hom.f P.π 0))
      (_ :
        F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
            F.map (HomologicalComplex.Hom.f P.π 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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
this :
  IsIso
    (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.Hom.f P.π 0))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            F.map (HomologicalComplex.Hom.f P.π 0) =
          0))
⊢ coequalizer.π (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0)) 0 ≫
      cokernel.map (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0))
          (𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))))
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
            (_ :
              𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                  F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                0))
          (_ :
            F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
                  (_ :
                    𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                        F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
                      0) =
              𝟙 (F.obj (HomologicalComplex.X P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0))) ≫
                kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                  (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0)) ≫
        (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0)).inv ≫
          homology.desc' (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0)
            (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
              F.map (HomologicalComplex.Hom.f P.π 0))
            (_ :
              kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                    (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                    (_ :
                      HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                          HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                        0) ≫
                  kernel.ι
                      (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                    F.map (HomologicalComplex.Hom.f P.π 0) =
                0) =
    coequalizer.π (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0)) 0 ≫
      cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
        (F.map (HomologicalComplex.Hom.f P.π 0))
        (_ :
          F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0) ≫
              F.map (HomologicalComplex.Hom.f P.π 0) =
            0)
[PROOFSTEP]
simp only [cokernel.π_desc_assoc, Category.assoc, cokernel.π_desc, homology.desc']
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
this :
  IsIso
    (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.Hom.f P.π 0))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            F.map (HomologicalComplex.Hom.f P.π 0) =
          0))
⊢ kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
        (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
        (_ :
          𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
              F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
            0) ≫
      cokernel.π
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0)) ≫
        (homologyIsoCokernelLift (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0)).inv ≫
          (homologyIsoCokernelLift
                (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0)).hom ≫
            cokernel.desc
              (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
                (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0))
              (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
                F.map (HomologicalComplex.Hom.f P.π 0))
              (_ :
                kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                      (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                      (_ :
                        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                            HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                          0) ≫
                    kernel.ι
                        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                      F.map (HomologicalComplex.Hom.f P.π 0) =
                  0) =
    F.map (HomologicalComplex.Hom.f P.π 0)
[PROOFSTEP]
rw [← Category.assoc, ← Category.assoc (homologyIsoCokernelLift _ _ _).inv, Iso.inv_hom_id]
[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✝¹ : EnoughProjectives C
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
this :
  IsIso
    (cokernel.desc (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
      (F.map (HomologicalComplex.Hom.f P.π 0))
      (_ :
        HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
            F.map (HomologicalComplex.Hom.f P.π 0) =
          0))
⊢ (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
          (𝟙 (F.obj (HomologicalComplex.X P.complex 0)))
          (_ :
            𝟙 (F.obj (HomologicalComplex.X P.complex 0)) ≫
                F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)) =
              0) ≫
        cokernel.π
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0))) ≫
      𝟙
          (cokernel
            (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
              (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
              (_ :
                HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                    HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                  0))) ≫
        cokernel.desc
          (kernel.lift (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0)))
            (F.map (HomologicalComplex.d P.complex (ComplexShape.prev (ComplexShape.down ℕ) 0) 0))
            (_ :
              HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                  HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                0))
          (kernel.ι (F.map (HomologicalComplex.d P.complex 0 (ComplexShape.next (ComplexShape.down ℕ) 0))) ≫
            F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0) ≫
                kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
              0) =
    F.map (HomologicalComplex.Hom.f P.π 0)
[PROOFSTEP]
simp only [Category.assoc, cokernel.π_desc, kernel.lift_ι_assoc, 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✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
⊢ (leftDerived F 0).map f ≫ leftDerivedZeroToSelfApp F Q = leftDerivedZeroToSelfApp F P ≫ F.map f
[PROOFSTEP]
dsimp only [leftDerivedZeroToSelfApp]
[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✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
⊢ (leftDerived F 0).map f ≫
      (leftDerivedObjIso F 0 Q).hom ≫
        homology.desc' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
          (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 =
              0)
          (kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0) ≫
            F.map (HomologicalComplex.Hom.f Q.π 0))
          (_ :
            kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
                  (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 =
                      0) ≫
                kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0) ≫
                  F.map (HomologicalComplex.Hom.f Q.π 0) =
              0) =
    ((leftDerivedObjIso F 0 P).hom ≫
        homology.desc' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
          (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)
          (kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
            F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0) ≫
                kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
              0)) ≫
      F.map f
[PROOFSTEP]
rw [Functor.leftDerived_map_eq F 0 f (ProjectiveResolution.lift f P Q) (by simp), Category.assoc, Category.assoc, ←
  Category.assoc _ (F.leftDerivedObjIso 0 Q).hom, Iso.inv_hom_id, Category.id_comp, Category.assoc, whisker_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
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
⊢ ProjectiveResolution.lift f P Q ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
[PROOFSTEP]
simp
[GOAL]
case 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✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
⊢ (homologyFunctor D (ComplexShape.down ℕ) 0).map
        ((mapHomologicalComplex F (ComplexShape.down ℕ)).map (ProjectiveResolution.lift f P Q)) ≫
      homology.desc' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 =
            0)
        (kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0) ≫
          F.map (HomologicalComplex.Hom.f Q.π 0))
        (_ :
          kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
                (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 =
                    0) ≫
              kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0) ≫
                F.map (HomologicalComplex.Hom.f Q.π 0) =
            0) =
    homology.desc' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)
        (kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
          F.map (HomologicalComplex.Hom.f P.π 0))
        (_ :
          kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0) ≫
              kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                F.map (HomologicalComplex.Hom.f P.π 0) =
            0) ≫
      F.map f
[PROOFSTEP]
dsimp only [homologyFunctor_map]
  -- Porting note: broken ext
[GOAL]
case 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✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
⊢ homology.map
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 =
            0)
        (HomologicalComplex.Hom.sqTo
          ((mapHomologicalComplex F (ComplexShape.down ℕ)).map (ProjectiveResolution.lift f P Q)) 0)
        (HomologicalComplex.Hom.sqFrom
          ((mapHomologicalComplex F (ComplexShape.down ℕ)).map (ProjectiveResolution.lift f P Q)) 0)
        (_ :
          (HomologicalComplex.Hom.sqTo
                ((mapHomologicalComplex F (ComplexShape.down ℕ)).map (ProjectiveResolution.lift f P Q)) 0).right =
            (HomologicalComplex.Hom.sqTo
                ((mapHomologicalComplex F (ComplexShape.down ℕ)).map (ProjectiveResolution.lift f P Q)) 0).right) ≫
      homology.desc' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 =
            0)
        (kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0) ≫
          F.map (HomologicalComplex.Hom.f Q.π 0))
        (_ :
          kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
                (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 =
                    0) ≫
              kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0) ≫
                F.map (HomologicalComplex.Hom.f Q.π 0) =
            0) =
    homology.desc' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0)
        (kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
          F.map (HomologicalComplex.Hom.f P.π 0))
        (_ :
          kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                (_ :
                  HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                      HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                    0) ≫
              kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                F.map (HomologicalComplex.Hom.f P.π 0) =
            0) ≫
      F.map f
[PROOFSTEP]
apply homology.hom_from_ext
[GOAL]
case w.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✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
⊢ homology.π' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0) ≫
      homology.map
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 =
              0)
          (HomologicalComplex.Hom.sqTo
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).map (ProjectiveResolution.lift f P Q)) 0)
          (HomologicalComplex.Hom.sqFrom
            ((mapHomologicalComplex F (ComplexShape.down ℕ)).map (ProjectiveResolution.lift f P Q)) 0)
          (_ :
            (HomologicalComplex.Hom.sqTo
                  ((mapHomologicalComplex F (ComplexShape.down ℕ)).map (ProjectiveResolution.lift f P Q)) 0).right =
              (HomologicalComplex.Hom.sqTo
                  ((mapHomologicalComplex F (ComplexShape.down ℕ)).map (ProjectiveResolution.lift f P Q)) 0).right) ≫
        homology.desc' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
          (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 =
              0)
          (kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0) ≫
            F.map (HomologicalComplex.Hom.f Q.π 0))
          (_ :
            kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
                  (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0 =
                      0) ≫
                kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj Q.complex) 0) ≫
                  F.map (HomologicalComplex.Hom.f Q.π 0) =
              0) =
    homology.π' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
        (_ :
          HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
              HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
            0) ≫
      homology.desc' (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
          (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
          (_ :
            HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
              0)
          (kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
            F.map (HomologicalComplex.Hom.f P.π 0))
          (_ :
            kernel.lift (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0)
                  (_ :
                    HomologicalComplex.dTo ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 ≫
                        HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0 =
                      0) ≫
                kernel.ι (HomologicalComplex.dFrom ((mapHomologicalComplex F (ComplexShape.down ℕ)).obj P.complex) 0) ≫
                  F.map (HomologicalComplex.Hom.f P.π 0) =
              0) ≫
        F.map f
[PROOFSTEP]
simp only [HomologicalComplex.Hom.sqTo_right, mapHomologicalComplex_map_f, homology.π'_map_assoc, homology.π'_desc',
  kernel.lift_ι_assoc, Category.assoc, homology.π'_desc'_assoc, ← map_comp,
  show (ProjectiveResolution.lift f P Q).f 0 ≫ _ = _ ≫ f from
    HomologicalComplex.congr_hom (ProjectiveResolution.lift_commutes f P Q) 0]
