case h.e'_3.h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing 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
⊢ fs = Finset.map (Finset.orderEmbOfFin fs h).toEmbedding Finset.univ
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing 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
⊢ Finset.centroid k Finset.univ (face s h).points = Finset.centroid k fs s.points
convert (Finset.univ.centroid_map k (fs.orderEmbOfFin h).toEmbedding s.points).symm
case h.e'_3.h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing 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
⊢ ↑fs = Set.range ↑(Finset.orderEmbOfFin fs h).toEmbedding
case h.e'_3.h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing 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
⊢ fs = Finset.map (Finset.orderEmbOfFin fs h).toEmbedding Finset.univ
rw [← Finset.coe_inj, Finset.coe_map, Finset.coe_univ, Set.image_univ]
no goals
case h.e'_3.h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing 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
⊢ ↑fs = Set.range ↑(Finset.orderEmbOfFin fs h).toEmbedding
simp