ι : 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 k₀ : ι
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap fun i j => dite (ComplexShape.Rel c j i) (h i j) fun x => 0) k₀ = 0
ι : 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 k₀ : ι
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap' h) k₀ = 0
simp only [nullHomotopicMap']
no goals
ι : 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 k₀ : ι
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap fun i j => dite (ComplexShape.Rel c j i) (h i j) fun x => 0) k₀ = 0
apply nullHomotopicMap_f_eq_zero hk₀ hk₀'