refine linearIndependent_of_finite _ fun t ht htfin ↦ ?_
α : 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)
hinj : Injective f
⊢ LinearIndependent (ι := { x // x ∈ range f }) R Subtype.val
α : 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)
hinj : Injective f
t : Set M
ht : t ⊆ range f
htfin : t.Finite
⊢ LinearIndependent R fun (x : ↑t) => ↑x