E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I
have hR : 0 < R := dist_nonneg.trans_lt hw
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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

case H
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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)
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹) = 2 * ↑π * I
suffices H : HasSum (fun n : ℕ => ∮ z in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * π * I)
case H
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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)
case H
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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)
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
case H
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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)
case H
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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)
have : (∮ z in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * π * I := by simp [hR.ne']
case H
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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
case H
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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)
refine' this ▸ hasSum_single _ fun n hn => _
case H
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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
case H
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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
simp only [div_eq_mul_inv, mul_pow, integral_const_mul, mul_assoc]
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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 : ℂ), z ∈ sphere c R → (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ (-↑n - 1)
case H
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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
rw [(integral_congr hR.le fun z hz => _).trans (H n hn), mul_zero]
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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)
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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 : ℂ), z ∈ sphere c R → (z - c)⁻¹ ^ n * (z - c)⁻¹ = (z - c) ^ (-↑n - 1)
intro z _
no goals
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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)
rw [← pow_succ', ← zpow_ofNat, inv_zpow, ← zpow_neg, Int.ofNat_succ, neg_add,
  sub_eq_add_neg _ (1 : ℤ)]
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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
have A : CircleIntegrable (fun _ => (1 : ℂ)) c R := continuousOn_const.circleIntegrable'
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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)⁻¹)
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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
refine' (H.unique _).symm
no goals
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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)⁻¹)
simpa only [smul_eq_mul, mul_one, add_sub_cancel'_right] using
  hasSum_two_pi_I_cauchyPowerSeries_integral A hw
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
n : ℕ
hn : n ≠ 0
⊢ -↑n - 1 ≠ -1
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ ∀ (n : ℕ), n ≠ 0 → (∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1)) = 0
refine' fun n hn => integral_sub_zpow_of_ne _ _ _ _
no goals
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
n : ℕ
hn : n ≠ 0
⊢ -↑n - 1 ≠ -1
simpa
no goals
E : Type ?u.901462
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
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
simp [hR.ne']