-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem exists_linearIndepOn_id_extension (hs : LinearIndepOn K id s) (hst : s ⊆ t) :
    ∃ b ⊆ t, s ⊆ b ∧ t ⊆ span K b ∧ LinearIndepOn K id b

Proof state:
case refine_3
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
c : Set (Set V)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K id b}
cc : IsChain (fun x1 x2 => x1 ⊆ x2) c
_c0 : c.Nonempty
x : Set V
⊢ x ∈ c → x ⊆ ⋃₀ c

Tactic:
exact subset_sUnion_of_mem

Result:
no goals

Proof state:
case intro.intro
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
b : Set V
sb : s ⊆ b
h : Maximal (fun x => x ∈ {b | b ⊆ t ∧ LinearIndepOn K id b}) b
⊢ ∃ b ⊆ t, s ⊆ b ∧ t ⊆ ↑(span K b) ∧ LinearIndepOn K id b

Tactic:
refine ⟨b, h.prop.1, sb, fun x xt => by_contra fun hn ↦ hn ?_, h.prop.2⟩

Result:
case intro.intro
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
b : Set V
sb : s ⊆ b
h : Maximal (fun x => x ∈ {b | b ⊆ t ∧ LinearIndepOn K id b}) b
x : V
xt : x ∈ t
hn : x ∉ ↑(span K b)
⊢ x ∈ ↑(span K b)

Proof state:
case refine_2
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
c : Set (Set V)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K id b}
cc : IsChain (fun x1 x2 => x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ LinearIndepOn K id (⋃₀ c)

Tactic:
exact linearIndepOn_sUnion_of_directed cc.directedOn fun x xc => (hc xc).2

Result:
no goals

Proof state:
case intro.intro
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
b : Set V
sb : s ⊆ b
h : Maximal (fun x => x ∈ {b | b ⊆ t ∧ LinearIndepOn K id b}) b
x : V
xt : x ∈ t
hn : x ∉ ↑(span K b)
⊢ x ∈ ↑(span K b)

Tactic:
exact subset_span <| h.mem_of_prop_insert ⟨insert_subset xt h.prop.1, h.prop.2.insert hn⟩

Result:
no goals

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ ∀ c ⊆ {b | b ⊆ t ∧ LinearIndepOn K id b},
    IsChain (fun x1 x2 => x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ {b | b ⊆ t ∧ LinearIndepOn K id b}, ∀ s ∈ c, s ⊆ ub

Tactic:
refine fun c hc cc _c0 => ⟨⋃₀ c, ⟨?_, ?_⟩, fun x => ?_⟩

Result:
case refine_1
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
c : Set (Set V)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K id b}
cc : IsChain (fun x1 x2 => x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ⋃₀ c ⊆ t

case refine_2
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
c : Set (Set V)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K id b}
cc : IsChain (fun x1 x2 => x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ LinearIndepOn K id (⋃₀ c)

case refine_3
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
c : Set (Set V)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K id b}
cc : IsChain (fun x1 x2 => x1 ⊆ x2) c
_c0 : c.Nonempty
x : Set V
⊢ x ∈ c → x ⊆ ⋃₀ c

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ ?m.265209

Tactic:
refine zorn_subset_nonempty { b | b ⊆ t ∧ LinearIndepOn K id b} ?_ _ ⟨hst, hs⟩

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ ∀ c ⊆ {b | b ⊆ t ∧ LinearIndepOn K id b},
    IsChain (fun x1 x2 => x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ {b | b ⊆ t ∧ LinearIndepOn K id b}, ∀ s ∈ c, s ⊆ ub

Proof state:
case refine_1
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
c : Set (Set V)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K id b}
cc : IsChain (fun x1 x2 => x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ⋃₀ c ⊆ t

Tactic:
exact sUnion_subset fun x xc => (hc xc).1

Result:
no goals