no goals
x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).re = (log ↑x).re
rw [log_re, ofReal_re, abs_of_nonneg hx]
no goals
x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).im = (log ↑x).im
rw [ofReal_im, log_im, arg_ofReal_of_nonneg hx]