case mp
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
⊢ CircleIntegrable (fun z => (z - w) ^ n) c R → R = 0 ∨ 0 ≤ n ∨ ¬w ∈ sphere c (Abs.abs R)

case mpr
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
⊢ R = 0 ∨ 0 ≤ n ∨ ¬w ∈ sphere c (Abs.abs R) → CircleIntegrable (fun z => (z - w) ^ n) c R
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
⊢ CircleIntegrable (fun z => (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ ¬w ∈ sphere c (Abs.abs R)
constructor
case mp
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
h : CircleIntegrable (fun z => (z - w) ^ n) c R
⊢ R = 0 ∨ 0 ≤ n ∨ ¬w ∈ sphere c (Abs.abs R)
case mp
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
⊢ CircleIntegrable (fun z => (z - w) ^ n) c R → R = 0 ∨ 0 ≤ n ∨ ¬w ∈ sphere c (Abs.abs R)
intro h
case mp
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c (Abs.abs R)
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R
case mp
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
h : CircleIntegrable (fun z => (z - w) ^ n) c R
⊢ R = 0 ∨ 0 ≤ n ∨ ¬w ∈ sphere c (Abs.abs R)
contrapose! h
case mp.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c (Abs.abs R)
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R
case mp
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c (Abs.abs R)
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R
rcases h with ⟨hR, hn, hw⟩
case mp.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c (Abs.abs R)
⊢ ¬IntervalIntegrable (fun θ => (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)
case mp.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c (Abs.abs R)
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R
simp only [circleIntegrable_iff R, deriv_circleMap]
case mp.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ circleMap c R '' Ioc 0 (2 * π)
⊢ ¬IntervalIntegrable (fun θ => (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)
case mp.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c (Abs.abs R)
⊢ ¬IntervalIntegrable (fun θ => (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)
rw [← image_circleMap_Ioc] at hw
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ Ioc 0 (2 * π)
⊢ ¬IntervalIntegrable (fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n) volume 0 (2 * π)
case mp.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ circleMap c R '' Ioc 0 (2 * π)
⊢ ¬IntervalIntegrable (fun θ => (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)
rcases hw with ⟨θ, hθ, rfl⟩
case hθ
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ Ioc 0 (2 * π)
⊢ θ ∈ [[0, 2 * π]]

case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
⊢ ¬IntervalIntegrable (fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n) volume 0 (2 * π)
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ Ioc 0 (2 * π)
⊢ ¬IntervalIntegrable (fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n) volume 0 (2 * π)
replace hθ : θ ∈ [[0, 2 * π]]
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
⊢ ¬IntervalIntegrable (fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n) volume 0 (2 * π)
case hθ
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ Ioc 0 (2 * π)
⊢ θ ∈ [[0, 2 * π]]

case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
⊢ ¬IntervalIntegrable (fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n) volume 0 (2 * π)
exact Icc_subset_uIcc (Ioc_subset_Icc_self hθ)
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
⊢ (fun x => (x - θ)⁻¹) =O[𝓝[{θ}ᶜ] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
⊢ ¬IntervalIntegrable (fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n) volume 0 (2 * π)
refine' not_intervalIntegrable_of_sub_inv_isBigO_punctured _ Real.two_pi_pos.ne hθ
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ (fun x => (x - θ)⁻¹) =O[𝓝[{θ}ᶜ] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
⊢ (fun x => (x - θ)⁻¹) =O[𝓝[{θ}ᶜ] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
set f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
⊢ (fun x => (x - θ)⁻¹) =O[𝓝[{θ}ᶜ] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ (fun x => (x - θ)⁻¹) =O[𝓝[{θ}ᶜ] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
have : ∀ᶠ θ' in 𝓝[≠] θ, f θ' ∈ ball (0 : ℂ) 1 \ {0} := by
  suffices : ∀ᶠ z in 𝓝[≠] circleMap c R θ, z - circleMap c R θ ∈ ball (0 : ℂ) 1 \ {0}
  exact ((differentiable_circleMap c R θ).hasDerivAt.tendsto_punctured_nhds
    (deriv_circleMap_ne_zero hR)).eventually this
  filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ball_mem_nhds _ zero_lt_one)]
  simp_all [dist_eq, sub_eq_zero]
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
⊢ (fun x => (circleMap c R x - circleMap c R θ)⁻¹) =O[𝓝 θ ⊓ 𝓟 ({θ}ᶜ)] fun θ_1 =>
    (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
⊢ (fun x => (x - θ)⁻¹) =O[𝓝[{θ}ᶜ] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
refine' (((hasDerivAt_circleMap c R θ).isBigO_sub.mono inf_le_left).inv_rev
  (this.mono fun θ' h₁ h₂ => absurd h₂ h₁.2)).trans _
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤
    (Abs.abs R)⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
⊢ (fun x => (circleMap c R x - circleMap c R θ)⁻¹) =O[𝓝 θ ⊓ 𝓟 ({θ}ᶜ)] fun θ_1 =>
    (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n
refine' IsBigO.of_bound (|R|)⁻¹ (this.mono fun θ' hθ' => _)
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤
    (Abs.abs R)⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤
    (Abs.abs R)⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖
set x := abs (f θ')
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
⊢ x⁻¹ ≤ x ^ n
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤
    (Abs.abs R)⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖
suffices x⁻¹ ≤ x ^ n by
  simpa only [inv_mul_cancel_left₀, abs_eq_zero.not.2 hR, norm_eq_abs, map_inv₀,
    Algebra.id.smul_eq_mul, map_mul, abs_circleMap_zero, abs_I, mul_one, abs_zpow, Ne.def,
    not_false_iff] using this
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
this : x ∈ Ioo 0 1
⊢ x⁻¹ ≤ x ^ n
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
⊢ x⁻¹ ≤ x ^ n
have : x ∈ Ioo (0 : ℝ) 1 := by simpa [and_comm] using hθ'
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
this : x ∈ Ioo 0 1
⊢ x ^ (-1) ≤ x ^ n
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
this : x ∈ Ioo 0 1
⊢ x⁻¹ ≤ x ^ n
rw [← zpow_neg_one]
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
this : x ∈ Ioo 0 1
⊢ n < -1 + 1
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
this : x ∈ Ioo 0 1
⊢ x ^ (-1) ≤ x ^ n
refine' (zpow_strictAnti this.1 this.2).le_iff_le.2 (Int.lt_add_one_iff.1 _)
no goals
case mp.intro.intro.intro.intro
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
this : x ∈ Ioo 0 1
⊢ n < -1 + 1
exact hn
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (z : ℂ) in 𝓝[{circleMap c R θ}ᶜ] circleMap c R θ, z - circleMap c R θ ∈ ball 0 1 \ {0}
⊢ ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}

case this
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ᶠ (z : ℂ) in 𝓝[{circleMap c R θ}ᶜ] circleMap c R θ, z - circleMap c R θ ∈ ball 0 1 \ {0}
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
suffices : ∀ᶠ z in 𝓝[≠] circleMap c R θ, z - circleMap c R θ ∈ ball (0 : ℂ) 1 \ {0}
case this
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ᶠ (z : ℂ) in 𝓝[{circleMap c R θ}ᶜ] circleMap c R θ, z - circleMap c R θ ∈ ball 0 1 \ {0}
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (z : ℂ) in 𝓝[{circleMap c R θ}ᶜ] circleMap c R θ, z - circleMap c R θ ∈ ball 0 1 \ {0}
⊢ ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}

case this
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ᶠ (z : ℂ) in 𝓝[{circleMap c R θ}ᶜ] circleMap c R θ, z - circleMap c R θ ∈ ball 0 1 \ {0}
exact ((differentiable_circleMap c R θ).hasDerivAt.tendsto_punctured_nhds
  (deriv_circleMap_ne_zero hR)).eventually this
case h
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ (a : ℂ), a ∈ {circleMap c R θ}ᶜ → a ∈ ball (circleMap c R θ) 1 → a - circleMap c R θ ∈ ball 0 1 \ {0}
case this
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ᶠ (z : ℂ) in 𝓝[{circleMap c R θ}ᶜ] circleMap c R θ, z - circleMap c R θ ∈ ball 0 1 \ {0}
filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ball_mem_nhds _ zero_lt_one)]
no goals
case h
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ (a : ℂ), a ∈ {circleMap c R θ}ᶜ → a ∈ ball (circleMap c R θ) 1 → a - circleMap c R θ ∈ ball 0 1 \ {0}
simp_all [dist_eq, sub_eq_zero]
no goals
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this✝ : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
this : x⁻¹ ≤ x ^ n
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤
    (Abs.abs R)⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖
simpa only [inv_mul_cancel_left₀, abs_eq_zero.not.2 hR, norm_eq_abs, map_inv₀,
  Algebra.id.smul_eq_mul, map_mul, abs_circleMap_zero, abs_I, mul_one, abs_zpow, Ne.def,
  not_false_iff] using this
no goals
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
this : ∀ᶠ (θ' : ℝ) in 𝓝[{θ}ᶜ] θ, f θ' ∈ ball 0 1 \ {0}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ↑Complex.abs (f θ')
⊢ x ∈ Ioo 0 1
simpa [and_comm] using hθ'
case mpr.inl
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
n : ℤ
⊢ CircleIntegrable (fun z => (z - w) ^ n) c 0

case mpr.inr
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
H : 0 ≤ n ∨ ¬w ∈ sphere c (Abs.abs R)
⊢ CircleIntegrable (fun z => (z - w) ^ n) c R
case mpr
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
⊢ R = 0 ∨ 0 ≤ n ∨ ¬w ∈ sphere c (Abs.abs R) → CircleIntegrable (fun z => (z - w) ^ n) c R
rintro (rfl | H)
no goals
case mpr.inl
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
n : ℤ
⊢ CircleIntegrable (fun z => (z - w) ^ n) c 0

case mpr.inr
E : Type ?u.111922
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
n : ℤ
H : 0 ≤ n ∨ ¬w ∈ sphere c (Abs.abs R)
⊢ CircleIntegrable (fun z => (z - w) ^ n) c R
exacts [circleIntegrable_zero_radius,
  ((continuousOn_id.sub continuousOn_const).zpow₀ _ fun z hz =>
    H.symm.imp_left fun (hw : w ∉ sphere c (|R|)) =>
      sub_ne_zero.2 <| ne_of_mem_of_not_mem hz hw).circleIntegrable']