-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem exists_subset_affineIndependent_affineSpan_eq_top {s : Set P}
    (h : AffineIndependent k (fun p => p : s → P)) :
    ∃ t : Set P, s ⊆ t ∧ AffineIndependent k (fun p => p : t → P) ∧ affineSpan k t = ⊤

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
h : LinearIndepOn k id ((fun p => p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : LinearIndepOn k id (LinearIndepOn.extend h✝ ⋯)
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
⊢ ∀ v ∈ h.extend ⋯, v ≠ 0

Tactic:
intro v hv

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
h : LinearIndepOn k id ((fun p => p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : LinearIndepOn k id (LinearIndepOn.extend h✝ ⋯)
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
v : V
hv : v ∈ h.extend ⋯
⊢ v ≠ 0

Proof state:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : AffineIndependent k fun p => ↑p
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
h0 : ∀ v ∈ Basis.ofVectorSpaceIndex k V, v ≠ 0
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤

Tactic:
exact
  ⟨{p₁} ∪ (fun v => v +ᵥ p₁) '' _, Set.empty_subset _, hsvi,
    affineSpan_singleton_union_vadd_eq_top_of_span_eq_top p₁ hsvt⟩

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
h : LinearIndepOn k id ((fun p => p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : LinearIndepOn k id (LinearIndepOn.extend h✝ ⋯)
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
v : V
hv : v ∈ h.extend ⋯
⊢ v ≠ 0

Tactic:
simpa [bsv] using bsv.ne_zero ⟨v, hv⟩

Result:
no goals

Proof state:
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
h : LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h ⋯)) k V := Basis.extend h
hsvi : LinearIndependent (ι := ↑(LinearIndepOn.extend h ⋯)) k ⇑bsv
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤

Tactic:
have hsvt := bsv.span_eq

Result:
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
h : LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h ⋯)) k V := Basis.extend h
hsvi : LinearIndependent (ι := ↑(LinearIndepOn.extend h ⋯)) k ⇑bsv
hsvt : Submodule.span k (Set.range ⇑bsv) = ⊤
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤

Proof state:
case inr.intro.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
h : LinearIndepOn k id ((fun p => p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : AffineIndependent k fun p => ↑p
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
h0 : ∀ v ∈ h.extend ⋯, v ≠ 0
⊢ s ⊆ {p₁} ∪ (fun v => v +ᵥ p₁) '' ((fun p => p -ᵥ p₁) '' (s \ {p₁}))

Tactic:
simp [Set.image_image]

Result:
no goals

Proof state:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤

Tactic:
have hsvi := hsv.linearIndependent

Result:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent (ι := ↑(Basis.ofVectorSpaceIndex k V)) k ⇑hsv
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤

Proof state:
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
h : LinearIndepOn k id ((fun p => p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : LinearIndepOn k id (LinearIndepOn.extend h✝ ⋯)
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
h0 : ∀ v ∈ h.extend ⋯, v ≠ 0
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤

Tactic:
rw [← linearIndependent_subtype_iff,
  linearIndependent_set_iff_affineIndependent_vadd_union_singleton k h0 p₁] at hsvi

Result:
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
h : LinearIndepOn k id ((fun p => p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : AffineIndependent k fun p => ↑p
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
h0 : ∀ v ∈ h.extend ⋯, v ≠ 0
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤

Proof state:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent (ι := ↑(Basis.ofVectorSpaceIndex k V)) k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
h0 : ∀ v ∈ Basis.ofVectorSpaceIndex k V, v ≠ 0
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤

Tactic:
rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k h0 p₁] at hsvi

Result:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : AffineIndependent k fun p => ↑p
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
h0 : ∀ v ∈ Basis.ofVectorSpaceIndex k V, v ≠ 0
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤