exact Eq.trans (get_set_ne xs h e hj) (if_neg h).symm
cont : Type u
idx : Type v
elem : Type w
domGet : cont → idx → Prop
domSet : cont → idx → elem → Prop
inst✝¹ : ArrayLike cont idx elem domGet domSet
inst✝ : DecidableEq idx
xs : cont
i j : idx
e : elem
hi : domSet xs i e
hj : domGet (SetElem.setElem xs i e hi) j
h : ¬i = j
⊢ (SetElem.setElem xs i e hi)[j] = if i = j then e else xs[j]
no goals