obtain (h_empt | hne) := isEmpty_or_nonempty η
α : 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)
⊢ LinearIndependent (ι := ↑(⋃ j, s j)) R ((⋃ j, s j).restrict f)
case inl
α : 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)
h_empt : IsEmpty η
⊢ LinearIndependent (ι := ↑(⋃ j, s j)) R ((⋃ j, s j).restrict f)

case inr
α : 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 η
⊢ LinearIndependent (ι := ↑(⋃ j, s j)) R ((⋃ j, s j).restrict f)