no goals
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : Finset.card fs = m + 1
⊢ Set.range (face s h).points = s.points '' ↑fs
rw [face_points', Set.range_comp, Finset.range_orderEmbOfFin]