Theorem: Ex113.ex1_1_3' (AlgebraI/Groups.lean)

State before:
⊢ {z | ‖z‖ = 1} = {x | ∃ θ, Complex.exp (↑θ * Complex.I) = x}
Tactic:
ext z
State after:
case h
z : ℂ
⊢ z ∈ {z | ‖z‖ = 1} ↔ z ∈ {x | ∃ θ, Complex.exp (↑θ * Complex.I) = x}

State before:
case h
z : ℂ
⊢ z ∈ {z | ‖z‖ = 1} ↔ z ∈ {x | ∃ θ, Complex.exp (↑θ * Complex.I) = x}
Tactic:
simp only [Complex.norm_eq_abs, Set.mem_setOf_eq, Complex.abs_eq_one_iff]
State after:
no goals