no goals
ι : Type u_1
ι' : Type ?u.98205
k : Type u_2
V : Type u_4
P : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
inst✝ : DecidableEq ι
i j : ι
⊢ ↑(coord b i) (↑b j) = if i = j then 1 else 0
cases' eq_or_ne i j with h h <;> simp [h]