no goals
ι : Type u_1
ι' : Type ?u.10411
k : Type ?u.10414
V : Type ?u.10417
P : Type ?u.10420
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
hι : IsEmpty ι
⊢ False
simpa only [@range_eq_empty _ _ hι, AffineSubspace.span_empty, bot_ne_top] using b.tot