x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ ContinuousWithinAt arg {z | 0 ≤ z.im} z
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ContinuousWithinAt arg {z | 0 ≤ z.im} z
have : arg =ᶠ[𝓝[{ z : ℂ | 0 ≤ z.im }] z] fun x => Real.arcsin ((-x).im / abs 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]
case refine'_1
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ ContinuousWithinAt (fun x => arcsin ((-x).im / ↑abs x) + π) {z | 0 ≤ z.im} z

case refine'_2
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ arg z = arcsin ((-z).im / ↑abs z) + π
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ ContinuousWithinAt arg {z | 0 ≤ z.im} z
refine' ContinuousWithinAt.congr_of_eventuallyEq _ this _
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
⊢ arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
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
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ arg a✝ = arcsin ((-a✝).im / ↑abs a✝) + π
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
⊢ arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
filter_upwards [self_mem_nhdsWithin (s := { z : ℂ | 0 ≤ z.im }),
  mem_nhdsWithin_of_mem_nhds this] with _ him hre
no goals
case h
x z✝ 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
⊢ arg a✝ = arcsin ((-a✝).im / ↑abs a✝) + π
rw [arg, if_neg hre.not_le, if_pos him]
case refine'_1
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ ↑abs z ≠ 0
case refine'_1
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ ContinuousWithinAt (fun x => arcsin ((-x).im / ↑abs x) + π) {z | 0 ≤ z.im} z
refine'
  (Real.continuousAt_arcsin.comp_continuousWithinAt
        ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
          continuous_abs.continuousWithinAt _)).add
    tendsto_const_nhds
case refine'_1.intro
x z✝ : ℂ
z : ℝ
hre : (↑z).re < 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] ↑z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ ↑abs ↑z ≠ 0
case refine'_1
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ ↑abs z ≠ 0
lift z to ℝ using him
no goals
case refine'_1.intro
x z✝ : ℂ
z : ℝ
hre : (↑z).re < 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] ↑z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ ↑abs ↑z ≠ 0
simpa using hre.ne
no goals
case refine'_2
x z✝ z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x => arcsin ((-x).im / ↑abs x) + π
⊢ arg z = arcsin ((-z).im / ↑abs z) + π
rw [arg, if_neg hre.not_le, if_pos him.ge]