[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ cycles C i = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ ⊤ ≤ cycles C i
[PROOFSTEP]
apply le_kernelSubobject
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ Subobject.arrow ⊤ ≫ dFrom C i = 0
[PROOFSTEP]
rw [C.dFrom_eq_zero h, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasZeroObject V
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ boundaries C j = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasZeroObject V
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ boundaries C j ≤ ⊥
[PROOFSTEP]
refine' imageSubobject_le _ 0 _
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasZeroObject V
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ 0 ≫ Subobject.arrow ⊥ = dTo C j
[PROOFSTEP]
rw [C.dTo_eq_zero h, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ComplexShape.Rel c j k
⊢ (xPrevIso C hij).hom ≫ (Arrow.mk (d C i j)).hom = (Arrow.mk (dTo C j)).hom ≫ (Iso.refl (Arrow.mk (dTo C j)).right).hom
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ComplexShape.Rel c j k
⊢ (xPrevIso C hij).hom ≫ d C i j = dTo C j ≫ 𝟙 (X C j)
[PROOFSTEP]
rw [C.dTo_eq hij, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ComplexShape.Rel c j k
⊢ (Iso.refl (Arrow.mk (dFrom C j)).left).hom ≫ (Arrow.mk (d C j k)).hom =
    (Arrow.mk (dFrom C j)).hom ≫ (xNextIso C hjk).hom
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ComplexShape.Rel c j k
⊢ 𝟙 (X C j) ≫ d C j k = dFrom C j ≫ (xNextIso C hjk).hom
[PROOFSTEP]
rw [C.dFrom_comp_xNextIso hjk, Category.id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
C : ChainComplex V ℕ
inst✝ : Epi (factorThruImage (HomologicalComplex.d C 1 0))
⊢ (HomologicalComplex.xPrevIso C (_ : 0 + 1 = 0 + 1)).hom ≫ (Arrow.mk (HomologicalComplex.d C 1 0)).hom =
    (Arrow.mk (HomologicalComplex.dTo C 0)).hom ≫ (Iso.refl (Arrow.mk (HomologicalComplex.dTo C 0)).right).hom
[PROOFSTEP]
rw [C.dTo_eq rfl]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
C : ChainComplex V ℕ
inst✝ : Epi (factorThruImage (HomologicalComplex.d C 1 0))
⊢ (HomologicalComplex.xPrevIso C (_ : 0 + 1 = 0 + 1)).hom ≫ (Arrow.mk (HomologicalComplex.d C 1 0)).hom =
    (Arrow.mk ((HomologicalComplex.xPrevIso C (_ : 0 + 1 = 0 + 1)).hom ≫ HomologicalComplex.d C (0 + 1) 0)).hom ≫
      (Iso.refl
          (Arrow.mk
              ((HomologicalComplex.xPrevIso C (_ : 0 + 1 = 0 + 1)).hom ≫ HomologicalComplex.d C (0 + 1) 0)).right).hom
[PROOFSTEP]
exact (Category.comp_id _).symm
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
C : ChainComplex V ℕ
inst✝ : Epi (factorThruImage (HomologicalComplex.d C 1 0))
⊢ (Iso.refl (Arrow.mk (HomologicalComplex.dFrom C 0)).left).hom ≫ (Arrow.mk 0).hom =
    (Arrow.mk (HomologicalComplex.dFrom C 0)).hom ≫ (Iso.refl (Arrow.mk (HomologicalComplex.dFrom C 0)).right).hom
[PROOFSTEP]
simp [C.dFrom_eq_zero fun h : _ = _ => one_ne_zero <| by rwa [ChainComplex.next_nat_zero, Nat.zero_add] at h ]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
C : ChainComplex V ℕ
inst✝ : Epi (factorThruImage (HomologicalComplex.d C 1 0))
h : ComplexShape.next (ComplexShape.down ℕ) ?m.17177 + 1 = ?m.17177
⊢ 1 = 0
[PROOFSTEP]
rwa [ChainComplex.next_nat_zero, Nat.zero_add] at h 
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasZeroObject V
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : CochainComplex V ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0
[PROOFSTEP]
rw [CochainComplex.prev_nat_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasZeroObject V
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : CochainComplex V ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) 0 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasZeroObject V
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : CochainComplex V ℕ
⊢ (HomologicalComplex.xPrevIsoSelf C
          (_ : ¬ComplexShape.Rel (ComplexShape.up ℕ) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)).hom ≫
      (Arrow.mk 0).hom =
    (Arrow.mk (HomologicalComplex.dTo C 0)).hom ≫ (Iso.refl (Arrow.mk (HomologicalComplex.dTo C 0)).right).hom
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasZeroObject V
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : CochainComplex V ℕ
⊢ (Iso.refl (Arrow.mk (HomologicalComplex.dFrom C 0)).left).hom ≫ (Arrow.mk (HomologicalComplex.d C 0 1)).hom =
    (Arrow.mk (HomologicalComplex.dFrom C 0)).hom ≫ (HomologicalComplex.xNextIso C (_ : 0 + 1 = 0 + 1)).hom
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasZeroObject V
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : CochainComplex V ℕ
⊢ (Arrow.isoMk
          (HomologicalComplex.xPrevIsoSelf C
            (_ : ¬ComplexShape.Rel (ComplexShape.up ℕ) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (Iso.refl (Arrow.mk (HomologicalComplex.dTo C 0)).right)).hom.right =
    (Arrow.isoMk (Iso.refl (Arrow.mk (HomologicalComplex.dFrom C 0)).left)
          (HomologicalComplex.xNextIso C (_ : 0 + 1 = 0 + 1))).hom.left
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f✝ f : C₁ ⟶ C₂
i : ι
⊢ (Subobject.arrow (cycles C₁ i) ≫ Hom.f f i) ≫ dFrom C₂ i = 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f✝ f : C₁ ⟶ C₂
i : ι
⊢ cyclesMap f i ≫ Subobject.arrow (cycles C₂ i) = Subobject.arrow (cycles C₁ i) ≫ Hom.f f i
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ cyclesMap (𝟙 C₁) i = 𝟙 (Subobject.underlying.obj (cycles C₁ i))
[PROOFSTEP]
dsimp only [cyclesMap]
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ Subobject.factorThru (cycles C₁ i) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (𝟙 C₁) i)
      (_ : Subobject.Factors (kernelSubobject (dFrom C₁ i)) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (𝟙 C₁) i)) =
    𝟙 (Subobject.underlying.obj (cycles C₁ i))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f✝ f : C₁ ⟶ C₂
g : C₂ ⟶ C₃
i : ι
⊢ cyclesMap (f ≫ g) i = cyclesMap f i ≫ cyclesMap g i
[PROOFSTEP]
dsimp only [cyclesMap]
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f✝ f : C₁ ⟶ C₂
g : C₂ ⟶ C₃
i : ι
⊢ Subobject.factorThru (cycles C₃ i) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (f ≫ g) i)
      (_ : Subobject.Factors (kernelSubobject (dFrom C₃ i)) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (f ≫ g) i)) =
    Subobject.factorThru (cycles C₂ i) (Subobject.arrow (cycles C₁ i) ≫ Hom.f f i)
        (_ : Subobject.Factors (kernelSubobject (dFrom C₂ i)) (Subobject.arrow (cycles C₁ i) ≫ Hom.f f i)) ≫
      Subobject.factorThru (cycles C₃ i) (Subobject.arrow (cycles C₂ i) ≫ Hom.f g i)
        (_ : Subobject.Factors (kernelSubobject (dFrom C₃ i)) (Subobject.arrow (cycles C₂ i) ≫ Hom.f g i))
[PROOFSTEP]
simp [Subobject.factorThru_right]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝² : HasEqualizers V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ boundariesMap f i ≫ boundariesToCycles C₂ i = boundariesToCycles C₁ i ≫ cyclesMap f i
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝² : HasEqualizers V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ (boundariesMap f i ≫ boundariesToCycles C₂ i) ≫ Subobject.arrow (cycles C₂ i) =
    (boundariesToCycles C₁ i ≫ cyclesMap f i) ≫ Subobject.arrow (cycles C₂ i)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
i : ι
x✝ : HomologicalComplex V c
⊢ { obj := fun C => HomologicalComplex.homology C i,
          map := fun {C₁ C₂} f =>
            homology.map (_ : dTo C₁ i ≫ dFrom C₁ i = 0) (_ : dTo C₂ i ≫ dFrom C₂ i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
              (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) }.map
      (𝟙 x✝) =
    𝟙
      ({ obj := fun C => HomologicalComplex.homology C i,
            map := fun {C₁ C₂} f =>
              homology.map (_ : dTo C₁ i ≫ dFrom C₁ i = 0) (_ : dTo C₂ i ≫ dFrom C₂ i = 0) (Hom.sqTo f i)
                (Hom.sqFrom f i) (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) }.obj
        x✝)
[PROOFSTEP]
simp only
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
i : ι
x✝ : HomologicalComplex V c
⊢ homology.map (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo (𝟙 x✝) i) (Hom.sqFrom (𝟙 x✝) i)
      (_ : (Hom.sqTo (𝟙 x✝) i).right = (Hom.sqTo (𝟙 x✝) i).right) =
    𝟙 (HomologicalComplex.homology x✝ i)
[PROOFSTEP]
ext1
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
i : ι
x✝ : HomologicalComplex V c
⊢ homology.π (dTo x✝ i) (dFrom x✝ i) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) ≫
      homology.map (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo (𝟙 x✝) i)
        (Hom.sqFrom (𝟙 x✝) i) (_ : (Hom.sqTo (𝟙 x✝) i).right = (Hom.sqTo (𝟙 x✝) i).right) =
    homology.π (dTo x✝ i) (dFrom x✝ i) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) ≫ 𝟙 (HomologicalComplex.homology x✝ i)
[PROOFSTEP]
simp only [homology.π_map, kernelSubobjectMap_id, Hom.sqFrom_id, Category.id_comp, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
i : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { obj := fun C => HomologicalComplex.homology C i,
          map := fun {C₁ C₂} f =>
            homology.map (_ : dTo C₁ i ≫ dFrom C₁ i = 0) (_ : dTo C₂ i ≫ dFrom C₂ i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
              (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) }.map
      (x✝¹ ≫ x✝) =
    { obj := fun C => HomologicalComplex.homology C i,
            map := fun {C₁ C₂} f =>
              homology.map (_ : dTo C₁ i ≫ dFrom C₁ i = 0) (_ : dTo C₂ i ≫ dFrom C₂ i = 0) (Hom.sqTo f i)
                (Hom.sqFrom f i) (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) }.map
        x✝¹ ≫
      { obj := fun C => HomologicalComplex.homology C i,
            map := fun {C₁ C₂} f =>
              homology.map (_ : dTo C₁ i ≫ dFrom C₁ i = 0) (_ : dTo C₂ i ≫ dFrom C₂ i = 0) (Hom.sqTo f i)
                (Hom.sqFrom f i) (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) }.map
        x✝
[PROOFSTEP]
simp only
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
i : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ homology.map (_ : dTo X✝ i ≫ dFrom X✝ i = 0) (_ : dTo Z✝ i ≫ dFrom Z✝ i = 0) (Hom.sqTo (x✝¹ ≫ x✝) i)
      (Hom.sqFrom (x✝¹ ≫ x✝) i) (_ : (Hom.sqTo (x✝¹ ≫ x✝) i).right = (Hom.sqTo (x✝¹ ≫ x✝) i).right) =
    homology.map (_ : dTo X✝ i ≫ dFrom X✝ i = 0) (_ : dTo Y✝ i ≫ dFrom Y✝ i = 0) (Hom.sqTo x✝¹ i) (Hom.sqFrom x✝¹ i)
        (_ : (Hom.sqTo x✝¹ i).right = (Hom.sqTo x✝¹ i).right) ≫
      homology.map (_ : dTo Y✝ i ≫ dFrom Y✝ i = 0) (_ : dTo Z✝ i ≫ dFrom Z✝ i = 0) (Hom.sqTo x✝ i) (Hom.sqFrom x✝ i)
        (_ : (Hom.sqTo x✝ i).right = (Hom.sqTo x✝ i).right)
[PROOFSTEP]
ext1
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
i : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ homology.π (dTo X✝ i) (dFrom X✝ i) (_ : dTo X✝ i ≫ dFrom X✝ i = 0) ≫
      homology.map (_ : dTo X✝ i ≫ dFrom X✝ i = 0) (_ : dTo Z✝ i ≫ dFrom Z✝ i = 0) (Hom.sqTo (x✝¹ ≫ x✝) i)
        (Hom.sqFrom (x✝¹ ≫ x✝) i) (_ : (Hom.sqTo (x✝¹ ≫ x✝) i).right = (Hom.sqTo (x✝¹ ≫ x✝) i).right) =
    homology.π (dTo X✝ i) (dFrom X✝ i) (_ : dTo X✝ i ≫ dFrom X✝ i = 0) ≫
      homology.map (_ : dTo X✝ i ≫ dFrom X✝ i = 0) (_ : dTo Y✝ i ≫ dFrom Y✝ i = 0) (Hom.sqTo x✝¹ i) (Hom.sqFrom x✝¹ i)
          (_ : (Hom.sqTo x✝¹ i).right = (Hom.sqTo x✝¹ i).right) ≫
        homology.map (_ : dTo Y✝ i ≫ dFrom Y✝ i = 0) (_ : dTo Z✝ i ≫ dFrom Z✝ i = 0) (Hom.sqTo x✝ i) (Hom.sqFrom x✝ i)
          (_ : (Hom.sqTo x✝ i).right = (Hom.sqTo x✝ i).right)
[PROOFSTEP]
simp only [Hom.sqFrom_comp, kernelSubobjectMap_comp, homology.π_map_assoc, homology.π_map, Category.assoc]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
x✝ : HomologicalComplex V c
⊢ { obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
      (𝟙 x✝) =
    𝟙
      ({ obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.obj
        x✝)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
x✝¹ : HomologicalComplex V c
x✝ : ι
⊢ { obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
      (𝟙 x✝¹) x✝ =
    𝟙
      ({ obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.obj
        x✝¹)
      x✝
[PROOFSTEP]
simp only [GradedObject.categoryOfGradedObjects_id]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
x✝¹ : HomologicalComplex V c
x✝ : ι
⊢ (homologyFunctor V c x✝).map (𝟙 x✝¹) = 𝟙 (HomologicalComplex.homology x✝¹ x✝)
[PROOFSTEP]
ext
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
x✝¹ : HomologicalComplex V c
x✝ : ι
⊢ homology.π (dTo x✝¹ x✝) (dFrom x✝¹ x✝) (_ : dTo x✝¹ x✝ ≫ dFrom x✝¹ x✝ = 0) ≫ (homologyFunctor V c x✝).map (𝟙 x✝¹) =
    homology.π (dTo x✝¹ x✝) (dFrom x✝¹ x✝) (_ : dTo x✝¹ x✝ ≫ dFrom x✝¹ x✝ = 0) ≫ 𝟙 (HomologicalComplex.homology x✝¹ x✝)
[PROOFSTEP]
simp only [homology.π_map, homologyFunctor_map, kernelSubobjectMap_id, Hom.sqFrom_id, Category.id_comp,
  Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
      (x✝¹ ≫ x✝) =
    { obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
        x✝¹ ≫
      { obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
        x✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ι
⊢ { obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
      (x✝² ≫ x✝¹) x✝ =
    ({ obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
          x✝² ≫
        { obj := fun C i => HomologicalComplex.homology C i,
              map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
          x✝¹)
      x✝
[PROOFSTEP]
simp only [GradedObject.categoryOfGradedObjects_comp]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ι
⊢ (homologyFunctor V c x✝).map (x✝² ≫ x✝¹) = (homologyFunctor V c x✝).map x✝² ≫ (homologyFunctor V c x✝).map x✝¹
[PROOFSTEP]
ext
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ι
⊢ homology.π (dTo X✝ x✝) (dFrom X✝ x✝) (_ : dTo X✝ x✝ ≫ dFrom X✝ x✝ = 0) ≫ (homologyFunctor V c x✝).map (x✝² ≫ x✝¹) =
    homology.π (dTo X✝ x✝) (dFrom X✝ x✝) (_ : dTo X✝ x✝ ≫ dFrom X✝ x✝ = 0) ≫
      (homologyFunctor V c x✝).map x✝² ≫ (homologyFunctor V c x✝).map x✝¹
[PROOFSTEP]
simp only [Hom.sqFrom_comp, kernelSubobjectMap_comp, homology.π_map_assoc, homology.π_map, homologyFunctor_map,
  Category.assoc]
