-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem continuousWithinAt_arg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :
    ContinuousWithinAt arg { z : ℂ | 0 ≤ z.im } z

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

Tactic:
refine ContinuousWithinAt.congr_of_eventuallyEq ?_ this ?_

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

case refine_2
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => Real.arcsin ((-x).im / ‖x‖) + π
⊢ z.arg = Real.arcsin ((-z).im / ‖z‖) + π

Proof state:
case refine_1.intro
z : ℝ
hre : (↑z).re < 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] ↑z] fun x => Real.arcsin ((-x).im / ‖x‖) + π
⊢ ‖↑z‖ ≠ 0

Tactic:
simpa using hre.ne

Result:
no goals

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

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

Result:
no goals

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

Tactic:
filter_upwards [self_mem_nhdsWithin (s := { z : ℂ | 0 ≤ z.im }),
  mem_nhdsWithin_of_mem_nhds this] with _ him hre

Result:
case h
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ a✝.arg = Real.arcsin ((-a✝).im / ‖a✝‖) + π

Proof state:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ContinuousWithinAt arg {z | 0 ≤ z.im} z

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

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

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

Tactic:
refine
  (Real.continuousAt_arcsin.comp_continuousWithinAt
        ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
          continuous_norm.continuousWithinAt ?_)).add
    tendsto_const_nhds

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

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

Tactic:
lift z to ℝ using him

Result:
case refine_1.intro
z : ℝ
hre : (↑z).re < 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] ↑z] fun x => Real.arcsin ((-x).im / ‖x‖) + π
⊢ ‖↑z‖ ≠ 0

Proof state:
case h
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ a✝.arg = Real.arcsin ((-a✝).im / ‖a✝‖) + π

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

Result:
no goals

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

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
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
⊢ arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => Real.arcsin ((-x).im / ‖x‖) + π