@[simp]

theorem stdSimplex.coe_mk {𝕜 : Type u_1} {ι : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [Fintype ι] (f : ι → 𝕜) (hf : f ∈ stdSimplex 𝕜 ι) : ⇑⟨f, hf⟩ = f

@[simp]

theorem stdSimplex.val_eq_coe {𝕜 : Type u_1} {ι : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [Fintype ι] (f : ↑(stdSimplex 𝕜 ι)) : ↑f = ⇑f