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

case inr
E : Type ?u.619077
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c (Abs.abs R)
h0 : R ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
E : Type ?u.619077
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c (Abs.abs R)
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
rcases eq_or_ne R 0 with (rfl | h0)
no goals
case inl
E : Type ?u.619077
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
c w : ℂ
hn : n < 0
hw : w ∈ sphere c (Abs.abs 0)
⊢ (∮ (z : ℂ) in C(c, 0), (z - w) ^ n) = 0
apply integral_radius_zero
case inr.hf
E : Type ?u.619077
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c (Abs.abs R)
h0 : R ≠ 0
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R
case inr
E : Type ?u.619077
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c (Abs.abs R)
h0 : R ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), (z - w) ^ n) = 0
apply integral_undef
no goals
case inr.hf
E : Type ?u.619077
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c (Abs.abs R)
h0 : R ≠ 0
⊢ ¬CircleIntegrable (fun z => (z - w) ^ n) c R
simpa [circleIntegrable_sub_zpow_iff, *, not_or]