simp_all [insert_subset_iff]
z✝ w✝ : ℂ
c : ℝ
U : Set ℂ
U_convex : Convex ℝ U
z w : ℂ
hz : z ∈ U
hw : w ∈ U
hzw : ↑z.re + ↑w.im * I ∈ U
hwz : ↑w.re + ↑z.im * I ∈ U
⊢ {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w} ⊆ U
no goals