x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
⊢ Tendsto arg (𝓝[{z | z.im < 0}] z) (𝓝 (-π))

case H
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto arg (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
suffices H :
  Tendsto (fun x : ℂ => Real.arcsin ((-x).im / abs x) - π) (𝓝[{ z : ℂ | z.im < 0 }] z) (𝓝 (-π))
case h.e'_5
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (-π) = 𝓝 ((arcsin ∘ (im ∘ Neg.neg / ↑abs)) z - π)

case H
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ↑abs z ≠ 0
case H
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
convert (Real.continuousAt_arcsin.comp_continuousWithinAt
        ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
          continuous_abs.continuousWithinAt (s := { z : ℂ | z.im < 0 }) (_ : abs z ≠ 0))
        ).sub_const π using 1
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
⊢ (fun x => arcsin ((-x).im / ↑abs x) - π) =ᶠ[𝓝[{z | z.im < 0}] z] arg
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
⊢ Tendsto arg (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
refine' H.congr' _
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
⊢ (fun x => arcsin ((-x).im / ↑abs x) - π) =ᶠ[𝓝[{z | z.im < 0}] z] arg
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
⊢ (fun x => arcsin ((-x).im / ↑abs x) - π) =ᶠ[𝓝[{z | z.im < 0}] z] arg
have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)
case h
x z✝ z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ arcsin ((-a✝).im / ↑abs a✝) - π = arg a✝
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
⊢ (fun x => arcsin ((-x).im / ↑abs x) - π) =ᶠ[𝓝[{z | z.im < 0}] z] arg
filter_upwards [self_mem_nhdsWithin (s := { z : ℂ | z.im < 0 }),
  mem_nhdsWithin_of_mem_nhds this] with _ him hre
no goals
case h
x z✝ z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x => arcsin ((-x).im / ↑abs x) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ arcsin ((-a✝).im / ↑abs a✝) - π = arg a✝
rw [arg, if_neg hre.not_le, if_neg him.not_le]
no goals
case h.e'_5
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (-π) = 𝓝 ((arcsin ∘ (im ∘ Neg.neg / ↑abs)) z - π)
simp [him]
case H.intro
x z✝ : ℂ
z : ℝ
hre : (↑z).re < 0
⊢ ↑abs ↑z ≠ 0
case H
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ↑abs z ≠ 0
lift z to ℝ using him
no goals
case H.intro
x z✝ : ℂ
z : ℝ
hre : (↑z).re < 0
⊢ ↑abs ↑z ≠ 0
simpa using hre.ne