case h
ι : Type u_1
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 : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n : ι
⊢ Hom.f (nullHomotopicMap' hom ≫ g) n = Hom.f (nullHomotopicMap' fun i j hij => hom i j hij ≫ Hom.f g j) n
ι : Type u_1
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 : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
⊢ nullHomotopicMap' hom ≫ g = nullHomotopicMap' fun i j hij => hom i j hij ≫ Hom.f g j
ext n
case h
ι : Type u_1
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 : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n : ι
⊢ Hom.f (nullHomotopicMap fun i j => (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) ≫ Hom.f g j) n =
    Hom.f (nullHomotopicMap' fun i j hij => hom i j hij ≫ Hom.f g j) n
case h
ι : Type u_1
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 : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n : ι
⊢ Hom.f (nullHomotopicMap' hom ≫ g) n = Hom.f (nullHomotopicMap' fun i j hij => hom i j hij ≫ Hom.f g j) n
erw [nullHomotopicMap_comp]
case h.e_self.e_hom
ι : Type u_1
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 : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n : ι
⊢ (fun i j => (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) ≫ Hom.f g j) = fun i j =>
    dite (ComplexShape.Rel c j i) ((fun i j hij => hom i j hij ≫ Hom.f g j) i j) fun x => 0
case h
ι : Type u_1
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 : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n : ι
⊢ Hom.f (nullHomotopicMap fun i j => (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) ≫ Hom.f g j) n =
    Hom.f (nullHomotopicMap' fun i j hij => hom i j hij ≫ Hom.f g j) n
congr
case h.e_self.e_hom.h.h
ι : Type u_1
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✝ : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n i j : ι
⊢ (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) ≫ Hom.f g j =
    dite (ComplexShape.Rel c j i) ((fun i j hij => hom i j hij ≫ Hom.f g j) i j) fun x => 0
case h.e_self.e_hom
ι : Type u_1
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 : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n : ι
⊢ (fun i j => (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) ≫ Hom.f g j) = fun i j =>
    dite (ComplexShape.Rel c j i) ((fun i j hij => hom i j hij ≫ Hom.f g j) i j) fun x => 0
ext (i j)
case h.e_self.e_hom.h.h.inl
ι : Type u_1
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✝ : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n i j : ι
h✝ : ComplexShape.Rel c j i
⊢ hom i j h✝ ≫ Hom.f g j = (fun i j hij => hom i j hij ≫ Hom.f g j) i j h✝

case h.e_self.e_hom.h.h.inr
ι : Type u_1
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✝ : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n i j : ι
h✝ : ¬ComplexShape.Rel c j i
⊢ 0 ≫ Hom.f g j = 0
case h.e_self.e_hom.h.h
ι : Type u_1
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✝ : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n i j : ι
⊢ (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) ≫ Hom.f g j =
    dite (ComplexShape.Rel c j i) ((fun i j hij => hom i j hij ≫ Hom.f g j) i j) fun x => 0
split_ifs
no goals
case h.e_self.e_hom.h.h.inl
ι : Type u_1
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✝ : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n i j : ι
h✝ : ComplexShape.Rel c j i
⊢ hom i j h✝ ≫ Hom.f g j = (fun i j hij => hom i j hij ≫ Hom.f g j) i j h✝
rfl
no goals
case h.e_self.e_hom.h.h.inr
ι : Type u_1
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✝ : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n i j : ι
h✝ : ¬ComplexShape.Rel c j i
⊢ 0 ≫ Hom.f g j = 0
rw [zero_comp]