case inl

⊢ ↑(↑abs 0) * exp (↑(arg 0) * I) = 0

case inr
x : ℂ
hx : x ≠ 0
⊢ ↑(↑abs x) * exp (↑(arg x) * I) = x
x : ℂ
⊢ ↑(↑abs x) * exp (↑(arg x) * I) = x
rcases eq_or_ne x 0 with (rfl | hx)
no goals
case inl

⊢ ↑(↑abs 0) * exp (↑(arg 0) * I) = 0
simp
case inr
x : ℂ
hx : x ≠ 0
this : ↑abs x ≠ 0
⊢ ↑(↑abs x) * exp (↑(arg x) * I) = x
case inr
x : ℂ
hx : x ≠ 0
⊢ ↑(↑abs x) * exp (↑(arg x) * I) = x
have : abs x ≠ 0 := abs.ne_zero hx
no goals
case inr
x : ℂ
hx : x ≠ 0
this : ↑abs x ≠ 0
⊢ ↑(↑abs x) * exp (↑(arg x) * I) = x
ext <;> field_simp [sin_arg, cos_arg hx, this, mul_comm (abs x)]