case refine'_1
z : ℂ
hz : ↑abs z = 1
⊢ exp (↑(arg z) * I) = z

case refine'_2
z : ℂ
⊢ (∃ θ, exp (↑θ * I) = z) → ↑abs z = 1
z : ℂ
⊢ ↑abs z = 1 ↔ ∃ θ, exp (↑θ * I) = z
refine' ⟨fun hz => ⟨arg z, _⟩, _⟩
no goals
case refine'_1
z : ℂ
hz : ↑abs z = 1
⊢ exp (↑(arg z) * I) = z
calc
  exp (arg z * I) = abs z * exp (arg z * I) := by rw [hz, ofReal_one, one_mul]
  _ = z := abs_mul_exp_arg_mul_I z
no goals
z : ℂ
hz : ↑abs z = 1
⊢ exp (↑(arg z) * I) = ↑(↑abs z) * exp (↑(arg z) * I)
rw [hz, ofReal_one, one_mul]
case refine'_2.intro
θ : ℝ
⊢ ↑abs (exp (↑θ * I)) = 1
case refine'_2
z : ℂ
⊢ (∃ θ, exp (↑θ * I) = z) → ↑abs z = 1
rintro ⟨θ, rfl⟩
no goals
case refine'_2.intro
θ : ℝ
⊢ ↑abs (exp (↑θ * I)) = 1
exact Complex.abs_exp_ofReal_mul_I θ