E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
have hR : 0 < R := dist_nonneg.trans_lt hw.1
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
set F : ℂ → E := dslope f w
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
have hws : (insert w s).Countable := hs.insert w
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
have hcF : ContinuousOn F (closedBall c R) :=
  (continuousOn_dslope <| closedBall_mem_nhds_of_mem hw.1).2 ⟨hc, hd _ hw⟩
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
have hdF : ∀ z ∈ ball (c : ℂ) R \ insert w s, DifferentiableAt ℂ F z := fun z hz =>
  (differentiableAt_dslope_of_ne (ne_of_mem_of_not_mem (mem_insert _ _) hz.2).symm).2
    (hd _ (diff_subset_diff_right (subset_insert _ _) hz))
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
HI : (∮ (z : ℂ) in C(c, R), F z) = 0
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
have HI := circleIntegral_eq_zero_of_differentiable_on_off_countable hR.le hws hcF hdF
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
HI : (∮ (z : ℂ) in C(c, R), F z) = 0
hne : ∀ (z : ℂ), z ∈ sphere c R → z ≠ w
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
HI : (∮ (z : ℂ) in C(c, R), F z) = 0
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
have hne : ∀ z ∈ sphere c R, z ≠ w := fun z hz => ne_of_mem_of_not_mem hz (ne_of_lt hw.1)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
HI : (∮ (z : ℂ) in C(c, R), F z) = 0
hne : ∀ (z : ℂ), z ∈ sphere c R → z ≠ w
hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
HI : (∮ (z : ℂ) in C(c, R), F z) = 0
hne : ∀ (z : ℂ), z ∈ sphere c R → z ≠ w
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
have hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R) := fun z hz ↦
  calc
    F z = (z - w)⁻¹ • (f z - f w) := update_noteq (hne z hz) _ _
    _ = (z - w)⁻¹ • f z - (z - w)⁻¹ • f w := smul_sub _ _ _
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
HI : (∮ (z : ℂ) in C(c, R), F z) = 0
hne : ∀ (z : ℂ), z ∈ sphere c R → z ≠ w
hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R)
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
HI : (∮ (z : ℂ) in C(c, R), F z) = 0
hne : ∀ (z : ℂ), z ∈ sphere c R → z ≠ w
hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
have hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R) :=
  (continuousOn_id.sub continuousOn_const).inv₀ fun z hz => sub_ne_zero.2 <| hne z hz
case hf
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
HI : (∮ (z : ℂ) in C(c, R), F z) = 0
hne : ∀ (z : ℂ), z ∈ sphere c R → z ≠ w
hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R)
⊢ CircleIntegrable (fun z => (z - w)⁻¹ • f z) c R

case hg
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
HI : (∮ (z : ℂ) in C(c, R), F z) = 0
hne : ∀ (z : ℂ), z ∈ sphere c R → z ≠ w
hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R)
⊢ CircleIntegrable (fun z => (z - w)⁻¹ • f w) c R
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
HI : (∮ (z : ℂ) in C(c, R), F z) = 0
hne : ∀ (z : ℂ), z ∈ sphere c R → z ≠ w
hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R)
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
rw [← circleIntegral.integral_sub_inv_of_mem_ball hw.1, ← circleIntegral.integral_smul_const, ←
  sub_eq_zero, ← circleIntegral.integral_sub, ← circleIntegral.integral_congr hR.le hFeq, HI]
no goals
case hf
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
HI : (∮ (z : ℂ) in C(c, R), F z) = 0
hne : ∀ (z : ℂ), z ∈ sphere c R → z ≠ w
hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R)
⊢ CircleIntegrable (fun z => (z - w)⁻¹ • f z) c R

case hg
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R \ s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
hR : 0 < R
F : ℂ → E := dslope f w
hws : Set.Countable (insert w s)
hcF : ContinuousOn F (closedBall c R)
hdF : ∀ (z : ℂ), z ∈ ball c R \ insert w s → DifferentiableAt ℂ F z
HI : (∮ (z : ℂ) in C(c, R), F z) = 0
hne : ∀ (z : ℂ), z ∈ sphere c R → z ≠ w
hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)
hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R)
⊢ CircleIntegrable (fun z => (z - w)⁻¹ • f w) c R
exacts [(hc'.smul (hc.mono sphere_subset_closedBall)).circleIntegrable hR.le,
  (hc'.smul continuousOn_const).circleIntegrable hR.le]