no goals
k : Type u_1
V : Type u_2
P : Type ?u.206684
ι : Type ?u.206687
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
n : ℕ
T : Simplex k V n
hrank : finrank k V = n
⊢ affineSpan k (Set.range T.points) = ⊤
rw [AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one T.Independent,
  Fintype.card_fin, hrank]