-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0)
    (him : z.im = 0) : Tendsto arg (𝓝[{ z : ℂ | z.im < 0 }] z) (𝓝 (-π))

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

Tactic:
refine H.congr' ?_

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

Proof state:
case h.e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (-π) = 𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / fun a => ‖a‖)) z - π)

Tactic:
simp [him]

Result:
no goals

Proof state:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto arg (𝓝[{z | z.im < 0}] z) (𝓝 (-π))

Tactic:
suffices H : Tendsto (fun x : ℂ => Real.arcsin ((-x).im / ‖x‖) - π)
    (𝓝[{ z : ℂ | z.im < 0 }] z) (𝓝 (-π)) by
  refine H.congr' ?_
  have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)
  filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds this] with _ him hre
  rw [arg, if_neg hre.not_le, if_neg him.not_le]

Result:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto (fun x => Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))

Proof state:
case convert_3.intro
z : ℝ
hre : (↑z).re < 0
⊢ ‖↑z‖ ≠ 0

Tactic:
simpa using hre.ne

Result:
no goals

Proof state:
z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun x => Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
⊢ (fun x => Real.arcsin ((-x).im / ‖x‖) - π) =ᶠ[𝓝[{z | z.im < 0}] z] arg

Tactic:
filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds this] with _ him hre

Result:
case h
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x => Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) - π = a✝.arg

Proof state:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto (fun x => Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))

Tactic:
convert (Real.continuousAt_arcsin.comp_continuousWithinAt
  ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
    continuous_norm.continuousWithinAt _)
  ).sub_const π using 1

Result:
case h.e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (-π) = 𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / fun a => ‖a‖)) z - π)

case convert_3
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0

Proof state:
z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun x => Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
⊢ (fun x => Real.arcsin ((-x).im / ‖x‖) - π) =ᶠ[𝓝[{z | z.im < 0}] z] arg

Tactic:
have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)

Result:
z : ℂ
hre : z.re < 0
him : z.im = 0
H : Tendsto (fun x => Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
⊢ (fun x => Real.arcsin ((-x).im / ‖x‖) - π) =ᶠ[𝓝[{z | z.im < 0}] z] arg

Proof state:
case h
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x => Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) - π = a✝.arg

Tactic:
rw [arg, if_neg hre.not_le, if_neg him.not_le]

Result:
no goals

Proof state:
case convert_3
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0

Tactic:
lift z to ℝ using him

Result:
case convert_3.intro
z : ℝ
hre : (↑z).re < 0
⊢ ‖↑z‖ ≠ 0