case intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ s = univ
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
⊢ s = univ
obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂
case intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ s = univ
case intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ s = univ
have : s = {p} := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])
case intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P
case intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ s = univ
rw [this, eq_comm, ← subsingleton_iff_singleton (mem_univ p), subsingleton_univ_iff]
no goals
case intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P
exact subsingleton_of_subsingleton_span_eq_top h₁ h₂
no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s : Set P
h₁ : Set.Subsingleton s
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ {p} ⊆ s
simp [hp]