-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem circleIntegrable_sub_zpow_iff {c w : ℂ} {R : ℝ} {n : ℤ} :
    CircleIntegrable (fun z => (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|

Proof state:
case mp.intro.intro.intro.intro
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 * π)

Tactic:
replace hθ : θ ∈ [[0, 2 * π]] := Icc_subset_uIcc (Ioc_subset_Icc_self hθ)

Result:
case mp.intro.intro.intro.intro
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 * π)

Proof state:
case mp
c w : ℂ
R : ℝ
n : ℤ
h : R ≠ 0 ∧ n < 0 ∧ w ∈ sphere c |R|
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R

Tactic:
rcases h with ⟨hR, hn, hw⟩

Result:
case mp.intro.intro
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c |R|
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R

Proof state:
case mp.intro.intro.intro.intro
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

Tactic:
refine IsBigO.of_bound |R|⁻¹ (this.mono fun θ' hθ' => ?_)

Result:
case mp.intro.intro.intro.intro
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 θ)⁻¹‖ ≤ |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖

Proof state:
case mp.intro.intro.intro.intro
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

Tactic:
refine (((hasDerivAt_circleMap c R θ).isBigO_sub.mono inf_le_left).inv_rev
  (this.mono fun θ' h₁ h₂ => absurd h₂ h₁.2)).trans ?_

Result:
case mp.intro.intro.intro.intro
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

Proof state:
case mp.intro.intro.intro.intro
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 : ℝ := ‖f θ'‖
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤ |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖

Tactic:
suffices x⁻¹ ≤ x ^ n by
  simp only [inv_mul_cancel_left₀, abs_eq_zero.not.2 hR, Algebra.id.smul_eq_mul, norm_mul,
    norm_inv, norm_I, mul_one]
  simpa only [norm_circleMap_zero, norm_zpow, Ne, abs_eq_zero.not.2 hR, not_false_iff,
    inv_mul_cancel_left₀] using this

Result:
case mp.intro.intro.intro.intro
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 : ℝ := ‖f θ'‖
⊢ x⁻¹ ≤ x ^ n

Proof state:
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 : ℝ := ‖f θ'‖
this : x⁻¹ ≤ x ^ n
⊢ ‖circleMap c R θ' - circleMap c R θ‖⁻¹ ≤ |R|⁻¹ * (‖circleMap 0 R θ'‖ * ‖(circleMap c R θ' - circleMap c R θ) ^ n‖)

Tactic:
simpa only [norm_circleMap_zero, norm_zpow, Ne, abs_eq_zero.not.2 hR, not_false_iff,
  inv_mul_cancel_left₀] using this

Result:
no goals

Proof state:
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 θ, z - circleMap c R θ ∈ ball 0 1 \ {0}

Tactic:
filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ball_mem_nhds _ zero_lt_one)]

Result:
case h
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ a ∈ {circleMap c R θ}ᶜ, a ∈ ball (circleMap c R θ) 1 → a - circleMap c R θ ∈ ball 0 1 \ {0}

Proof state:
case h
c : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
θ : ℝ
hθ : θ ∈ [[0, 2 * π]]
f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
⊢ ∀ a ∈ {circleMap c R θ}ᶜ, a ∈ ball (circleMap c R θ) 1 → a - circleMap c R θ ∈ ball 0 1 \ {0}

Tactic:
simp_all [dist_eq, sub_eq_zero]

Result:
no goals

Proof state:
case mp.intro.intro
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 * π)

Tactic:
rcases hw with ⟨θ, hθ, rfl⟩

Result:
case mp.intro.intro.intro.intro
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 * π)

Proof state:
case mp
c w : ℂ
R : ℝ
n : ℤ
⊢ CircleIntegrable (fun z => (z - w) ^ n) c R → R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|

Tactic:
intro h

Result:
case mp
c w : ℂ
R : ℝ
n : ℤ
h : CircleIntegrable (fun z => (z - w) ^ n) c R
⊢ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|

Proof state:
case mp.intro.intro.intro.intro
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 * π)

Tactic:
refine not_intervalIntegrable_of_sub_inv_isBigO_punctured ?_ Real.two_pi_pos.ne hθ

Result:
case mp.intro.intro.intro.intro
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

Proof state:
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 : ℝ := ‖f θ'‖
this : x⁻¹ ≤ x ^ n
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤ |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - circleMap c R θ) ^ n‖

Tactic:
simp only [inv_mul_cancel_left₀, abs_eq_zero.not.2 hR, Algebra.id.smul_eq_mul, norm_mul,
  norm_inv, norm_I, mul_one]

Result:
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 : ℝ := ‖f θ'‖
this : x⁻¹ ≤ x ^ n
⊢ ‖circleMap c R θ' - circleMap c R θ‖⁻¹ ≤ |R|⁻¹ * (‖circleMap 0 R θ'‖ * ‖(circleMap c R θ' - circleMap c R θ) ^ n‖)