simp_rw [← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm, reProdIm]
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ [[z.re, w.re]] ×ℂ [[z.im, w.im]] = (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}
z✝ w✝ : ℂ
c : ℝ
z w : ℂ
⊢ (convexHull ℝ) (re ⁻¹' {z.re, w.re} ∩ im ⁻¹' {z.im, w.im}) =
    (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w}