-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem continuousAt_arg_coe_angle (h : x ≠ 0) : ContinuousAt ((↑) ∘ arg : ℂ → Real.Angle) x

Proof state:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (((Real.Angle.coe ∘ arg) ∘ Neg.neg) ∘ Neg.neg) x

Tactic:
refine ContinuousAt.comp ?_ continuous_neg.continuousAt

Result:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)

Proof state:
case pos
x : ℂ
h : x ≠ 0
hs : x ∈ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
exact Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg hs)

Result:
no goals

Proof state:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)

Tactic:
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⟩

Result:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π
⊢ ContinuousAt (Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)

Proof state:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
rw [← Function.comp_id (((↑) : ℝ → Real.Angle) ∘ arg),
  (funext_iff.2 fun _ => (neg_neg _).symm : (id : ℂ → ℂ) = Neg.neg ∘ Neg.neg), ←
  Function.comp_assoc]

Result:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (((Real.Angle.coe ∘ arg) ∘ Neg.neg) ∘ Neg.neg) x

Proof state:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π

Tactic:
rw [Function.update_eq_iff]

Result:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ↑π = ↑(arg 0) + ↑π ∧ ∀ (x : ℂ), x ≠ 0 → ((Real.Angle.coe ∘ arg) ∘ Neg.neg) x = ↑x.arg + ↑π

Proof state:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ↑π = ↑(arg 0) + ↑π ∧ ∀ (x : ℂ), x ≠ 0 → ((Real.Angle.coe ∘ arg) ∘ Neg.neg) x = ↑x.arg + ↑π

Tactic:
exact ⟨by simp, fun z hz => arg_neg_coe_angle hz⟩

Result:
no goals

Proof state:
x : ℂ
h : x ≠ 0
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
by_cases hs : x ∈ slitPlane

Result:
case pos
x : ℂ
h : x ≠ 0
hs : x ∈ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Proof state:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π
⊢ ContinuousAt (fun z => ↑z.arg + ↑π) (-x)

Tactic:
replace hs := mem_slitPlane_iff.mpr.mt hs

Result:
case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt (fun z => ↑z.arg + ↑π) (-x)

Proof state:
case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π
hs : ¬(0 < x.re ∨ x.im ≠ 0)
⊢ ContinuousAt (fun z => ↑z.arg + ↑π) (-x)

Tactic:
push_neg at hs

Result:
case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ ContinuousAt (fun z => ↑z.arg + ↑π) (-x)

Proof state:
case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ 0 < (-x).re

Tactic:
rw [neg_re, neg_pos]

Result:
case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ x.re < 0

Proof state:
case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ ContinuousAt (fun z => ↑z.arg + ↑π) (-x)

Tactic:
refine
  (Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg (Or.inl ?_))).add
    continuousAt_const

Result:
case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ 0 < (-x).re

Proof state:
case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ x.re < 0

Tactic:
exact hs.1.lt_of_ne fun h0 => h (Complex.ext_iff.2 ⟨h0, hs.2⟩)

Result:
no goals

Proof state:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)

Tactic:
suffices ContinuousAt (Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π) (-x) by
  rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this

Result:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)

Proof state:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π
⊢ ContinuousAt (Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)

Tactic:
rw [ha]

Result:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z => ↑z.arg + ↑π
⊢ ContinuousAt (fun z => ↑z.arg + ↑π) (-x)

Proof state:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ↑π = ↑(arg 0) + ↑π

Tactic:
simp

Result:
no goals

Proof state:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
this : ContinuousAt (Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg) (-x)

Tactic:
rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this

Result:
no goals