ι : 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₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
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₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
ι : 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₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap' h) k₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
simp only [nullHomotopicMap']
ι : 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₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (dite (ComplexShape.Rel c k₁ k₀) (h k₀ k₁) fun x => 0) ≫ d D k₁ k₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
ι : 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₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
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₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
rw [nullHomotopicMap_f_of_not_rel_left r₁₀ hk₀]
ι : 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₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (dite (ComplexShape.Rel c k₁ k₀) (h k₀ k₁) fun x => 0) ≫ d D k₁ k₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
ι : 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₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (dite (ComplexShape.Rel c k₁ k₀) (h k₀ k₁) fun x => 0) ≫ d D k₁ k₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
dsimp
ι : 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₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ h k₀ k₁ r₁₀ ≫ d D k₁ k₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
ι : 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₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (dite (ComplexShape.Rel c k₁ k₀) (h k₀ k₁) fun x => 0) ≫ d D k₁ k₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
split_ifs
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₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ h k₀ k₁ r₁₀ ≫ d D k₁ k₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
rfl