exact (le_sup_iff.mp hxim_le).casesOn (fun h ↦ h.trans hz'im_le) (fun h ↦ h.trans hw'im_le)
case mpr.refine_4
z✝ w✝ : ℂ
c : ℝ
z w z' w' : ℂ
hz're_ge : z.re ⊓ w.re ≤ z'.re
hz're_le : z'.re ≤ z.re ⊔ w.re
hz'im_ge : z.im ⊓ w.im ≤ z'.im
hz'im_le : z'.im ≤ z.im ⊔ w.im
hw're_ge : z.re ⊓ w.re ≤ w'.re
hw're_le : w'.re ≤ z.re ⊔ w.re
hw'im_ge : z.im ⊓ w.im ≤ w'.im
hw'im_le : w'.im ≤ z.im ⊔ w.im
x : ℂ
hxre_ge : z'.re ⊓ w'.re ≤ x.re
hxre_le : x.re ≤ z'.re ⊔ w'.re
hxim_ge : z'.im ⊓ w'.im ≤ x.im
hxim_le : x.im ≤ z'.im ⊔ w'.im
⊢ x.im ≤ z.im ⊔ w.im
no goals