case intro
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
⊢ ∃ s x, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
hne : Set.Nonempty u
⊢ ∃ s x, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
rcases hne with ⟨x, hx⟩
case intro.intro.intro.intro
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
s : Set P
hsu : s ⊆ u
hs : AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
⊢ ∃ s x, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
case intro
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
⊢ ∃ s x, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
rcases hu.exists_between_affineIndependent_span_eq_top (singleton_subset_iff.mpr hx)
  (singleton_nonempty _) (affineIndependent_of_subsingleton _ _) with ⟨s, -, hsu, hs⟩
no goals
case intro.intro.intro.intro
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
s : Set P
hsu : s ⊆ u
hs : AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
⊢ ∃ s x, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
exact ⟨s, hsu, hs⟩