case pos
x z : ℂ
h : x ≠ 0
hs : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt (Angle.coe ∘ arg) x

case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt (Angle.coe ∘ arg) x
x z : ℂ
h : x ≠ 0
⊢ ContinuousAt (Angle.coe ∘ arg) x
by_cases hs : 0 < x.re ∨ x.im ≠ 0
no goals
case pos
x z : ℂ
h : x ≠ 0
hs : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt (Angle.coe ∘ arg) x
exact Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg hs)
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt (((Angle.coe ∘ arg) ∘ Neg.neg) ∘ Neg.neg) x
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt (Angle.coe ∘ arg) x
rw [← Function.comp.right_id (((↑) : ℝ → Real.Angle) ∘ arg),
  (Function.funext_iff.2 fun _ => (neg_neg _).symm : (id : ℂ → ℂ) = Neg.neg ∘ Neg.neg), ←
  Function.comp.assoc]
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt ((Angle.coe ∘ arg) ∘ Neg.neg) (-x)
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt (((Angle.coe ∘ arg) ∘ Neg.neg) ∘ Neg.neg) x
refine' ContinuousAt.comp _ continuous_neg.continuousAt
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt (Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt ((Angle.coe ∘ arg) ∘ Neg.neg) (-x)
suffices ContinuousAt (Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π) (-x) by
  rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
⊢ ContinuousAt (Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt (Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)
have ha :
  Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π = fun z =>
    (arg z : Real.Angle) + π := by
  rw [Function.update_eq_iff]
  exact ⟨by simp, fun z hz => arg_neg_coe_angle hz⟩
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
⊢ ContinuousAt (fun z => ↑(arg z) + ↑π) (-x)
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
⊢ ContinuousAt (Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)
rw [ha]
case neg
x z : ℂ
h : x ≠ 0
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ ContinuousAt (fun z => ↑(arg z) + ↑π) (-x)
case neg
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
⊢ ContinuousAt (fun z => ↑(arg z) + ↑π) (-x)
push_neg  at hs
case neg
x z : ℂ
h : x ≠ 0
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ 0 < (-x).re
case neg
x z : ℂ
h : x ≠ 0
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ ContinuousAt (fun z => ↑(arg z) + ↑π) (-x)
refine'
  (Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg (Or.inl _))).add
    continuousAt_const
case neg
x z : ℂ
h : x ≠ 0
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ x.re < 0
case neg
x z : ℂ
h : x ≠ 0
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ 0 < (-x).re
rw [neg_re, neg_pos]
no goals
case neg
x z : ℂ
h : x ≠ 0
ha : Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ x.re < 0
exact hs.1.lt_of_ne fun h0 => h (ext_iff.2 ⟨h0, hs.2⟩)
no goals
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
this : ContinuousAt (Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)
⊢ ContinuousAt ((Angle.coe ∘ arg) ∘ Neg.neg) (-x)
rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ↑π = ↑(arg 0) + ↑π ∧ ∀ (x : ℂ), x ≠ 0 → ((Angle.coe ∘ arg) ∘ Neg.neg) x = ↑(arg x) + ↑π
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ Function.update ((Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑(arg z) + ↑π
rw [Function.update_eq_iff]
no goals
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ↑π = ↑(arg 0) + ↑π ∧ ∀ (x : ℂ), x ≠ 0 → ((Angle.coe ∘ arg) ∘ Neg.neg) x = ↑(arg x) + ↑π
exact ⟨by simp, fun z hz => arg_neg_coe_angle hz⟩
no goals
x z : ℂ
h : x ≠ 0
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ↑π = ↑(arg 0) + ↑π
simp