rintro _ ⟨x, hx, rfl⟩
case refine_2.intro.intro.intro.intro.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
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
⊢ f '' t ⊆ ↑(span K (f '' m))
case refine_2.intro.intro.intro.intro.intro.intro.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
m : Set ι
hs₀m : s₀ ⊆ m
hmt : m ⊆ t
hli : LinearIndependent (ι := ↑m) K (m.restrict f)
hmax : ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
x : ι
hx : x ∈ t
⊢ f x ∈ ↑(span K (f '' m))