x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ arg x = arg y ↔ arg (↑(↑abs y) / ↑(↑abs x) * x) = arg y
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ arg x = arg y ↔ ↑(↑abs y) / ↑(↑abs x) * x = y
simp only [ext_abs_arg_iff, map_mul, map_div₀, abs_ofReal, abs_abs,
  div_mul_cancel _ (abs.ne_zero hx), eq_self_iff_true, true_and_iff]
case hr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ 0 < ↑abs y / ↑abs x
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ arg x = arg y ↔ arg (↑(↑abs y) / ↑(↑abs x) * x) = arg y
rw [← ofReal_div, arg_real_mul]
no goals
case hr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ 0 < ↑abs y / ↑abs x
exact div_pos (abs.pos hy) (abs.pos hx)