ι : 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₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ 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₁ =
    d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + 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₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap' h) k₁ = d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + 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₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (d C k₁ k₀ ≫ dite (ComplexShape.Rel c k₁ k₀) (h k₀ k₁) fun x => 0) +
      (dite (ComplexShape.Rel c k₂ k₁) (h k₁ k₂) fun x => 0) ≫ d D k₂ k₁ =
    d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + 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₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ 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₁ =
    d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ d D k₂ k₁
rw [nullHomotopicMap_f r₂₁ r₁₀]
ι : 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₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (d C k₁ k₀ ≫ dite (ComplexShape.Rel c k₁ k₀) (h k₀ k₁) fun x => 0) +
      (dite (ComplexShape.Rel c k₂ k₁) (h k₁ k₂) fun x => 0) ≫ d D k₂ k₁ =
    d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + 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₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (d C k₁ k₀ ≫ dite (ComplexShape.Rel c k₁ k₀) (h k₀ k₁) fun x => 0) +
      (dite (ComplexShape.Rel c k₂ k₁) (h k₁ k₂) fun x => 0) ≫ d D k₂ k₁ =
    d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + 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₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ d D k₂ k₁ = d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + 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₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (d C k₁ k₀ ≫ dite (ComplexShape.Rel c k₁ k₀) (h k₀ k₁) fun x => 0) +
      (dite (ComplexShape.Rel c k₂ k₁) (h k₁ k₂) fun x => 0) ≫ d D k₂ k₁ =
    d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + 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₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ d D k₂ k₁ = d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ d D k₂ k₁
rfl