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
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Set.range (reindex s e).points = Set.range s.points
rw [reindex, Set.range_comp, Equiv.range_eq_univ, Set.image_univ]