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 : affineSpan k s = ⊤
⊢ s ≠ ∅
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 : affineSpan k s = ⊤
⊢ Set.Nonempty s
rw [Set.nonempty_iff_ne_empty]
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
h : affineSpan k ∅ = ⊤
⊢ False
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 : affineSpan k s = ⊤
⊢ s ≠ ∅
rintro rfl
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
h : ⊥ = ⊤
⊢ False
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
h : affineSpan k ∅ = ⊤
⊢ False
rw [AffineSubspace.span_empty] at 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
h : ⊥ = ⊤
⊢ False
exact bot_ne_top k V P h