[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i j : ι
h : ¬ComplexShape.Rel c i j
⊢ (fun i j => NatTrans.app (d C i j) t) i j = 0
[PROOFSTEP]
have := C.shape _ _ h
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i j : ι
h : ¬ComplexShape.Rel c i j
this : d C i j = 0
⊢ (fun i j => NatTrans.app (d C i j) t) i j = 0
[PROOFSTEP]
rw [NatTrans.ext_iff, Function.funext_iff] at this 
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i j : ι
h : ¬ComplexShape.Rel c i j
this : ∀ (a : T), NatTrans.app (d C i j) a = NatTrans.app 0 a
⊢ (fun i j => NatTrans.app (d C i j) t) i j = 0
[PROOFSTEP]
exact this t
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i j k : ι
x✝¹ : ComplexShape.Rel c i j
x✝ : ComplexShape.Rel c j k
⊢ (fun i j => NatTrans.app (d C i j) t) i j ≫ (fun i j => NatTrans.app (d C i j) t) j k = 0
[PROOFSTEP]
have := C.d_comp_d i j k
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i j k : ι
x✝¹ : ComplexShape.Rel c i j
x✝ : ComplexShape.Rel c j k
this : d C i j ≫ d C j k = 0
⊢ (fun i j => NatTrans.app (d C i j) t) i j ≫ (fun i j => NatTrans.app (d C i j) t) j k = 0
[PROOFSTEP]
rw [NatTrans.ext_iff, Function.funext_iff] at this 
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i j k : ι
x✝¹ : ComplexShape.Rel c i j
x✝ : ComplexShape.Rel c j k
this : ∀ (a : T), NatTrans.app (d C i j ≫ d C j k) a = NatTrans.app 0 a
⊢ (fun i j => NatTrans.app (d C i j) t) i j ≫ (fun i j => NatTrans.app (d C i j) t) j k = 0
[PROOFSTEP]
exact this t
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
⊢ { obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
          map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
      (𝟙 t) =
    𝟙
      ({ obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
            map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.obj
        t)
[PROOFSTEP]
ext i
[GOAL]
case h
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i : ι
⊢ Hom.f
      ({ obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
            map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
        (𝟙 t))
      i =
    Hom.f
      (𝟙
        ({ obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
              map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.obj
          t))
      i
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i : ι
⊢ (X C i).map (𝟙 t) = 𝟙 ((X C i).obj t)
[PROOFSTEP]
rw [(C.X i).map_id]
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
⊢ { obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
          map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
      (h₁ ≫ h₂) =
    { obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
            map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
        h₁ ≫
      { obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
            map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
        h₂
[PROOFSTEP]
ext i
[GOAL]
case h
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
i : ι
⊢ Hom.f
      ({ obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
            map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
        (h₁ ≫ h₂))
      i =
    Hom.f
      ({ obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
              map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
          h₁ ≫
        { obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
              map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
          h₂)
      i
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
i : ι
⊢ (X C i).map (h₁ ≫ h₂) = (X C i).map h₁ ≫ (X C i).map h₂
[PROOFSTEP]
rw [Functor.map_comp]
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.4445, u_2} T
X✝ Y✝ : HomologicalComplex (T ⥤ V) c
f : X✝ ⟶ Y✝
t t' : T
g : t ⟶ t'
⊢ ((fun C => asFunctor C) X✝).map g ≫ (fun t => Hom.mk fun i => NatTrans.app (Hom.f f i) t) t' =
    (fun t => Hom.mk fun i => NatTrans.app (Hom.f f i) t) t ≫ ((fun C => asFunctor C) Y✝).map g
[PROOFSTEP]
ext i
[GOAL]
case h
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.4445, u_2} T
X✝ Y✝ : HomologicalComplex (T ⥤ V) c
f : X✝ ⟶ Y✝
t t' : T
g : t ⟶ t'
i : ι
⊢ Hom.f (((fun C => asFunctor C) X✝).map g ≫ (fun t => Hom.mk fun i => NatTrans.app (Hom.f f i) t) t') i =
    Hom.f ((fun t => Hom.mk fun i => NatTrans.app (Hom.f f i) t) t ≫ ((fun C => asFunctor C) Y✝).map g) i
[PROOFSTEP]
exact (f.f i).naturality g
