x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h₀ : ↑abs x ≠ 0
⊢ ContinuousAt arg x
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt arg x
have h₀ : abs x ≠ 0 := by
  rw [abs.ne_zero_iff]
  rintro rfl
  simp at h
x z : ℂ
h✝ : 0 < x.re ∨ x.im ≠ 0
h : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
h₀ : ↑abs x ≠ 0
⊢ ContinuousAt arg x
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h₀ : ↑abs x ≠ 0
⊢ ContinuousAt arg x
rw [← lt_or_lt_iff_ne] at h
case inl
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h₀ : ↑abs x ≠ 0
hx_re : 0 < x.re
⊢ ContinuousAt arg x

case inr.inl
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h₀ : ↑abs x ≠ 0
hx_im : x.im < 0
⊢ ContinuousAt arg x

case inr.inr
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h₀ : ↑abs x ≠ 0
hx_im : 0 < x.im
⊢ ContinuousAt arg x
x z : ℂ
h✝ : 0 < x.re ∨ x.im ≠ 0
h : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
h₀ : ↑abs x ≠ 0
⊢ ContinuousAt arg x
rcases h with (hx_re | hx_im | hx_im)
no goals
case inl
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h₀ : ↑abs x ≠ 0
hx_re : 0 < x.re
⊢ ContinuousAt arg x

case inr.inl
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h₀ : ↑abs x ≠ 0
hx_im : x.im < 0
⊢ ContinuousAt arg x

case inr.inr
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h₀ : ↑abs x ≠ 0
hx_im : 0 < x.im
⊢ ContinuousAt arg x
exacts [(Real.continuousAt_arcsin.comp
        (continuous_im.continuousAt.div continuous_abs.continuousAt h₀)).congr
    (arg_eq_nhds_of_re_pos hx_re).symm,
  (Real.continuous_arccos.continuousAt.comp
          (continuous_re.continuousAt.div continuous_abs.continuousAt h₀)).neg.congr
    (arg_eq_nhds_of_im_neg hx_im).symm,
  (Real.continuous_arccos.continuousAt.comp
        (continuous_re.continuousAt.div continuous_abs.continuousAt h₀)).congr
    (arg_eq_nhds_of_im_pos hx_im).symm]
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ x ≠ 0
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ↑abs x ≠ 0
rw [abs.ne_zero_iff]
z : ℂ
h : 0 < 0.re ∨ 0.im ≠ 0
⊢ False
x z : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ x ≠ 0
rintro rfl
no goals
z : ℂ
h : 0 < 0.re ∨ 0.im ≠ 0
⊢ False
simp at h