case a
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z.re = (↑z.re).re

case a
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z.im = (↑z.re).im
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z = ↑z.re
ext
case a
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z.im = (↑z.re).im
case a
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z.re = (↑z.re).re

case a
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z.im = (↑z.re).im
rfl
no goals
case a
r : ℝ
z : ℂ
hz : ↑r ≤ z
⊢ z.im = (↑z.re).im
simp only [← (Complex.le_def.1 hz).2, Complex.zero_im, Complex.ofReal_im]