case pos
x : ℂ
h : x = 0
⊢ Real.tan (arg x) = x.im / x.re

case neg
x : ℂ
h : ¬x = 0
⊢ Real.tan (arg x) = x.im / x.re
x : ℂ
⊢ Real.tan (arg x) = x.im / x.re
by_cases h : x = 0
no goals
case neg
x : ℂ
h : ¬x = 0
⊢ Real.tan (arg x) = x.im / x.re
rw [Real.tan_eq_sin_div_cos, sin_arg, cos_arg h, div_div_div_cancel_right _ (abs.ne_zero h)]
no goals
case pos
x : ℂ
h : x = 0
⊢ Real.tan (arg x) = x.im / x.re
simp only [h, zero_div, Complex.zero_im, Complex.arg_zero, Real.tan_zero, Complex.zero_re]