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 : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n : ι
⊢ Hom.f (f ≫ nullHomotopicMap' hom) n = Hom.f (nullHomotopicMap' fun i j hij => Hom.f f i ≫ hom i j hij) 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 : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
⊢ f ≫ nullHomotopicMap' hom = nullHomotopicMap' fun i j hij => Hom.f f i ≫ hom i j hij
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 : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n : ι
⊢ Hom.f (nullHomotopicMap fun i j => Hom.f f i ≫ dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) n =
    Hom.f (nullHomotopicMap' fun i j hij => Hom.f f i ≫ hom i j hij) 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 : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n : ι
⊢ Hom.f (f ≫ nullHomotopicMap' hom) n = Hom.f (nullHomotopicMap' fun i j hij => Hom.f f i ≫ hom i j hij) n
erw [comp_nullHomotopicMap]
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 : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n : ι
⊢ (fun i j => Hom.f f i ≫ 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 => Hom.f f i ≫ hom i j hij) 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 : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n : ι
⊢ Hom.f (nullHomotopicMap fun i j => Hom.f f i ≫ dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) n =
    Hom.f (nullHomotopicMap' fun i j hij => Hom.f f i ≫ hom i j hij) 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✝ : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n i j : ι
⊢ (Hom.f f i ≫ dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) =
    dite (ComplexShape.Rel c j i) ((fun i j hij => Hom.f f i ≫ hom i j hij) 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 : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n : ι
⊢ (fun i j => Hom.f f i ≫ 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 => Hom.f f i ≫ hom i j hij) 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✝ : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n i j : ι
h✝ : ComplexShape.Rel c j i
⊢ Hom.f f i ≫ hom i j h✝ = (fun i j hij => Hom.f f i ≫ hom i j hij) 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✝ : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n i j : ι
h✝ : ¬ComplexShape.Rel c j i
⊢ Hom.f f i ≫ 0 = 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✝ : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n i j : ι
⊢ (Hom.f f i ≫ dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) =
    dite (ComplexShape.Rel c j i) ((fun i j hij => Hom.f f i ≫ hom i j hij) 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✝ : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n i j : ι
h✝ : ComplexShape.Rel c j i
⊢ Hom.f f i ≫ hom i j h✝ = (fun i j hij => Hom.f f i ≫ hom i j hij) 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✝ : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n i j : ι
h✝ : ¬ComplexShape.Rel c j i
⊢ Hom.f f i ≫ 0 = 0
rw [comp_zero]