-- 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θ : θ ∈ [[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‖

Tactic:
set x := ‖f θ'‖

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 θ'‖
⊢ ‖(circleMap c R θ' - circleMap c R θ)⁻¹‖ ≤ |R|⁻¹ * ‖(circleMap 0 R θ' * I) • (circleMap c R θ' - 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 θ
⊢ ∀ᶠ (θ' : ℝ) in 𝓝[≠] θ, f θ' ∈ ball 0 1 \ {0}

Tactic:
suffices ∀ᶠ z in 𝓝[≠] circleMap c R θ, z - circleMap c R θ ∈ ball (0 : ℂ) 1 \ {0} from
  ((differentiable_circleMap c R θ).hasDerivAt.tendsto_punctured_nhds
    (deriv_circleMap_ne_zero hR)).eventually this

Result:
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}

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 θ'‖
this : x ∈ Ioo 0 1
⊢ x ^ (-1) ≤ x ^ n

Tactic:
refine (zpow_right_strictAnti₀ this.1 this.2).le_iff_le.2 (Int.lt_add_one_iff.1 ?_)

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 θ'‖
this : x ∈ Ioo 0 1
⊢ n < -1 + 1

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 θ'‖
⊢ x⁻¹ ≤ x ^ n

Tactic:
have : x ∈ Ioo (0 : ℝ) 1 := by simpa [x, and_comm] using 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}
x : ℝ := ‖f θ'‖
this : x ∈ Ioo 0 1
⊢ x⁻¹ ≤ x ^ 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 θ'‖
this : x ∈ Ioo 0 1
⊢ n < -1 + 1

Tactic:
exact hn

Result:
no goals

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 θ
⊢ (fun x => (x - θ)⁻¹) =O[𝓝[≠] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n

Tactic:
have : ∀ᶠ θ' in 𝓝[≠] θ, f θ' ∈ ball (0 : ℂ) 1 \ {0} := by
  suffices ∀ᶠ z in 𝓝[≠] circleMap c R θ, z - circleMap c R θ ∈ ball (0 : ℂ) 1 \ {0} from
    ((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]

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 => (x - θ)⁻¹) =O[𝓝[≠] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n

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

Tactic:
constructor

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

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

Proof state:
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

Tactic:
simp only [circleIntegrable_iff R, deriv_circleMap]

Result:
case mp.intro.intro
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c |R|
⊢ ¬IntervalIntegrable (fun θ => (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)

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 θ'‖
⊢ x ∈ Ioo 0 1

Tactic:
simpa [x, and_comm] using hθ'

Result:
no goals

Proof state:
case mpr.inl
c w : ℂ
n : ℤ
⊢ CircleIntegrable (fun z => (z - w) ^ n) c 0

case mpr.inr
c w : ℂ
R : ℝ
n : ℤ
H : 0 ≤ n ∨ w ∉ sphere c |R|
⊢ CircleIntegrable (fun z => (z - w) ^ n) c R

Tactic:
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']

Result:
no goals

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

Tactic:
rintro (rfl | H)

Result:
case mpr.inl
c w : ℂ
n : ℤ
⊢ CircleIntegrable (fun z => (z - w) ^ n) c 0

case mpr.inr
c w : ℂ
R : ℝ
n : ℤ
H : 0 ≤ n ∨ 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}
θ' : ℝ
hθ' : f θ' ∈ ball 0 1 \ {0}
x : ℝ := ‖f θ'‖
this : x ∈ Ioo 0 1
⊢ x⁻¹ ≤ x ^ n

Tactic:
rw [← zpow_neg_one]

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 θ'‖
this : x ∈ Ioo 0 1
⊢ x ^ (-1) ≤ x ^ n

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

Tactic:
contrapose! h

Result:
case mp
c w : ℂ
R : ℝ
n : ℤ
h : R ≠ 0 ∧ n < 0 ∧ 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 * π]]
⊢ (fun x => (x - θ)⁻¹) =O[𝓝[≠] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n

Tactic:
set f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ

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 θ
⊢ (fun x => (x - θ)⁻¹) =O[𝓝[≠] θ] fun θ_1 => (circleMap 0 R θ_1 * I) • (circleMap c R θ_1 - circleMap c R θ) ^ n