simp
α : 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
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
x y : ι
hxy : f x = f y
hli : LinearIndependent (ι := ↑{x, y}) R ({x, y}.restrict f)
⊢ y ∈ {x, y}
no goals