-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem integral_sub_inv_of_mem_ball {c w : ℂ} {R : ℝ} (hw : w ∈ ball c R) :
    (∮ z in C(c, R), (z - w)⁻¹) = 2 * π * I

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)

Tactic:
refine this ▸ hasSum_single _ fun n hn => ?_

Result:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) = 0

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
z : ℂ
hz✝ : z ∈ sphere c R
⊢ (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ (-↑n - 1)

Tactic:
rw [← pow_succ, ← zpow_natCast, inv_zpow, ← zpow_neg, Int.ofNat_succ, neg_add,
  sub_eq_add_neg _ (1 : ℤ)]

Result:
no goals

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
⊢ ∀ z ∈ sphere c R, (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ (-↑n - 1)

Tactic:
intro z _

Result:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
z : ℂ
hz✝ : z ∈ sphere c R
⊢ (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ (-↑n - 1)

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
A : CircleIntegrable (fun x => 1) c R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I

Tactic:
refine (H.unique ?_).symm

Result:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
A : CircleIntegrable (fun x => 1) c R
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (∮ (z : ℂ) in C(c, R), (z - w)⁻¹)

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
⊢ (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I

Tactic:
simp [hR.ne']

Result:
no goals

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)

Tactic:
have : (∮ z in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * π * I := by simp [hR.ne']

Result:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0

Tactic:
refine fun n hn => integral_sub_zpow_of_ne ?_ _ _ _

Result:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
n : ℕ
hn : n ≠ 0
⊢ -↑n - 1 ≠ -1

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)

Tactic:
have H : ∀ n : ℕ, n ≠ 0 → (∮ z in C(c, R), (z - c) ^ (-n - 1 : ℤ)) = 0 := by
  refine fun n hn => integral_sub_zpow_of_ne ?_ _ _ _; simpa

Result:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I

Tactic:
have hR : 0 < R := dist_nonneg.trans_lt hw

Result:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
⊢ ((w - c) ^ n * ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n * (z - c)⁻¹) = 0

Tactic:
rw [(integral_congr hR.le fun z hz => _).trans (H n hn), mul_zero]

Result:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
⊢ ∀ z ∈ sphere c R, (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ (-↑n - 1)

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I

Tactic:
suffices H : HasSum (fun n : ℕ => ∮ z in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹)
    (2 * π * I) by
  have A : CircleIntegrable (fun _ => (1 : ℂ)) c R := continuousOn_const.circleIntegrable'
  refine (H.unique ?_).symm
  simpa only [smul_eq_mul, mul_one, add_sub_cancel] using
    hasSum_two_pi_I_cauchyPowerSeries_integral A hw

Result:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
A : CircleIntegrable (fun x => 1) c R
⊢ HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (∮ (z : ℂ) in C(c, R), (z - w)⁻¹)

Tactic:
simpa only [smul_eq_mul, mul_one, add_sub_cancel] using
  hasSum_two_pi_I_cauchyPowerSeries_integral A hw

Result:
no goals

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) = 0

Tactic:
simp only [div_eq_mul_inv, mul_pow, integral_const_mul, mul_assoc]

Result:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
this : (∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
⊢ ((w - c) ^ n * ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n * (z - c)⁻¹) = 0

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I

Tactic:
have A : CircleIntegrable (fun _ => (1 : ℂ)) c R := continuousOn_const.circleIntegrable'

Result:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : HasSum (fun n => ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
A : CircleIntegrable (fun x => 1) c R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I

Proof state:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
n : ℕ
hn : n ≠ 0
⊢ -↑n - 1 ≠ -1

Tactic:
simpa

Result:
no goals