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