ι : Type ?u.219028
V : Type u
inst✝⁴ : Category V
inst✝³ : HasZeroMorphisms V
α : Type u_1
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
h : i + 1 ≠ j
⊢ (if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) = 0
ι : Type ?u.219028
V : Type u
inst✝⁴ : Category V
inst✝³ : HasZeroMorphisms V
α : Type u_1
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
h : i + 1 ≠ j
⊢ HomologicalComplex.d (of X d sq) i j = 0
dsimp [of]
no goals
ι : Type ?u.219028
V : Type u
inst✝⁴ : Category V
inst✝³ : HasZeroMorphisms V
α : Type u_1
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
h : i + 1 ≠ j
⊢ (if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) = 0
rw [dif_neg h]