no goals
ι : Sort ?u.137089
𝕜 : Type u_2
E : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x y a b c d : E
⊢ convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = ↑(convexHull 𝕜).toOrderHom {a, b, c, d}
simp_rw [← convexHull_pair, convexHull_insert (insert_nonempty _ _),
  convexHull_insert (singleton_nonempty _), convexJoin_assoc,
  convexHull_singleton]