[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
n : ℕ
f : C ⟶ D
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun i => n • Hom.f f i) i ≫ d D i j = d C i j ≫ (fun i => n • Hom.f f i) j
[PROOFSTEP]
simp [Preadditive.nsmul_comp, Preadditive.comp_nsmul]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
n : ℤ
f : C ⟶ D
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun i => n • Hom.f f i) i ≫ d D i j = d C i j ≫ (fun i => n • Hom.f f i) j
[PROOFSTEP]
simp [Preadditive.zsmul_comp, Preadditive.comp_zsmul]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ 0.f = 0
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ ∀ (x y : C ⟶ D), (x + y).f = x.f + y.f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ ∀ (x : C ⟶ D), (-x).f = -x.f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ ∀ (x y : C ⟶ D), (x - y).f = x.f - y.f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ ∀ (x : C ⟶ D) (n : ℕ), (n • x).f = n • x.f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ ∀ (x : C ⟶ D) (n : ℤ), (n • x).f = n • x.f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
x✝² x✝¹ x✝ : HomologicalComplex V c
f f' : x✝² ⟶ x✝¹
g : x✝¹ ⟶ x✝
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
x✝² x✝¹ x✝ : HomologicalComplex V c
f f' : x✝² ⟶ x✝¹
g : x✝¹ ⟶ x✝
i✝ : ι
⊢ Hom.f ((f + f') ≫ g) i✝ = Hom.f (f ≫ g + f' ≫ g) i✝
[PROOFSTEP]
simp only [comp_f, add_f_apply]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
x✝² x✝¹ x✝ : HomologicalComplex V c
f f' : x✝² ⟶ x✝¹
g : x✝¹ ⟶ x✝
i✝ : ι
⊢ (Hom.f f i✝ + Hom.f f' i✝) ≫ Hom.f g i✝ = Hom.f f i✝ ≫ Hom.f g i✝ + Hom.f f' i✝ ≫ Hom.f g i✝
[PROOFSTEP]
rw [Preadditive.add_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
x✝² x✝¹ x✝ : HomologicalComplex V c
f : x✝² ⟶ x✝¹
g g' : x✝¹ ⟶ x✝
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
x✝² x✝¹ x✝ : HomologicalComplex V c
f : x✝² ⟶ x✝¹
g g' : x✝¹ ⟶ x✝
i✝ : ι
⊢ Hom.f (f ≫ (g + g')) i✝ = Hom.f (f ≫ g + f ≫ g') i✝
[PROOFSTEP]
simp only [comp_f, add_f_apply]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
x✝² x✝¹ x✝ : HomologicalComplex V c
f : x✝² ⟶ x✝¹
g g' : x✝¹ ⟶ x✝
i✝ : ι
⊢ Hom.f f i✝ ≫ (Hom.f g i✝ + Hom.f g' i✝) = Hom.f f i✝ ≫ Hom.f g i✝ + Hom.f f i✝ ≫ Hom.f g' i✝
[PROOFSTEP]
rw [Preadditive.comp_add]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
x✝¹ x✝ : HomologicalComplex V c
f g : x✝¹ ⟶ x✝
⊢ (homologyFunctor V c i).map (f + g) = (homologyFunctor V c i).map f + (homologyFunctor V c i).map g
[PROOFSTEP]
dsimp [homologyFunctor]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
x✝¹ x✝ : HomologicalComplex V c
f g : x✝¹ ⟶ x✝
⊢ homology.map (_ : dTo x✝¹ i ≫ dFrom x✝¹ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo (f + g) i)
      (Hom.sqFrom (f + g) i) (_ : (Hom.sqTo (f + g) i).right = (Hom.sqTo (f + g) i).right) =
    homology.map (_ : dTo x✝¹ i ≫ dFrom x✝¹ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
        (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) +
      homology.map (_ : dTo x✝¹ i ≫ dFrom x✝¹ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo g i) (Hom.sqFrom g i)
        (_ : (Hom.sqTo g i).right = (Hom.sqTo g i).right)
[PROOFSTEP]
ext
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
x✝¹ x✝ : HomologicalComplex V c
f g : x✝¹ ⟶ x✝
⊢ 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 (f + g) i)
        (Hom.sqFrom (f + g) i) (_ : (Hom.sqTo (f + g) i).right = (Hom.sqTo (f + g) 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 x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
          (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) +
        homology.map (_ : dTo x✝¹ i ≫ dFrom x✝¹ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo g i) (Hom.sqFrom g i)
          (_ : (Hom.sqTo g i).right = (Hom.sqTo g i).right))
[PROOFSTEP]
simp only [homology.π_map, Preadditive.comp_add, ← Preadditive.add_comp]
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
x✝¹ x✝ : HomologicalComplex V c
f g : x✝¹ ⟶ x✝
⊢ kernelSubobjectMap (Hom.sqFrom (f + g) i) ≫ homology.π (dTo x✝ i) (dFrom x✝ i) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) =
    (kernelSubobjectMap (Hom.sqFrom f i) + kernelSubobjectMap (Hom.sqFrom g i)) ≫
      homology.π (dTo x✝ i) (dFrom x✝ i) (_ : dTo x✝ i ≫ dFrom x✝ i = 0)
[PROOFSTEP]
congr
[GOAL]
case p.e_a
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
x✝¹ x✝ : HomologicalComplex V c
f g : x✝¹ ⟶ x✝
⊢ kernelSubobjectMap (Hom.sqFrom (f + g) i) = kernelSubobjectMap (Hom.sqFrom f i) + kernelSubobjectMap (Hom.sqFrom g i)
[PROOFSTEP]
ext
[GOAL]
case p.e_a.h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
x✝¹ x✝ : HomologicalComplex V c
f g : x✝¹ ⟶ x✝
⊢ kernelSubobjectMap (Hom.sqFrom (f + g) i) ≫ Subobject.arrow (kernelSubobject (dFrom x✝ i)) =
    (kernelSubobjectMap (Hom.sqFrom f i) + kernelSubobjectMap (Hom.sqFrom g i)) ≫
      Subobject.arrow (kernelSubobject (dFrom x✝ i))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
C✝ D E : HomologicalComplex V c✝
f g : C✝ ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.55346, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
w : ¬ComplexShape.Rel c i j
⊢ (fun i j => F.map (d C i j)) i j = 0
[PROOFSTEP]
dsimp only
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
C✝ D E : HomologicalComplex V c✝
f g : C✝ ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.55346, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
w : ¬ComplexShape.Rel c i j
⊢ F.map (d C i j) = 0
[PROOFSTEP]
rw [C.shape _ _ w, F.map_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
C✝ D E : HomologicalComplex V c✝
f g : C✝ ⟶ D
h k✝ : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.55346, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
x✝¹ : ComplexShape.Rel c i j
x✝ : ComplexShape.Rel c j k
⊢ (fun i j => F.map (d C i j)) i j ≫ (fun i j => F.map (d C i j)) j k = 0
[PROOFSTEP]
rw [← F.map_comp, C.d_comp_d, F.map_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.55346, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
c : ComplexShape ι
X✝ Y✝ : HomologicalComplex V c
f : X✝ ⟶ Y✝
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun i => F.map (Hom.f f i)) i ≫
      d ((fun C => HomologicalComplex.mk (fun i => F.obj (X C i)) fun i j => F.map (d C i j)) Y✝) i j =
    d ((fun C => HomologicalComplex.mk (fun i => F.obj (X C i)) fun i j => F.map (d C i j)) X✝) i j ≫
      (fun i => F.map (Hom.f f i)) j
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.55346, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
c : ComplexShape ι
X✝ Y✝ : HomologicalComplex V c
f : X✝ ⟶ Y✝
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ F.map (Hom.f f i) ≫ F.map (d Y✝ i j) = F.map (d X✝ i j) ≫ F.map (Hom.f f j)
[PROOFSTEP]
rw [← F.map_comp, ← F.map_comp, f.comm]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝³ : Category.{?u.91619, u_2} W
inst✝² : Preadditive W
F : V ⥤ W
inst✝¹ : Additive F
inst✝ : ReflectsIsomorphisms F
c : ComplexShape ι
A✝ B✝ : HomologicalComplex V c
f : A✝ ⟶ B✝
⊢ ∀ [inst : IsIso ((mapHomologicalComplex F c).map f)], IsIso f
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁴ : Category.{?u.91619, u_2} W
inst✝³ : Preadditive W
F : V ⥤ W
inst✝² : Additive F
inst✝¹ : ReflectsIsomorphisms F
c : ComplexShape ι
A✝ B✝ : HomologicalComplex V c
f : A✝ ⟶ B✝
inst✝ : IsIso ((mapHomologicalComplex F c).map f)
⊢ IsIso f
[PROOFSTEP]
haveI : ∀ n : ι, IsIso (F.map (f.f n)) := fun n =>
  IsIso.of_iso ((HomologicalComplex.eval W c n).mapIso (asIso ((F.mapHomologicalComplex c).map f)))
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁴ : Category.{?u.91619, u_2} W
inst✝³ : Preadditive W
F : V ⥤ W
inst✝² : Additive F
inst✝¹ : ReflectsIsomorphisms F
c : ComplexShape ι
A✝ B✝ : HomologicalComplex V c
f : A✝ ⟶ B✝
inst✝ : IsIso ((mapHomologicalComplex F c).map f)
this : ∀ (n : ι), IsIso (F.map (Hom.f f n))
⊢ IsIso f
[PROOFSTEP]
haveI := fun n => isIso_of_reflects_iso (f.f n) F
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁴ : Category.{?u.91619, u_2} W
inst✝³ : Preadditive W
F : V ⥤ W
inst✝² : Additive F
inst✝¹ : ReflectsIsomorphisms F
c : ComplexShape ι
A✝ B✝ : HomologicalComplex V c
f : A✝ ⟶ B✝
inst✝ : IsIso ((mapHomologicalComplex F c).map f)
this✝ : ∀ (n : ι), IsIso (F.map (Hom.f f n))
this : ∀ (n : ι), IsIso (Hom.f f n)
⊢ IsIso f
[PROOFSTEP]
exact HomologicalComplex.Hom.isIso_of_components f
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
c : ComplexShape ι
F : V ⥤ W
inst✝ : Functor.Additive F
⊢ mapHomologicalComplex (𝟙 F) c = 𝟙 (Functor.mapHomologicalComplex F c)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁴ : Category.{u_3, u_2} W
inst✝³ : Preadditive W
c : ComplexShape ι
F G H : V ⥤ W
inst✝² : Functor.Additive F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Additive H
α : F ⟶ G
β : G ⟶ H
⊢ mapHomologicalComplex (α ≫ β) c = mapHomologicalComplex α c ≫ mapHomologicalComplex β c
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c✝
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
W : Type u_2
inst✝³ : Category.{u_3, u_2} W
inst✝² : Preadditive W
c : ComplexShape ι
F G : V ⥤ W
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
C D : HomologicalComplex V c
f : C ⟶ D
⊢ (Functor.mapHomologicalComplex F c).map f ≫ app (mapHomologicalComplex α c) D =
    app (mapHomologicalComplex α c) C ≫ (Functor.mapHomologicalComplex G c).map f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝³ : Category.{?u.106581, u_2} W
inst✝² : Preadditive W
F G : V ⥤ W
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ≅ G
c : ComplexShape ι
⊢ NatTrans.mapHomologicalComplex α.hom c ≫ NatTrans.mapHomologicalComplex α.inv c =
    𝟙 (Functor.mapHomologicalComplex F c)
[PROOFSTEP]
simp only [← NatTrans.mapHomologicalComplex_comp, α.hom_inv_id, NatTrans.mapHomologicalComplex_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝³ : Category.{?u.106581, u_2} W
inst✝² : Preadditive W
F G : V ⥤ W
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ≅ G
c : ComplexShape ι
⊢ NatTrans.mapHomologicalComplex α.inv c ≫ NatTrans.mapHomologicalComplex α.hom c =
    𝟙 (Functor.mapHomologicalComplex G c)
[PROOFSTEP]
simp only [← NatTrans.mapHomologicalComplex_comp, α.inv_hom_id, NatTrans.mapHomologicalComplex_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁵ : Category.{?u.119648, u_2} W
inst✝⁴ : Preadditive W
α : Type u_3
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : V ⥤ W
inst✝ : Functor.Additive F
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
n : α
⊢ (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0
[PROOFSTEP]
rw [← F.map_comp, sq n, Functor.map_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁵ : Category.{u_4, u_2} W
inst✝⁴ : Preadditive W
α : Type u_3
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : V ⥤ W
inst✝ : Functor.Additive F
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
⊢ (Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq) =
    of (fun n => F.obj (X n)) (fun n => F.map (d n))
      (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0)
[PROOFSTEP]
refine' HomologicalComplex.ext rfl _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁵ : Category.{u_4, u_2} W
inst✝⁴ : Preadditive W
α : Type u_3
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : V ⥤ W
inst✝ : Functor.Additive F
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
⊢ ∀ (i j : α),
    ComplexShape.Rel (ComplexShape.down α) i j →
      HomologicalComplex.d ((Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq)) i j ≫
          eqToHom
            (_ :
              HomologicalComplex.X ((Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq)) j =
                HomologicalComplex.X
                  (of (fun n => F.obj (X n)) (fun n => F.map (d n))
                    (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0))
                  j) =
        eqToHom
            (_ :
              HomologicalComplex.X ((Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq)) i =
                HomologicalComplex.X
                  (of (fun n => F.obj (X n)) (fun n => F.map (d n))
                    (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0))
                  i) ≫
          HomologicalComplex.d
            (of (fun n => F.obj (X n)) (fun n => F.map (d n))
              (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0))
            i j
[PROOFSTEP]
rintro i j (rfl : j + 1 = i)
[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁵ : Category.{u_4, u_2} W
inst✝⁴ : Preadditive W
α : Type u_3
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : V ⥤ W
inst✝ : Functor.Additive F
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ HomologicalComplex.d ((Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq)) (j + 1) j ≫
      eqToHom
        (_ :
          HomologicalComplex.X ((Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq)) j =
            HomologicalComplex.X
              (of (fun n => F.obj (X n)) (fun n => F.map (d n))
                (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0))
              j) =
    eqToHom
        (_ :
          HomologicalComplex.X ((Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq)) (j + 1) =
            HomologicalComplex.X
              (of (fun n => F.obj (X n)) (fun n => F.map (d n))
                (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0))
              (j + 1)) ≫
      HomologicalComplex.d
        (of (fun n => F.obj (X n)) (fun n => F.map (d n))
          (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0))
        (j + 1) j
[PROOFSTEP]
simp only [CategoryTheory.Functor.mapHomologicalComplex_obj_d, of_d, eqToHom_refl, comp_id, id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : i = j
⊢ HomologicalComplex.X ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X) i =
    HomologicalComplex.X ((F ⋙ single W c j).obj X) i
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : i = j
⊢ HomologicalComplex.X ((F ⋙ single W c j).obj X) i =
    HomologicalComplex.X ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X) i
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
⊢ ((Hom.mk fun i =>
        if h : i = j then
          eqToHom
            (_ :
              HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
        else 0) ≫
      Hom.mk fun i =>
        if h : i = j then
          eqToHom
            (_ :
              HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
        else 0) =
    𝟙 ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X)
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
⊢ Hom.f
      ((Hom.mk fun i =>
          if h : i = j then
            eqToHom
              (_ :
                HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                  HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
          else 0) ≫
        Hom.mk fun i =>
          if h : i = j then
            eqToHom
              (_ :
                HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                  HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
          else 0)
      i =
    Hom.f (𝟙 ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X)) i
[PROOFSTEP]
dsimp
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
⊢ ((if h : i = j then eqToHom (_ : F.obj (if i = j then X else 0) = if i = j then F.obj X else 0) else 0) ≫
      if h : i = j then eqToHom (_ : (if i = j then F.obj X else 0) = F.obj (if i = j then X else 0)) else 0) =
    𝟙 (F.obj (if i = j then X else 0))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : i = j
⊢ eqToHom (_ : F.obj (if i = j then X else 0) = if i = j then F.obj X else 0) ≫
      eqToHom (_ : (if i = j then F.obj X else 0) = F.obj (if i = j then X else 0)) =
    𝟙 (F.obj (if i = j then X else 0))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : ¬i = j
⊢ 0 ≫ 0 = 𝟙 (F.obj (if i = j then X else 0))
[PROOFSTEP]
rw [zero_comp, if_neg h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : ¬i = j
⊢ 0 = 𝟙 (F.obj 0)
[PROOFSTEP]
exact (zero_of_source_iso_zero _ F.mapZeroObject).symm
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
⊢ ((Hom.mk fun i =>
        if h : i = j then
          eqToHom
            (_ :
              HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
        else 0) ≫
      Hom.mk fun i =>
        if h : i = j then
          eqToHom
            (_ :
              HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
        else 0) =
    𝟙 ((F ⋙ single W c j).obj X)
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
⊢ Hom.f
      ((Hom.mk fun i =>
          if h : i = j then
            eqToHom
              (_ :
                HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                  HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
          else 0) ≫
        Hom.mk fun i =>
          if h : i = j then
            eqToHom
              (_ :
                HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                  HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
          else 0)
      i =
    Hom.f (𝟙 ((F ⋙ single W c j).obj X)) i
[PROOFSTEP]
dsimp
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
⊢ ((if h : i = j then eqToHom (_ : (if i = j then F.obj X else 0) = F.obj (if i = j then X else 0)) else 0) ≫
      if h : i = j then eqToHom (_ : F.obj (if i = j then X else 0) = if i = j then F.obj X else 0) else 0) =
    𝟙 (if i = j then F.obj X else 0)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : i = j
⊢ eqToHom (_ : (if i = j then F.obj X else 0) = F.obj (if i = j then X else 0)) ≫
      eqToHom (_ : F.obj (if i = j then X else 0) = if i = j then F.obj X else 0) =
    𝟙 (if i = j then F.obj X else 0)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : ¬i = j
⊢ 0 ≫ 0 = 𝟙 (if i = j then F.obj X else 0)
[PROOFSTEP]
rw [zero_comp, if_neg h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : ¬i = j
⊢ 0 = 𝟙 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ (single V c j ⋙ Functor.mapHomologicalComplex F c).map f ≫
      ((fun X =>
            Iso.mk
              (Hom.mk fun i =>
                if h : i = j then
                  eqToHom
                    (_ :
                      HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                        HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
                else 0)
              (Hom.mk fun i =>
                if h : i = j then
                  eqToHom
                    (_ :
                      HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                        HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
                else 0))
          Y✝).hom =
    ((fun X =>
            Iso.mk
              (Hom.mk fun i =>
                if h : i = j then
                  eqToHom
                    (_ :
                      HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                        HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
                else 0)
              (Hom.mk fun i =>
                if h : i = j then
                  eqToHom
                    (_ :
                      HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                        HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
                else 0))
          X✝).hom ≫
      (F ⋙ single W c j).map f
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
⊢ Hom.f
      ((single V c j ⋙ Functor.mapHomologicalComplex F c).map f ≫
        ((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  if h : i = j then
                    eqToHom
                      (_ :
                        HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                          HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
                  else 0)
                (Hom.mk fun i =>
                  if h : i = j then
                    eqToHom
                      (_ :
                        HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                          HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
                  else 0))
            Y✝).hom)
      i =
    Hom.f
      (((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  if h : i = j then
                    eqToHom
                      (_ :
                        HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                          HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
                  else 0)
                (Hom.mk fun i =>
                  if h : i = j then
                    eqToHom
                      (_ :
                        HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                          HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
                  else 0))
            X✝).hom ≫
        (F ⋙ single W c j).map f)
      i
[PROOFSTEP]
dsimp
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
⊢ (F.map
        (if h : i = j then
          eqToHom (_ : X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) X✝) i = X✝) ≫
            f ≫ eqToHom (_ : Y✝ = X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) Y✝) i)
        else 0) ≫
      if h : i = j then eqToHom (_ : F.obj (if i = j then Y✝ else 0) = if i = j then F.obj Y✝ else 0) else 0) =
    (if h : i = j then eqToHom (_ : F.obj (if i = j then X✝ else 0) = if i = j then F.obj X✝ else 0) else 0) ≫
      if h : i = j then
        eqToHom (_ : X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) (F.obj X✝)) i = F.obj X✝) ≫
          F.map f ≫
            eqToHom (_ : F.obj Y✝ = X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) (F.obj Y✝)) i)
      else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ F.map
        (eqToHom (_ : X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) X✝) i = X✝) ≫
          f ≫ eqToHom (_ : Y✝ = X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) Y✝) i)) ≫
      eqToHom (_ : F.obj (if i = j then Y✝ else 0) = if i = j then F.obj Y✝ else 0) =
    eqToHom (_ : F.obj (if i = j then X✝ else 0) = if i = j then F.obj X✝ else 0) ≫
      eqToHom (_ : X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) (F.obj X✝)) i = F.obj X✝) ≫
        F.map f ≫
          eqToHom (_ : F.obj Y✝ = X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) (F.obj Y✝)) i)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : ¬i = j
⊢ F.map 0 ≫ 0 = 0 ≫ 0
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.161257, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
j : ι
X : V
⊢ HomologicalComplex.X ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X) j =
    HomologicalComplex.X ((F ⋙ single W c j).obj X) j
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{u_3, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
j : ι
X : V
⊢ Hom.f (NatTrans.app (singleMapHomologicalComplex F c j).hom X) j =
    eqToHom (_ : F.obj (if j = j then X else 0) = if j = j then F.obj X else 0)
[PROOFSTEP]
simp [singleMapHomologicalComplex]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{u_3, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
i j : ι
h : i ≠ j
X : V
⊢ Hom.f (NatTrans.app (singleMapHomologicalComplex F c j).hom X) i = 0
[PROOFSTEP]
simp [singleMapHomologicalComplex, h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.177119, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
j : ι
X : V
⊢ HomologicalComplex.X ((F ⋙ single W c j).obj X) j =
    HomologicalComplex.X ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X) j
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{u_3, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
j : ι
X : V
⊢ Hom.f (NatTrans.app (singleMapHomologicalComplex F c j).inv X) j =
    eqToHom (_ : (if j = j then F.obj X else 0) = F.obj (if j = j then X else 0))
[PROOFSTEP]
simp [singleMapHomologicalComplex]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{u_3, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
i j : ι
h : i ≠ j
X : V
⊢ Hom.f (NatTrans.app (singleMapHomologicalComplex F c j).inv X) i = 0
[PROOFSTEP]
simp [singleMapHomologicalComplex, h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ ((Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).hom) ≫
      Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).inv) =
    𝟙 ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv)
      Nat.zero =
    Hom.f (𝟙 ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv)
      (Nat.succ n✝) =
    Hom.f (𝟙 ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)) (Nat.succ n✝)
[PROOFSTEP]
exact IsZero.eq_of_src (IsZero.of_iso (isZero_zero _) F.mapZeroObject) _ _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ ((Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).inv) ≫
      Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).hom) =
    𝟙 ((F ⋙ single₀ W).obj X)
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom)
      Nat.zero =
    Hom.f (𝟙 ((F ⋙ single₀ W).obj X)) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom)
      (Nat.succ n✝) =
    Hom.f (𝟙 ((F ⋙ single₀ W).obj X)) (Nat.succ n✝)
[PROOFSTEP]
exact IsZero.eq_of_src (isZero_zero _) _ _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ (single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map f ≫
      ((fun X =>
            Iso.mk
              (Hom.mk fun i =>
                match i with
                | 0 =>
                  𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).hom)
              (Hom.mk fun i =>
                match i with
                | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).inv))
          Y✝).hom =
    ((fun X =>
            Iso.mk
              (Hom.mk fun i =>
                match i with
                | 0 =>
                  𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).hom)
              (Hom.mk fun i =>
                match i with
                | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).inv))
          X✝).hom ≫
      (F ⋙ single₀ W).map f
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ Hom.f
      ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map f ≫
        ((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙
                      (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)
                        0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            Y✝).hom)
      Nat.zero =
    Hom.f
      (((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙
                      (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)
                        0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            X✝).hom ≫
        (F ⋙ single₀ W).map f)
      Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X✝ Y✝ : V
f : X✝ ⟶ Y✝
n✝ : ℕ
⊢ Hom.f
      ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map f ≫
        ((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙
                      (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)
                        0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            Y✝).hom)
      (Nat.succ n✝) =
    Hom.f
      (((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙
                      (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)
                        0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            X✝).hom ≫
        (F ⋙ single₀ W).map f)
      (Nat.succ n✝)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ ((Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).hom) ≫
      Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).inv) =
    𝟙 ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X)
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv)
      Nat.zero =
    Hom.f (𝟙 ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X)) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv)
      (Nat.succ n✝) =
    Hom.f (𝟙 ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X)) (Nat.succ n✝)
[PROOFSTEP]
exact IsZero.eq_of_src (IsZero.of_iso (isZero_zero _) F.mapZeroObject) _ _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ ((Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).inv) ≫
      Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).hom) =
    𝟙 ((F ⋙ single₀ W).obj X)
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom)
      Nat.zero =
    Hom.f (𝟙 ((F ⋙ single₀ W).obj X)) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom)
      (Nat.succ n✝) =
    Hom.f (𝟙 ((F ⋙ single₀ W).obj X)) (Nat.succ n✝)
[PROOFSTEP]
exact IsZero.eq_of_src (isZero_zero _) _ _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ (single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map f ≫
      ((fun X =>
            Iso.mk
              (Hom.mk fun i =>
                match i with
                | 0 =>
                  𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).hom)
              (Hom.mk fun i =>
                match i with
                | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).inv))
          Y✝).hom =
    ((fun X =>
            Iso.mk
              (Hom.mk fun i =>
                match i with
                | 0 =>
                  𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).hom)
              (Hom.mk fun i =>
                match i with
                | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).inv))
          X✝).hom ≫
      (F ⋙ single₀ W).map f
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ Hom.f
      ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map f ≫
        ((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            Y✝).hom)
      Nat.zero =
    Hom.f
      (((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            X✝).hom ≫
        (F ⋙ single₀ W).map f)
      Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X✝ Y✝ : V
f : X✝ ⟶ Y✝
n✝ : ℕ
⊢ Hom.f
      ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map f ≫
        ((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            Y✝).hom)
      (Nat.succ n✝) =
    Hom.f
      (((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            X✝).hom ≫
        (F ⋙ single₀ W).map f)
      (Nat.succ n✝)
[PROOFSTEP]
simp
