no goals
ι : Type ?u.267671
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type ?u.268026
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
i j : ι
hij : ComplexShape.Rel c j i
⊢ X ((Functor.mapHomologicalComplex G c).obj C) i ⟶ X ((Functor.mapHomologicalComplex G c).obj D) j
exact G.map (hom i j hij)
case h
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n : ι
⊢ Hom.f ((Functor.mapHomologicalComplex G c).map (nullHomotopicMap' hom)) n =
    Hom.f (nullHomotopicMap' fun i j hij => G.map (hom i j hij)) n
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (Functor.mapHomologicalComplex G c).map (nullHomotopicMap' hom) = nullHomotopicMap' fun i j hij => G.map (hom i j hij)
ext n
case h
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n : ι
⊢ Hom.f (nullHomotopicMap fun i j => G.map (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0)) n =
    Hom.f (nullHomotopicMap' fun i j hij => G.map (hom i j hij)) n
case h
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n : ι
⊢ Hom.f ((Functor.mapHomologicalComplex G c).map (nullHomotopicMap' hom)) n =
    Hom.f (nullHomotopicMap' fun i j hij => G.map (hom i j hij)) n
erw [map_nullHomotopicMap]
case h.e_self.e_hom
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n : ι
⊢ (fun i j => G.map (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0)) = fun i j =>
    dite (ComplexShape.Rel c j i) ((fun i j hij => G.map (hom i j hij)) i j) fun x => 0
case h
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n : ι
⊢ Hom.f (nullHomotopicMap fun i j => G.map (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0)) n =
    Hom.f (nullHomotopicMap' fun i j hij => G.map (hom i j hij)) n
congr
case h.e_self.e_hom.h.h
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n i j : ι
⊢ G.map (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) =
    dite (ComplexShape.Rel c j i) ((fun i j hij => G.map (hom i j hij)) i j) fun x => 0
case h.e_self.e_hom
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n : ι
⊢ (fun i j => G.map (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0)) = fun i j =>
    dite (ComplexShape.Rel c j i) ((fun i j hij => G.map (hom i j hij)) i j) fun x => 0
ext (i j)
case h.e_self.e_hom.h.h.inl
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n i j : ι
h✝ : ComplexShape.Rel c j i
⊢ G.map (hom i j h✝) = (fun i j hij => G.map (hom i j hij)) i j h✝

case h.e_self.e_hom.h.h.inr
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n i j : ι
h✝ : ¬ComplexShape.Rel c j i
⊢ G.map 0 = 0
case h.e_self.e_hom.h.h
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n i j : ι
⊢ G.map (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) =
    dite (ComplexShape.Rel c j i) ((fun i j hij => G.map (hom i j hij)) i j) fun x => 0
split_ifs
no goals
case h.e_self.e_hom.h.h.inl
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n i j : ι
h✝ : ComplexShape.Rel c j i
⊢ G.map (hom i j h✝) = (fun i j hij => G.map (hom i j hij)) i j h✝
rfl
no goals
case h.e_self.e_hom.h.h.inr
ι : Type u_3
V : Type u
inst✝⁴ : Category V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_1
inst✝² : Category W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n i j : ι
h✝ : ¬ComplexShape.Rel c j i
⊢ G.map 0 = 0
rw [G.map_zero]