case h
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
i : Fin (n + 1)
i✝ : Fin (0 + 1)
⊢ points (face s (_ : Finset.card {i} = 1)) i✝ = points (mkOfPoint k (points s i)) i✝
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
i : Fin (n + 1)
⊢ face s (_ : Finset.card {i} = 1) = mkOfPoint k (points s i)
ext
case h
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
i : Fin (n + 1)
i✝ : Fin (0 + 1)
⊢ points s (↑(Finset.orderEmbOfFin {i} (_ : Finset.card {i} = 1)) i✝) = points s i
case h
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
i : Fin (n + 1)
i✝ : Fin (0 + 1)
⊢ points (face s (_ : Finset.card {i} = 1)) i✝ = points (mkOfPoint k (points s i)) i✝
simp only [Affine.Simplex.mkOfPoint_points, Affine.Simplex.face_points]
no goals
case h
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
i : Fin (n + 1)
i✝ : Fin (0 + 1)
⊢ points s (↑(Finset.orderEmbOfFin {i} (_ : Finset.card {i} = 1)) i✝) = points s i
rw [Finset.orderEmbOfFin_singleton]