case inl
r : ℝ
hr : 0 < r
⊢ arg (↑r * 0) = arg 0

case inr
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
⊢ arg (↑r * x) = arg x
x : ℂ
r : ℝ
hr : 0 < r
⊢ arg (↑r * x) = arg x
rcases eq_or_ne x 0 with (rfl | hx)
no goals
case inr
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
⊢ arg (↑r * x) = arg x
conv_lhs =>
  rw [← abs_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
    arg_mul_cos_add_sin_mul_I (mul_pos hr (abs.pos hx)) x.arg_mem_Ioc]
no goals
case inl
r : ℝ
hr : 0 < r
⊢ arg (↑r * 0) = arg 0
rw [MulZeroClass.mul_zero]