Theorem: exists_linearIndependent_extension' (Matroid/ForMathlib/LinearAlgebra/LinearIndependent.lean)

State before:
α : 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
⊢ ∃ s, s₀ ⊆ s ∧ s ⊆ t ∧ f '' t ⊆ ↑(span K (f '' s)) ∧ LinearIndependent (ι := ↑s) K (s.restrict f)
Tactic:
have hzorn := zorn_subset_nonempty {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent K (r.restrict f)}
  ?_ s₀ ⟨Subset.rfl, hs₀t, hli⟩
State after:
case refine_2
α : 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
hzorn :
  ∃ m ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)},
    s₀ ⊆ m ∧ ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
⊢ ∃ s, s₀ ⊆ s ∧ s ⊆ t ∧ f '' t ⊆ ↑(span K (f '' s)) ∧ LinearIndependent (ι := ↑s) K (s.restrict f)

case refine_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'
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 ⊆ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)},
    IsChain (fun x x_1 => x ⊆ x_1) c →
      c.Nonempty → ∃ ub ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, ∀ s ∈ c, s ⊆ ub

State before:
case refine_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'
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 ⊆ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)},
    IsChain (fun x x_1 => x ⊆ x_1) c →
      c.Nonempty → ∃ ub ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, ∀ s ∈ c, s ⊆ ub
Tactic:
rintro c hcss hchain ⟨r, hr⟩
State after:
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
⊢ ∃ ub ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, ∀ s ∈ c, s ⊆ ub

State before:
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
⊢ ∃ ub ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, ∀ s ∈ c, s ⊆ ub
Tactic:
refine ⟨⋃₀ c, ⟨(hcss hr).1.trans <| subset_sUnion_of_mem hr,
  sUnion_subset fun t' ht'c ↦ (hcss ht'c).2.1,?_⟩, fun _ ↦ subset_sUnion_of_mem⟩
State after:
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)

State before:
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)
Tactic:
apply linearIndependent_sUnion_of_directed' _ _ (IsChain.directedOn hchain)
  (fun s hs ↦ (hcss hs).2.2)
State after:
no goals

State before:
case refine_2
α : 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
hzorn :
  ∃ m ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)},
    s₀ ⊆ m ∧ ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
⊢ ∃ s, s₀ ⊆ s ∧ s ⊆ t ∧ f '' t ⊆ ↑(span K (f '' s)) ∧ LinearIndependent (ι := ↑s) K (s.restrict f)
Tactic:
obtain ⟨m, ⟨hs₀m, hmt, hli⟩, -, hmax⟩ := hzorn
State after:
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
⊢ ∃ s, s₀ ⊆ s ∧ s ⊆ t ∧ f '' t ⊆ ↑(span K (f '' s)) ∧ LinearIndependent (ι := ↑s) K (s.restrict f)

State before:
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
⊢ ∃ s, s₀ ⊆ s ∧ s ⊆ t ∧ f '' t ⊆ ↑(span K (f '' s)) ∧ LinearIndependent (ι := ↑s) K (s.restrict f)
Tactic:
refine ⟨m, hs₀m, hmt, ?_, hli⟩
State after:
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))

State before:
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))
Tactic:
rintro _ ⟨x, hx, rfl⟩
State after:
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))

State before:
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))
Tactic:
by_contra hxm
State after:
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
hxm : f x ∉ ↑(span K (f '' m))
⊢ False

State before:
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
hxm : f x ∉ ↑(span K (f '' m))
⊢ False
Tactic:
have hxm' : x ∉ m := fun hxm' ↦ hxm <| subset_span <| mem_image_of_mem _ hxm'
State after:
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
hxm : f x ∉ ↑(span K (f '' m))
hxm' : x ∉ m
⊢ False

State before:
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
hxm : f x ∉ ↑(span K (f '' m))
hxm' : x ∉ m
⊢ False
Tactic:
have hli' := (linearIndependent_insert' hxm').2 ⟨hli, hxm⟩
State after:
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
hxm : f x ∉ ↑(span K (f '' m))
hxm' : x ∉ m
hli' : LinearIndependent K fun (x_1 : ↑(insert x m)) => f ↑x_1
⊢ False

State before:
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
hxm : f x ∉ ↑(span K (f '' m))
hxm' : x ∉ m
hli' : LinearIndependent K fun (x_1 : ↑(insert x m)) => f ↑x_1
⊢ False
Tactic:
rw [← hmax _ ⟨hs₀m.trans <| subset_insert _ _, insert_subset hx hmt, hli'⟩ (subset_insert _ _)]
  at hxm'
State after:
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
hxm : f x ∉ ↑(span K (f '' m))
hxm' : x ∉ insert x m
hli' : LinearIndependent K fun (x_1 : ↑(insert x m)) => f ↑x_1
⊢ False

State before:
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
hxm : f x ∉ ↑(span K (f '' m))
hxm' : x ∉ insert x m
hli' : LinearIndependent K fun (x_1 : ↑(insert x m)) => f ↑x_1
⊢ False
Tactic:
exact hxm' <| mem_insert _ _
State after:
no goals