case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤

case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
h : AffineIndependent k fun p => ↑p
p₁ : P
hp₁ : p₁ ∈ s
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
h : AffineIndependent k fun p => ↑p
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
rcases s.eq_empty_or_nonempty with (rfl | ⟨p₁, hp₁⟩)
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
have p₁ : P := AddTorsor.Nonempty.some
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
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 = ⊤
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
let hsv := Basis.ofVectorSpace k V
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent k ↑hsv
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
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 = ⊤
have hsvi := hsv.linearIndependent
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent k ↑hsv
hsvt : Submodule.span k (Set.range ↑hsv) = ⊤
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent k ↑hsv
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
have hsvt := hsv.span_eq
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent k ↑hsv
hsvt : Submodule.span k (Set.range ↑hsv) = ⊤
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
rw [Basis.coe_ofVectorSpace] at hsvi hsvt
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
h0 : ∀ (v : V), v ∈ Basis.ofVectorSpaceIndex k V → v ≠ 0
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
have h0 : ∀ v : V, v ∈ Basis.ofVectorSpaceIndex _ _ → v ≠ 0 := by
  intro v hv
  simpa using hsv.ne_zero ⟨v, hv⟩
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
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 : V), v ∈ Basis.ofVectorSpaceIndex k V → v ≠ 0
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
h0 : ∀ (v : V), v ∈ Basis.ofVectorSpaceIndex k V → v ≠ 0
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k h0 p₁] at hsvi
no goals
case inl
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
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 : V), v ∈ Basis.ofVectorSpaceIndex k V → v ≠ 0
⊢ ∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
exact
  ⟨{p₁} ∪ (fun v => v +ᵥ p₁) '' _, Set.empty_subset _, hsvi,
    affineSpan_singleton_union_vadd_eq_top_of_span_eq_top p₁ hsvt⟩
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
v : V
hv : v ∈ Basis.ofVectorSpaceIndex (?m.393281 v) V
⊢ v ≠ 0
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
⊢ ∀ (v : V), v ∈ Basis.ofVectorSpaceIndex (?m.393281 v) V → v ≠ 0
intro v hv
no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
h : AffineIndependent k fun p => ↑p
p₁ : P
hsv : Basis (↑(Basis.ofVectorSpaceIndex k V)) k V := Basis.ofVectorSpace k V
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
v : V
hv : v ∈ Basis.ofVectorSpaceIndex (?m.393281 v) V
⊢ v ≠ 0
simpa using hsv.ne_zero ⟨v, hv⟩
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
h : AffineIndependent k fun p => ↑p
p₁ : P
hp₁ : p₁ ∈ s
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁] at h
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
let bsv := Basis.extend h
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k ↑bsv
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
have hsvi := bsv.linearIndependent
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k ↑bsv
hsvt : Submodule.span k (Set.range ↑bsv) = ⊤
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k ↑bsv
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
have hsvt := bsv.span_eq
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k ↑bsv
hsvt : Submodule.span k (Set.range ↑bsv) = ⊤
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
rw [Basis.coe_extend] at hsvi hsvt
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
have hsv := h.subset_extend (Set.subset_univ _)
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
h0 : ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ) → v ≠ 0
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
have h0 : ∀ v : V, v ∈ h.extend _ → v ≠ 0 := by
  intro v hv
  simpa using bsv.ne_zero ⟨v, hv⟩
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) 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₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
h0 : ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ) → v ≠ 0
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
h0 : ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ) → v ≠ 0
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k h0 p₁] at hsvi
case inr.intro.refine'_1
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) 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₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
h0 : ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ) → v ≠ 0
⊢ s ⊆ {p₁} ∪ (fun v => v +ᵥ p₁) '' LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)

case inr.intro.refine'_2
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) 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₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
h0 : ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ) → v ≠ 0
⊢ (AffineIndependent k fun p => ↑p) ∧
    affineSpan k
        ({p₁} ∪ (fun v => v +ᵥ p₁) '' LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)) =
      ⊤
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) 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₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
h0 : ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ) → v ≠ 0
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
refine' ⟨{p₁} ∪ (fun v => v +ᵥ p₁) '' h.extend (Set.subset_univ _), _, _⟩
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
v : V
hv : v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ ?m.397283 v)
⊢ v ≠ 0
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
⊢ ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ ?m.397283 v) → v ≠ 0
intro v hv
no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) k V := Basis.extend h
hsvi : LinearIndependent k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
v : V
hv : v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ ?m.397283 v)
⊢ v ≠ 0
simpa using bsv.ne_zero ⟨v, hv⟩
case inr.intro.refine'_1
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) 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₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
h0 : ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ) → v ≠ 0
⊢ s ⊆ {p₁} ∪ (fun v => v +ᵥ p₁) '' ((fun p => p -ᵥ p₁) '' (s \ {p₁}))
case inr.intro.refine'_1
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) 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₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
h0 : ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ) → v ≠ 0
⊢ s ⊆ {p₁} ∪ (fun v => v +ᵥ p₁) '' LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
refine' Set.Subset.trans _ (Set.union_subset_union_right _ (Set.image_subset _ hsv))
no goals
case inr.intro.refine'_1
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) 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₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
h0 : ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ) → v ≠ 0
⊢ s ⊆ {p₁} ∪ (fun v => v +ᵥ p₁) '' ((fun p => p -ᵥ p₁) '' (s \ {p₁}))
simp [Set.image_image]
case inr.intro.refine'_2
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) 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₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
h0 : ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ) → v ≠ 0
⊢ affineSpan k
      ({p₁} ∪ (fun v => v +ᵥ p₁) '' LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)) =
    ⊤
case inr.intro.refine'_2
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) 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₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
h0 : ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ) → v ≠ 0
⊢ (AffineIndependent k fun p => ↑p) ∧
    affineSpan k
        ({p₁} ∪ (fun v => v +ᵥ p₁) '' LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)) =
      ⊤
use hsvi
no goals
case inr.intro.refine'_2
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.391021
s : Set P
p₁ : P
h : LinearIndependent k fun v => ↑v
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ))) 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₁}) ⊆ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)
h0 : ∀ (v : V), v ∈ LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ) → v ≠ 0
⊢ affineSpan k
      ({p₁} ∪ (fun v => v +ᵥ p₁) '' LinearIndependent.extend h (_ : (fun p => p -ᵥ p₁) '' (s \ {p₁}) ⊆ Set.univ)) =
    ⊤
exact affineSpan_singleton_union_vadd_eq_top_of_span_eq_top p₁ hsvt