x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
h_forall_nhds : ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
⊢ arg =ᶠ[𝓝 x] fun x => arcsin ((-x).im / ↑abs x) + π

case h_forall_nhds
x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ arg =ᶠ[𝓝 x] fun x => arcsin ((-x).im / ↑abs x) + π
suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ 0 < y.im
case h_forall_nhds
x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
h_forall_nhds : ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
⊢ arg =ᶠ[𝓝 x] fun x => arcsin ((-x).im / ↑abs x) + π

case h_forall_nhds
x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
exact h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_nonneg hy.1 hy.2.le
case h_forall_nhds
x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ IsOpen fun y => y.re < 0 ∧ 0 < y.im
case h_forall_nhds
x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
refine' IsOpen.eventually_mem _ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ 0 < x.im)
no goals
case h_forall_nhds
x z : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ IsOpen fun y => y.re < 0 ∧ 0 < y.im
exact
  IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_zero continuous_im)