apply linearIndependent_sUnion_of_directed' _ _ (IsChain.directedOn hchain)
  (fun s hs ↦ (hcss hs).2.2)
case refine_1.intro
α : 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'
K : Type u_7
V : Type u_8
ι : Type u_9
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
s₀ s t : Set ι
hli : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
c : Set (Set ι)
hcss : c ⊆ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
r : Set ι
hr : r ∈ c
⊢ LinearIndependent (ι := ↑(⋃₀ c)) K ((⋃₀ c).restrict f)
no goals