no goals
ι : Sort ?u.134927
𝕜 : Type u_2
E : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x y : E
hs : Set.Nonempty s
⊢ ↑(convexHull 𝕜).toOrderHom (insert x s) = convexJoin 𝕜 {x} (↑(convexHull 𝕜).toOrderHom s)
rw [insert_eq, convexHull_union (singleton_nonempty _) hs, convexHull_singleton]