[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : HasZeroMorphisms V
inst✝⁵ : HasZeroObject V
inst✝⁴ : HasEqualizers V
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
inst✝ : IsIso f
i : ι
⊢ IsIso ((homologyFunctor V c i).map f)
[PROOFSTEP]
change IsIso ((homologyFunctor V c i).mapIso (asIso f)).hom
[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : HasZeroMorphisms V
inst✝⁵ : HasZeroObject V
inst✝⁴ : HasEqualizers V
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
inst✝ : IsIso f
i : ι
⊢ IsIso ((homologyFunctor V c i).mapIso (asIso f)).hom
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
inst✝¹ : QuasiIso f
g : D ⟶ E
inst✝ : QuasiIso g
i : ι
⊢ IsIso ((homologyFunctor V c i).map (f ≫ g))
[PROOFSTEP]
rw [Functor.map_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
inst✝¹ : QuasiIso f
g : D ⟶ E
inst✝ : QuasiIso g
i : ι
⊢ IsIso ((homologyFunctor V c i).map f ≫ (homologyFunctor V c i).map g)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ IsIso ((homologyFunctor W c i).map e.hom)
[PROOFSTEP]
refine' ⟨⟨(homologyFunctor W c i).map e.inv, _⟩⟩
[GOAL]
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ (homologyFunctor W c i).map e.hom ≫ (homologyFunctor W c i).map e.inv = 𝟙 ((homologyFunctor W c i).obj C) ∧
    (homologyFunctor W c i).map e.inv ≫ (homologyFunctor W c i).map e.hom = 𝟙 ((homologyFunctor W c i).obj D)
[PROOFSTEP]
simp only [← Functor.map_comp, ← (homologyFunctor W c i).map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ (homologyFunctor W c i).map (e.hom ≫ e.inv) = (homologyFunctor W c i).map (𝟙 C) ∧
    (homologyFunctor W c i).map (e.inv ≫ e.hom) = (homologyFunctor W c i).map (𝟙 D)
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ (homologyFunctor W c i).map (e.hom ≫ e.inv) = (homologyFunctor W c i).map (𝟙 C)
[PROOFSTEP]
apply homology_map_eq_of_homotopy
[GOAL]
case right
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ (homologyFunctor W c i).map (e.inv ≫ e.hom) = (homologyFunctor W c i).map (𝟙 D)
[PROOFSTEP]
apply homology_map_eq_of_homotopy
[GOAL]
case left.h
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ Homotopy (e.hom ≫ e.inv) (𝟙 C)
case right.h
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ Homotopy (e.inv ≫ e.hom) (𝟙 D)
[PROOFSTEP]
exacts [e.homotopyHomInvId, e.homotopyInvHomId]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ (asIso ((homologyFunctor W c i).map e.hom)).inv = (homologyFunctor W c i).map e.inv
[PROOFSTEP]
symm
[GOAL]
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ (homologyFunctor W c i).map e.inv = (asIso ((homologyFunctor W c i).map e.hom)).inv
[PROOFSTEP]
haveI := e.toQuasiIso.1 i
[GOAL]
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
this : IsIso ((homologyFunctor W c i).map e.hom)
⊢ (homologyFunctor W c i).map e.inv = (asIso ((homologyFunctor W c i).map e.hom)).inv
[PROOFSTEP]
simp only [← Iso.hom_comp_eq_id, asIso_hom, ← Functor.map_comp, ← (homologyFunctor W c i).map_id,
  homology_map_eq_of_homotopy e.homotopyHomInvId _]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{?u.22788, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
[PROOFSTEP]
rw [← f.2 1 0 rfl]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{?u.22788, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ HomologicalComplex.Hom.f f 1 ≫ d ((ChainComplex.single₀ W).obj Y) 1 0 = 0
[PROOFSTEP]
exact comp_zero
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ (toSingle₀CokernelAtZeroIso f).hom =
    cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) (_ : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ coequalizer.π (d X 1 0) 0 ≫ (toSingle₀CokernelAtZeroIso f).hom =
    coequalizer.π (d X 1 0) 0 ≫
      cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) (_ : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0)
[PROOFSTEP]
dsimp only [toSingle₀CokernelAtZeroIso, ChainComplex.homologyZeroIso, homologyOfZeroRight, homology.mapIso,
  ChainComplex.homologyFunctor0Single₀, cokernel.map]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ coequalizer.π (d X 1 0) 0 ≫
      ((Iso.mk
                (homology.map (_ : dTo X 0 ≫ dFrom X 0 = 0) (_ : d X 1 0 ≫ 0 = 0)
                  (Arrow.isoMk (xPrevIso X ChainComplex.homologyZeroIso.proof_10)
                      (Iso.refl (Arrow.mk (dTo X 0)).right)).hom
                  (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left) (Iso.refl (Arrow.mk (dFrom X 0)).right)).hom
                  (_ :
                    (Arrow.isoMk (xPrevIso X (_ : 0 + 1 = 0 + 1)) (Iso.refl (Arrow.mk (dTo X 0)).right)).hom.right =
                      (Arrow.isoMk (xPrevIso X (_ : 0 + 1 = 0 + 1)) (Iso.refl (Arrow.mk (dTo X 0)).right)).hom.right))
                (homology.map (_ : d X 1 0 ≫ 0 = 0) (_ : dTo X 0 ≫ dFrom X 0 = 0)
                  (Arrow.isoMk (xPrevIso X ChainComplex.homologyZeroIso.proof_10)
                      (Iso.refl (Arrow.mk (dTo X 0)).right)).inv
                  (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left) (Iso.refl (Arrow.mk (dFrom X 0)).right)).inv
                  (_ :
                    (Arrow.isoMk (xPrevIso X ChainComplex.homologyZeroIso.proof_10)
                            (Iso.refl (Arrow.mk (dTo X 0)).right)).inv.right =
                      (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                            (Iso.refl (Arrow.mk (dFrom X 0)).right)).inv.left)) ≪≫
              cokernel.mapIso (imageToKernel (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0)) (image.ι (d X 1 0))
                  (imageSubobjectIso (d X 1 0)) (kernelSubobjectIso 0 ≪≫ kernelZeroIsoSource)
                  (_ :
                    imageToKernel (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0) ≫ (kernelSubobjectIso 0).hom ≫ kernel.ι 0 =
                      (imageSubobjectIso (d X 1 0)).hom ≫ image.ι (d X 1 0)) ≪≫
                cokernelImageι (d X 1 0)).symm ≪≫
          asIso ((homologyFunctor W (ComplexShape.down ℕ) 0).map f) ≪≫
            (NatIso.ofComponents fun X =>
                  homology.congr
                      (_ : dTo ((ChainComplex.single₀ W).obj X) 0 ≫ dFrom ((ChainComplex.single₀ W).obj X) 0 = 0)
                      (_ : 0 ≫ 0 = 0) (_ : 0 = 0)
                      (_ : d ((ChainComplex.single₀ W).obj X) 0 (ComplexShape.next (ComplexShape.down ℕ) 0) = 0) ≪≫
                    homologyZeroZero).app
              Y).hom =
    coequalizer.π (d X 1 0) 0 ≫
      cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) (_ : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0)
[PROOFSTEP]
dsimp [asIso]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ cokernel.π (d X 1 0) ≫
      ((cokernel.desc (d X 1 0) (cokernel.π (image.ι (d X 1 0))) (_ : d X 1 0 ≫ cokernel.π (image.ι (d X 1 0)) = 0) ≫
            cokernel.map (image.ι (d X 1 0)) (imageToKernel (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0))
              (imageSubobjectIso (d X 1 0)).inv (kernelZeroIsoSource.inv ≫ (kernelSubobjectIso 0).inv)
              (_ :
                image.ι (d X 1 0) ≫ (kernelSubobjectIso 0 ≪≫ kernelZeroIsoSource).inv =
                  (imageSubobjectIso (d X 1 0)).inv ≫ imageToKernel (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0))) ≫
          homology.map (_ : d X 1 0 ≫ 0 = 0) (_ : dTo X 0 ≫ dFrom X 0 = 0)
            (Arrow.isoMk (xPrevIso X ChainComplex.homologyZeroIso.proof_10) (Iso.refl (HomologicalComplex.X X 0))).inv
            (Arrow.isoMk (Iso.refl (HomologicalComplex.X X 0)) (Iso.refl (xNext X 0))).inv
            (_ :
              (Arrow.isoMk (xPrevIso X ChainComplex.homologyZeroIso.proof_10)
                      (Iso.refl (HomologicalComplex.X X 0))).inv.right =
                (Arrow.isoMk (Iso.refl (HomologicalComplex.X X 0)) (Iso.refl (xNext X 0))).inv.left)) ≫
        homology.map (_ : dTo X 0 ≫ dFrom X 0 = 0)
            (_ : dTo ((ChainComplex.single₀ W).obj Y) 0 ≫ dFrom ((ChainComplex.single₀ W).obj Y) 0 = 0) (sqTo f 0)
            (sqFrom f 0) (_ : (sqTo f 0).right = (sqTo f 0).right) ≫
          homology.map (_ : dTo ((ChainComplex.single₀ W).obj Y) 0 ≫ dFrom ((ChainComplex.single₀ W).obj Y) 0 = 0)
              (_ : 0 ≫ 0 = 0) (CommaMorphism.mk (𝟙 (xPrev ((ChainComplex.single₀ W).obj Y) 0)) (𝟙 Y))
              (CommaMorphism.mk (𝟙 Y) (𝟙 (xNext ((ChainComplex.single₀ W).obj Y) 0)))
              (_ :
                (CommaMorphism.mk (𝟙 (Arrow.mk 0).left) (𝟙 (Arrow.mk 0).right)).right =
                  (CommaMorphism.mk (𝟙 (Arrow.mk 0).left) (𝟙 (Arrow.mk 0).right)).right) ≫
            homology.desc 0 0 (_ : 0 ≫ 0 = 0) (Subobject.arrow (kernelSubobject 0))
              (_ : imageToKernel 0 0 (_ : 0 ≫ 0 = 0) ≫ Subobject.arrow (kernelSubobject 0) = 0) =
    cokernel.π (d X 1 0) ≫
      cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) (_ : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0)
[PROOFSTEP]
simp only [cokernel.π_desc, Category.assoc, homology.map_desc, cokernel.π_desc_assoc]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ kernelZeroIsoSource.inv ≫
      (kernelSubobjectIso 0).inv ≫
        cokernel.π (imageToKernel (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0)) ≫
          homology.desc (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0)
            (kernelSubobjectMap (Arrow.isoMk (Iso.refl (HomologicalComplex.X X 0)) (Iso.refl (xNext X 0))).inv ≫
              kernelSubobjectMap (sqFrom f 0) ≫
                kernelSubobjectMap (CommaMorphism.mk (𝟙 Y) (𝟙 (xNext ((ChainComplex.single₀ W).obj Y) 0))) ≫
                  Subobject.arrow (kernelSubobject 0))
            (_ :
              imageToKernel (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0) ≫
                  kernelSubobjectMap (Arrow.isoMk (Iso.refl (HomologicalComplex.X X 0)) (Iso.refl (xNext X 0))).inv ≫
                    kernelSubobjectMap (sqFrom f 0) ≫
                      kernelSubobjectMap (CommaMorphism.mk (𝟙 Y) (𝟙 (xNext ((ChainComplex.single₀ W).obj Y) 0))) ≫
                        Subobject.arrow (kernelSubobject 0) =
                0) =
    HomologicalComplex.Hom.f f 0
[PROOFSTEP]
simp [homology.desc, Iso.refl_inv (X.X 0)]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ Epi (HomologicalComplex.Hom.f f 0)
[PROOFSTEP]
constructor
[GOAL]
case left_cancellation
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ ∀ {Z : W} (g h : HomologicalComplex.X ((ChainComplex.single₀ W).obj Y) 0 ⟶ Z),
    HomologicalComplex.Hom.f f 0 ≫ g = HomologicalComplex.Hom.f f 0 ≫ h → g = h
[PROOFSTEP]
intro Z g h Hgh
[GOAL]
case left_cancellation
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
Z : W
g h : HomologicalComplex.X ((ChainComplex.single₀ W).obj Y) 0 ⟶ Z
Hgh : HomologicalComplex.Hom.f f 0 ≫ g = HomologicalComplex.Hom.f f 0 ≫ h
⊢ g = h
[PROOFSTEP]
rw [← cokernel.π_desc (X.d 1 0) (f.f 0) (by rw [← f.2 1 0 rfl]; exact comp_zero), ←
  toSingle₀CokernelAtZeroIso_hom_eq] at Hgh 
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
Z : W
g h : HomologicalComplex.X ((ChainComplex.single₀ W).obj Y) 0 ⟶ Z
Hgh : HomologicalComplex.Hom.f f 0 ≫ g = HomologicalComplex.Hom.f f 0 ≫ h
⊢ d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
[PROOFSTEP]
rw [← f.2 1 0 rfl]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
Z : W
g h : HomologicalComplex.X ((ChainComplex.single₀ W).obj Y) 0 ⟶ Z
Hgh : HomologicalComplex.Hom.f f 0 ≫ g = HomologicalComplex.Hom.f f 0 ≫ h
⊢ HomologicalComplex.Hom.f f 1 ≫ d ((ChainComplex.single₀ W).obj Y) 1 0 = 0
[PROOFSTEP]
exact comp_zero
[GOAL]
case left_cancellation
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
Z : W
g h : HomologicalComplex.X ((ChainComplex.single₀ W).obj Y) 0 ⟶ Z
Hgh✝ : HomologicalComplex.Hom.f f 0 ≫ g = HomologicalComplex.Hom.f f 0 ≫ h
Hgh :
  (cokernel.π (d X 1 0) ≫ (toSingle₀CokernelAtZeroIso f).hom) ≫ g =
    (cokernel.π (d X 1 0) ≫ (toSingle₀CokernelAtZeroIso f).hom) ≫ h
⊢ g = h
[PROOFSTEP]
rw [(@cancel_epi _ _ _ _ _ _ (epi_comp _ _) _ _).1 Hgh]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ Exact (d X 1 0) (HomologicalComplex.Hom.f f 0)
[PROOFSTEP]
rw [Preadditive.exact_iff_homology_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ ∃ w, Nonempty (_root_.homology (d X 1 0) (HomologicalComplex.Hom.f f 0) w ≅ 0)
[PROOFSTEP]
have h : X.d 1 0 ≫ f.f 0 = 0 := by simp only [← f.2 1 0 rfl, ChainComplex.single₀_obj_X_d, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
[PROOFSTEP]
simp only [← f.2 1 0 rfl, ChainComplex.single₀_obj_X_d, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ ∃ w, Nonempty (_root_.homology (d X 1 0) (HomologicalComplex.Hom.f f 0) w ≅ 0)
[PROOFSTEP]
refine' ⟨h, Nonempty.intro (homologyIsoKernelDesc _ _ _ ≪≫ _)⟩
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ kernel (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h) ≅ 0
[PROOFSTEP]
suffices IsIso (cokernel.desc _ _ h) by apply kernel.ofMono
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
this : IsIso (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h)
⊢ kernel (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h) ≅ 0
[PROOFSTEP]
apply kernel.ofMono
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ IsIso (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h)
[PROOFSTEP]
rw [← toSingle₀CokernelAtZeroIso_hom_eq]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ IsIso (toSingle₀CokernelAtZeroIso f).hom
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{?u.68820, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
[PROOFSTEP]
rw [f.2 0 1 rfl]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{?u.68820, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ d ((CochainComplex.single₀ W).obj Y) 0 1 ≫ HomologicalComplex.Hom.f f 1 = 0
[PROOFSTEP]
exact zero_comp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ (fromSingle₀KernelAtZeroIso f).inv =
    kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) (_ : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ (fromSingle₀KernelAtZeroIso f).inv ≫ equalizer.ι (d X 0 1) 0 =
    kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) (_ : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0) ≫
      equalizer.ι (d X 0 1) 0
[PROOFSTEP]
dsimp only [fromSingle₀KernelAtZeroIso, CochainComplex.homologyZeroIso, homologyOfZeroLeft, homology.mapIso,
  CochainComplex.homologyFunctor0Single₀, kernel.map]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ ((Iso.mk
                (homology.map (_ : dTo X 0 ≫ dFrom X 0 = 0) (_ : 0 ≫ d X 0 1 = 0)
                  (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                      (Iso.refl (Arrow.mk (dTo X 0)).right)).hom
                  (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                      (xNextIso X CochainComplex.homologyZeroIso.proof_11)).hom
                  (_ : 𝟙 (HomologicalComplex.X X 0) = 𝟙 (HomologicalComplex.X X 0)))
                (homology.map (_ : 0 ≫ d X 0 1 = 0) (_ : dTo X 0 ≫ dFrom X 0 = 0)
                  (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                      (Iso.refl (Arrow.mk (dTo X 0)).right)).inv
                  (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                      (xNextIso X CochainComplex.homologyZeroIso.proof_11)).inv
                  (_ :
                    (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                            (Iso.refl (Arrow.mk (dTo X 0)).right)).inv.right =
                      (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                            (xNextIso X CochainComplex.homologyZeroIso.proof_11)).inv.left)) ≪≫
              (cokernelIsoOfEq (_ : imageToKernel 0 (d X 0 1) (_ : 0 ≫ d X 0 1 = 0) = 0) ≪≫ cokernelZeroIsoTarget) ≪≫
                kernelSubobjectIso (d X 0 1)).symm ≪≫
          (asIso ((homologyFunctor W (ComplexShape.up ℕ) 0).map f)).symm ≪≫
            (NatIso.ofComponents fun X =>
                  homology.congr
                      (_ : dTo ((CochainComplex.single₀ W).obj X) 0 ≫ dFrom ((CochainComplex.single₀ W).obj X) 0 = 0)
                      (_ : 0 ≫ 0 = 0)
                      (_ : d ((CochainComplex.single₀ W).obj X) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 = 0)
                      (_ : 0 = 0) ≪≫
                    homologyZeroZero).app
              Y).inv ≫
      equalizer.ι (d X 0 1) 0 =
    kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) (_ : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0) ≫
      equalizer.ι (d X 0 1) 0
[PROOFSTEP]
simp only [Iso.trans_inv, Iso.app_inv, Iso.symm_inv, Category.assoc, equalizer_as_kernel, kernel.lift_ι]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ NatTrans.app
        (NatIso.ofComponents fun X =>
            homology.congr
                (_ : dTo ((CochainComplex.single₀ W).obj X) 0 ≫ dFrom ((CochainComplex.single₀ W).obj X) 0 = 0)
                (_ : 0 ≫ 0 = 0)
                (_ : d ((CochainComplex.single₀ W).obj X) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 = 0)
                (_ : 0 = 0) ≪≫
              homologyZeroZero).inv
        Y ≫
      (asIso ((homologyFunctor W (ComplexShape.up ℕ) 0).map f)).hom ≫
        (Iso.mk
                (homology.map (_ : dTo X 0 ≫ dFrom X 0 = 0) (_ : 0 ≫ d X 0 1 = 0)
                  (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                      (Iso.refl (Arrow.mk (dTo X 0)).right)).hom
                  (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                      (xNextIso X CochainComplex.homologyZeroIso.proof_11)).hom
                  (_ : 𝟙 (HomologicalComplex.X X 0) = 𝟙 (HomologicalComplex.X X 0)))
                (homology.map (_ : 0 ≫ d X 0 1 = 0) (_ : dTo X 0 ≫ dFrom X 0 = 0)
                  (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                      (Iso.refl (Arrow.mk (dTo X 0)).right)).inv
                  (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                      (xNextIso X CochainComplex.homologyZeroIso.proof_11)).inv
                  (_ :
                    (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                            (Iso.refl (Arrow.mk (dTo X 0)).right)).inv.right =
                      (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                            (xNextIso X CochainComplex.homologyZeroIso.proof_11)).inv.left)) ≪≫
              (cokernelIsoOfEq (_ : imageToKernel 0 (d X 0 1) (_ : 0 ≫ d X 0 1 = 0) = 0) ≪≫ cokernelZeroIsoTarget) ≪≫
                kernelSubobjectIso (d X 0 1)).hom ≫
          kernel.ι (d X 0 1) =
    HomologicalComplex.Hom.f f 0
[PROOFSTEP]
dsimp [asIso]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ ((inv (Subobject.arrow (kernelSubobject 0)) ≫ homology.π 0 0 (_ : 0 ≫ 0 = 0)) ≫
        homology.map (_ : 0 ≫ 0 = 0)
          (_ : dTo ((CochainComplex.single₀ W).obj Y) 0 ≫ dFrom ((CochainComplex.single₀ W).obj Y) 0 = 0)
          (CommaMorphism.mk (𝟙 (xPrev ((CochainComplex.single₀ W).obj Y) 0)) (𝟙 Y))
          (CommaMorphism.mk (𝟙 Y) (𝟙 (xNext ((CochainComplex.single₀ W).obj Y) 0)))
          (_ :
            (CommaMorphism.mk (𝟙 (Arrow.mk 0).left) (𝟙 (Arrow.mk 0).right)).right =
              (CommaMorphism.mk (𝟙 (Arrow.mk 0).left) (𝟙 (Arrow.mk 0).right)).right)) ≫
      homology.map (_ : dTo ((CochainComplex.single₀ W).obj Y) 0 ≫ dFrom ((CochainComplex.single₀ W).obj Y) 0 = 0)
          (_ : dTo X 0 ≫ dFrom X 0 = 0) (sqTo f 0) (sqFrom f 0) (_ : (sqTo f 0).right = (sqTo f 0).right) ≫
        (homology.map (_ : dTo X 0 ≫ dFrom X 0 = 0) (_ : 0 ≫ d X 0 1 = 0)
              (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                  (Iso.refl (HomologicalComplex.X X 0))).hom
              (Arrow.isoMk (Iso.refl (HomologicalComplex.X X 0))
                  (xNextIso X CochainComplex.homologyZeroIso.proof_11)).hom
              (_ : 𝟙 (HomologicalComplex.X X 0) = 𝟙 (HomologicalComplex.X X 0)) ≫
            ((cokernelIsoOfEq (_ : imageToKernel 0 (d X 0 1) (_ : 0 ≫ d X 0 1 = 0) = 0)).hom ≫
                cokernelZeroIsoTarget.hom) ≫
              (kernelSubobjectIso (d X 0 1)).hom) ≫
          kernel.ι (d X 0 1) =
    HomologicalComplex.Hom.f f 0
[PROOFSTEP]
simp only [Category.assoc, homology.π_map, cokernelZeroIsoTarget_hom, cokernelIsoOfEq_hom_comp_desc,
  kernelSubobject_arrow, homology.π_map_assoc, IsIso.inv_comp_eq]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ kernelSubobjectMap (CommaMorphism.mk (𝟙 Y) (𝟙 (xNext ((CochainComplex.single₀ W).obj Y) 0))) ≫
      kernelSubobjectMap (sqFrom f 0) ≫
        kernelSubobjectMap
            (Arrow.isoMk (Iso.refl (HomologicalComplex.X X 0))
                (xNextIso X CochainComplex.homologyZeroIso.proof_11)).hom ≫
          homology.π 0 (d X 0 1) (_ : 0 ≫ d X 0 1 = 0) ≫
            cokernel.desc (imageToKernel 0 (d X 0 1) (_ : 0 ≫ d X 0 1 = 0))
                (𝟙 (Subobject.underlying.obj (kernelSubobject (d X 0 1))))
                (_ :
                  imageToKernel 0 (d X 0 1) (_ : 0 ≫ d X 0 1 = 0) ≫
                      𝟙 (Subobject.underlying.obj (kernelSubobject (d X 0 1))) =
                    0) ≫
              Subobject.arrow (kernelSubobject (d X 0 1)) =
    Subobject.arrow (kernelSubobject 0) ≫ HomologicalComplex.Hom.f f 0
[PROOFSTEP]
simp [homology.π, kernelSubobjectMap_comp, Iso.refl_hom (X.X 0), Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ Mono (HomologicalComplex.Hom.f f 0)
[PROOFSTEP]
constructor
[GOAL]
case right_cancellation
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ ∀ {Z : W} (g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0),
    g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0 → g = h
[PROOFSTEP]
intro Z g h Hgh
[GOAL]
case right_cancellation
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
⊢ g = h
[PROOFSTEP]
rw [← kernel.lift_ι (X.d 0 1) (f.f 0) (by rw [f.2 0 1 rfl]; exact zero_comp), ← fromSingle₀KernelAtZeroIso_inv_eq] at
  Hgh 
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
⊢ HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
[PROOFSTEP]
rw [f.2 0 1 rfl]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
⊢ d ((CochainComplex.single₀ W).obj Y) 0 1 ≫ HomologicalComplex.Hom.f f 1 = 0
[PROOFSTEP]
exact zero_comp
[GOAL]
case right_cancellation
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh✝ : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
Hgh :
  g ≫ (fromSingle₀KernelAtZeroIso f).inv ≫ kernel.ι (d X 0 1) =
    h ≫ (fromSingle₀KernelAtZeroIso f).inv ≫ kernel.ι (d X 0 1)
⊢ g = h
[PROOFSTEP]
rw [(@cancel_mono _ _ _ _ _ _ (mono_comp _ _) _ _).1 Hgh]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ Exact (HomologicalComplex.Hom.f f 0) (d X 0 1)
[PROOFSTEP]
rw [Preadditive.exact_iff_homology_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ ∃ w, Nonempty (_root_.homology (HomologicalComplex.Hom.f f 0) (d X 0 1) w ≅ 0)
[PROOFSTEP]
have h : f.f 0 ≫ X.d 0 1 = 0 := by simp only [HomologicalComplex.Hom.comm, CochainComplex.single₀_obj_X_d, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
[PROOFSTEP]
simp only [HomologicalComplex.Hom.comm, CochainComplex.single₀_obj_X_d, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ ∃ w, Nonempty (_root_.homology (HomologicalComplex.Hom.f f 0) (d X 0 1) w ≅ 0)
[PROOFSTEP]
refine' ⟨h, Nonempty.intro (homologyIsoCokernelLift _ _ _ ≪≫ _)⟩
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ cokernel (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h) ≅ 0
[PROOFSTEP]
suffices IsIso (kernel.lift (X.d 0 1) (f.f 0) h) by apply cokernel.ofEpi
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
this : IsIso (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h)
⊢ cokernel (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h) ≅ 0
[PROOFSTEP]
apply cokernel.ofEpi
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ IsIso (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h)
[PROOFSTEP]
rw [← fromSingle₀KernelAtZeroIso_inv_eq f]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ IsIso (fromSingle₀KernelAtZeroIso f).inv
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁴ : Category.{v, u} V
inst✝¹³ : HasZeroMorphisms V
inst✝¹² : HasZeroObject V
inst✝¹¹ : HasEqualizers V
inst✝¹⁰ : HasImages V
inst✝⁹ : HasImageMaps V
inst✝⁸ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
A : Type u_2
inst✝⁷ : Category.{u_4, u_2} A
inst✝⁶ : Abelian A
B : Type u_3
inst✝⁵ : Category.{u_5, u_3} B
inst✝⁴ : Abelian B
F : A ⥤ B
inst✝³ : Additive F
inst✝² : PreservesFiniteLimits F
inst✝¹ : PreservesFiniteColimits F
inst✝ : Faithful F
C D : HomologicalComplex A c
f : C ⟶ D
hf : QuasiIso ((mapHomologicalComplex F c).map f)
i : ι
⊢ IsIso (F.map ((homologyFunctor A c i).map f))
[PROOFSTEP]
rw [← Functor.comp_map, ← NatIso.naturality_2 (F.homologyFunctorIso i) f, Functor.comp_map]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁴ : Category.{v, u} V
inst✝¹³ : HasZeroMorphisms V
inst✝¹² : HasZeroObject V
inst✝¹¹ : HasEqualizers V
inst✝¹⁰ : HasImages V
inst✝⁹ : HasImageMaps V
inst✝⁸ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
A : Type u_2
inst✝⁷ : Category.{u_4, u_2} A
inst✝⁶ : Abelian A
B : Type u_3
inst✝⁵ : Category.{u_5, u_3} B
inst✝⁴ : Abelian B
F : A ⥤ B
inst✝³ : Additive F
inst✝² : PreservesFiniteLimits F
inst✝¹ : PreservesFiniteColimits F
inst✝ : Faithful F
C D : HomologicalComplex A c
f : C ⟶ D
hf : QuasiIso ((mapHomologicalComplex F c).map f)
i : ι
⊢ IsIso
    (NatTrans.app (homologyFunctorIso F i).hom C ≫
      (homologyFunctor B c i).map ((mapHomologicalComplex F c).map f) ≫ NatTrans.app (homologyFunctorIso F i).inv D)
[PROOFSTEP]
infer_instance
