Theorem: sqrt_𝔻_eq_𝔻 (RMT4/defs.lean)

State before:
u : ℂ
U V W : Set ℂ
⊢ {z | z ^ 2 ∈ 𝔻} = 𝔻
Tactic:
simp [𝔻, ball]
State after:
no goals