rwa [Unique.eq_default i]
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
h : f default ≠ 0
i : ι
⊢ f i ≠ 0
no goals