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

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

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