exact congrArg _ <| Set.ext <| by simpa [Complex.ext_iff] using by tauto
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}
no goals