case inl.intro
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn✝ : n ≠ -1
c w : ℂ
R : ℝ
hw : w ∈ sphere c (Abs.abs R)
hn : n < -1
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0

case inr
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ¬(w ∈ sphere c (Abs.abs R) ∧ n < -1)
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
rcases em (w ∈ sphere c (|R|) ∧ n < -1) with (⟨hw, hn⟩ | H)
case inr
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
case inr
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : ¬(w ∈ sphere c (Abs.abs R) ∧ n < -1)
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
push_neg at H
case inr
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
hd : ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z => (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
z : ℂ
hz : z ∈ sphere c (Abs.abs R)
⊢ z ≠ w ∨ -1 ≤ n
case inr
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
hd : ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z => (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
refine' integral_eq_zero_of_hasDerivWithinAt' fun z hz => (hd z _).hasDerivWithinAt
no goals
case inr
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
hd : ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z => (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
z : ℂ
hz : z ∈ sphere c (Abs.abs R)
⊢ z ≠ w ∨ -1 ≤ n
exact (ne_or_eq z w).imp_right fun (h : z = w) => H <| h ▸ hz
no goals
case inl.intro
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn✝ : n ≠ -1
c w : ℂ
R : ℝ
hw : w ∈ sphere c (Abs.abs R)
hn : n < -1
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
exact integral_sub_zpow_of_undef (hn.trans (by decide)) hw
no goals
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn✝ : n ≠ -1
c w : ℂ
R : ℝ
hw : w ∈ sphere c (Abs.abs R)
hn : n < -1
⊢ -1 < 0
decide
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ HasDerivAt (fun z => (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
⊢ ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z => (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
intro z hne
case h.e'_7
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ (z - w) ^ n = ↑(n + 1) * (id z - w) ^ (n + 1 - 1) * 1 / (↑n + 1)

case convert_1
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ z ≠ w → id z - w ≠ 0

case convert_2
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ -1 ≤ n → 0 ≤ n + 1
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ HasDerivAt (fun z => (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
convert ((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z
  ((hasDerivAt_id z).sub_const w)).div_const _ using 1
no goals
case convert_1
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ z ≠ w → id z - w ≠ 0

case convert_2
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ -1 ≤ n → 0 ≤ n + 1
exacts [sub_ne_zero.2, neg_le_iff_add_nonneg.1]
case h.e'_7
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
hn' : ↑n + 1 ≠ 0
⊢ (z - w) ^ n = ↑(n + 1) * (id z - w) ^ (n + 1 - 1) * 1 / (↑n + 1)
case h.e'_7
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ (z - w) ^ n = ↑(n + 1) * (id z - w) ^ (n + 1 - 1) * 1 / (↑n + 1)
have hn' : (n + 1 : ℂ) ≠ 0 := by
  rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
no goals
case h.e'_7
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
hn' : ↑n + 1 ≠ 0
⊢ (z - w) ^ n = ↑(n + 1) * (id z - w) ^ (n + 1 - 1) * 1 / (↑n + 1)
simp [mul_assoc, mul_div_cancel_left _ hn']
no goals
E : Type ?u.690594
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c (Abs.abs R) → -1 ≤ n
z : ℂ
hne : z ≠ w ∨ -1 ≤ n
⊢ ↑n + 1 ≠ 0
rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]