simpa using h.1
α : 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
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h✝ : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
i : η
j : ι
h : i ∈ I ∧ j ∈ s i
⊢ i ∈ hIfin.toFinset
no goals