[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[{c}ᶜ] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
⊢ AnalyticAt ℂ f c
[PROOFSTEP]
rcases(nhdsWithin_hasBasis nhds_basis_closedBall _).mem_iff.1 hd with ⟨R, hR0, hRs⟩
[GOAL]
case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[{c}ᶜ] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ
hR0 : 0 < R
hRs : closedBall c R ∩ {c}ᶜ ⊆ {x | (fun z => DifferentiableAt ℂ f z) x}
⊢ AnalyticAt ℂ f c
[PROOFSTEP]
lift R to ℝ≥0 using hR0.le
[GOAL]
case intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[{c}ᶜ] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < ↑R
hRs : closedBall c ↑R ∩ {c}ᶜ ⊆ {x | (fun z => DifferentiableAt ℂ f z) x}
⊢ AnalyticAt ℂ f c
[PROOFSTEP]
replace hc : ContinuousOn f (closedBall c R)
[GOAL]
case hc
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[{c}ᶜ] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < ↑R
hRs : closedBall c ↑R ∩ {c}ᶜ ⊆ {x | (fun z => DifferentiableAt ℂ f z) x}
⊢ ContinuousOn f (closedBall c ↑R)
[PROOFSTEP]
refine' fun z hz => ContinuousAt.continuousWithinAt _
[GOAL]
case hc
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[{c}ᶜ] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < ↑R
hRs : closedBall c ↑R ∩ {c}ᶜ ⊆ {x | (fun z => DifferentiableAt ℂ f z) x}
z : ℂ
hz : z ∈ closedBall c ↑R
⊢ ContinuousAt f z
[PROOFSTEP]
rcases eq_or_ne z c with (rfl | hne)
[GOAL]
case hc.inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ≥0
hR0 : 0 < ↑R
z : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[{z}ᶜ] z, DifferentiableAt ℂ f z
hc : ContinuousAt f z
hRs : closedBall z ↑R ∩ {z}ᶜ ⊆ {x | (fun z => DifferentiableAt ℂ f z) x}
hz : z ∈ closedBall z ↑R
⊢ ContinuousAt f z
case hc.inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[{c}ᶜ] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < ↑R
hRs : closedBall c ↑R ∩ {c}ᶜ ⊆ {x | (fun z => DifferentiableAt ℂ f z) x}
z : ℂ
hz : z ∈ closedBall c ↑R
hne : z ≠ c
⊢ ContinuousAt f z
[PROOFSTEP]
exacts [hc, (hRs ⟨hz, hne⟩).continuousAt]
[GOAL]
case intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[{c}ᶜ] c, DifferentiableAt ℂ f z
R : ℝ≥0
hR0 : 0 < ↑R
hRs : closedBall c ↑R ∩ {c}ᶜ ⊆ {x | (fun z => DifferentiableAt ℂ f z) x}
hc : ContinuousOn f (closedBall c ↑R)
⊢ AnalyticAt ℂ f c
[PROOFSTEP]
exact
  (hasFPowerSeriesOnBall_of_differentiable_off_countable (countable_singleton c) hc
      (fun z hz => hRs (diff_subset_diff_left ball_subset_closedBall hz)) hR0).analyticAt
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
⊢ DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c ↔ DifferentiableOn ℂ f s
[PROOFSTEP]
refine' ⟨_, fun hd => ⟨hd.mono (diff_subset _ _), (hd.differentiableAt hs).continuousAt⟩⟩
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
⊢ DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c → DifferentiableOn ℂ f s
[PROOFSTEP]
rintro ⟨hd, hc⟩ x hx
[GOAL]
case intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
hc : ContinuousAt f c
x : ℂ
hx : x ∈ s
⊢ DifferentiableWithinAt ℂ f s x
[PROOFSTEP]
rcases eq_or_ne x c with (rfl | hne)
[GOAL]
case intro.inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
⊢ DifferentiableWithinAt ℂ f s x
[PROOFSTEP]
refine' (analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt _ hc).differentiableAt.differentiableWithinAt
[GOAL]
case intro.inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
⊢ ∀ᶠ (z : ℂ) in 𝓝[{x}ᶜ] x, DifferentiableAt ℂ f z
[PROOFSTEP]
refine' eventually_nhdsWithin_iff.2 ((eventually_mem_nhds.2 hs).mono fun z hz hzx => _)
[GOAL]
case intro.inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
x : ℂ
hx : x ∈ s
hs : s ∈ 𝓝 x
hd : DifferentiableOn ℂ f (s \ {x})
hc : ContinuousAt f x
z : ℂ
hz : s ∈ 𝓝 z
hzx : z ∈ {x}ᶜ
⊢ DifferentiableAt ℂ f z
[PROOFSTEP]
exact hd.differentiableAt (inter_mem hz (isOpen_ne.mem_nhds hzx))
[GOAL]
case intro.inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hs : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
hc : ContinuousAt f c
x : ℂ
hx : x ∈ s
hne : x ≠ c
⊢ DifferentiableWithinAt ℂ f s x
[PROOFSTEP]
simpa only [DifferentiableWithinAt, HasFDerivWithinAt, hne.nhdsWithin_diff_singleton] using hd x ⟨hx, hne⟩
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
[PROOFSTEP]
set F : ℂ → E := fun z => (z - c) • f z
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
[PROOFSTEP]
suffices DifferentiableOn ℂ F (s \ { c }) ∧ ContinuousAt F c
  by
  rw [differentiableOn_compl_singleton_and_continuousAt_iff hc, ← differentiableOn_dslope hc, dslope_sub_smul] at this 
  have hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c)) := continuousAt_update_same.mp (this.continuousOn.continuousAt hc)
  rwa [hc.limUnder_eq]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this : DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
[PROOFSTEP]
rw [differentiableOn_compl_singleton_and_continuousAt_iff hc, ← differentiableOn_dslope hc, dslope_sub_smul] at this 
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this✝ : DifferentiableOn ℂ (dslope F c) s
this : DifferentiableOn ℂ (update (fun z => f z) c (deriv (fun x => (x - c) • f x) c)) s
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
[PROOFSTEP]
have hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c)) := continuousAt_update_same.mp (this.continuousOn.continuousAt hc)
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc✝ : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this✝ : DifferentiableOn ℂ (dslope F c) s
this : DifferentiableOn ℂ (update (fun z => f z) c (deriv (fun x => (x - c) • f x) c)) s
hc : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (deriv F c))
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
[PROOFSTEP]
rwa [hc.limUnder_eq]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c
[PROOFSTEP]
refine' ⟨(differentiableOn_id.sub_const _).smul hd, _⟩
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ ContinuousAt F c
[PROOFSTEP]
rw [← continuousWithinAt_compl_self]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ ContinuousWithinAt F {c}ᶜ c
[PROOFSTEP]
have H := ho.tendsto_inv_smul_nhds_zero
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
H : Tendsto (fun x => (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[{c}ᶜ] c) (𝓝 0)
⊢ ContinuousWithinAt F {c}ᶜ c
[PROOFSTEP]
have H' : Tendsto (fun z => (z - c) • f c) (𝓝[≠] c) (𝓝 (F c)) :=
  (continuousWithinAt_id.tendsto.sub tendsto_const_nhds).smul tendsto_const_nhds
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
H : Tendsto (fun x => (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[{c}ᶜ] c) (𝓝 0)
H' : Tendsto (fun z => (z - c) • f c) (𝓝[{c}ᶜ] c) (𝓝 (F c))
⊢ ContinuousWithinAt F {c}ᶜ c
[PROOFSTEP]
simpa [← smul_add, ContinuousWithinAt] using H.add H'
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[{c}ᶜ] c, DifferentiableAt ℂ f z
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
⊢ Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (limUnder (𝓝[{c}ᶜ] c) f))
[PROOFSTEP]
rw [eventually_nhdsWithin_iff] at hd 
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
⊢ Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (limUnder (𝓝[{c}ᶜ] c) f))
[PROOFSTEP]
have : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ { c }) := fun z hz =>
  (hz.1 hz.2).differentiableWithinAt
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})
⊢ Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (limUnder (𝓝[{c}ᶜ] c) f))
[PROOFSTEP]
have H := differentiableOn_update_limUnder_of_isLittleO hd this ho
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})
H : DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) {x | (fun x => x ∈ {c}ᶜ → DifferentiableAt ℂ f x) x}
⊢ Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (limUnder (𝓝[{c}ᶜ] c) f))
[PROOFSTEP]
exact continuousAt_update_same.1 (H.differentiableAt hd).continuousAt
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
⊢ ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = deriv f w₀
[PROOFSTEP]
have hf' : DifferentiableOn ℂ (dslope f w₀) U :=
  (differentiableOn_dslope (hU.mem_nhds ((ball_subset_closedBall.trans hc) hw₀))).mpr hf
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
⊢ ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = deriv f w₀
[PROOFSTEP]
have h0 := (hf'.diffContOnCl_ball hc).two_pi_i_inv_smul_circleIntegral_sub_inv_smul hw₀
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = deriv f w₀
[PROOFSTEP]
rw [← dslope_same, ← h0]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) =
    (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z
[PROOFSTEP]
congr 1
[GOAL]
case e_a
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z
[PROOFSTEP]
trans ∮ z in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)
[PROOFSTEP]
have h1 : ContinuousOn (fun z : ℂ => ((z - w₀) ^ 2)⁻¹) (sphere c R) :=
  by
  refine' ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => _
  exact sphere_disjoint_ball.ne_of_mem hw hw₀ (sub_eq_zero.mp (sq_eq_zero_iff.mp h))
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
[PROOFSTEP]
refine' ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => _
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
w : ℂ
hw : w ∈ sphere c R
h : (w - w₀) ^ 2 = 0
⊢ False
[PROOFSTEP]
exact sphere_disjoint_ball.ne_of_mem hw hw₀ (sub_eq_zero.mp (sq_eq_zero_iff.mp h))
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)
[PROOFSTEP]
have h2 : CircleIntegrable (fun z : ℂ => ((z - w₀) ^ 2)⁻¹ • f z) c R :=
  by
  refine' ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le _
  exact h1.smul (hf.continuousOn.mono (sphere_subset_closedBall.trans hc))
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
⊢ CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f z) c R
[PROOFSTEP]
refine' ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le _
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
⊢ ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹ • f z) (sphere c R)
[PROOFSTEP]
exact h1.smul (hf.continuousOn.mono (sphere_subset_closedBall.trans hc))
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
h2 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f z) c R
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)
[PROOFSTEP]
have h3 : CircleIntegrable (fun z : ℂ => ((z - w₀) ^ 2)⁻¹ • f w₀) c R :=
  ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le (h1.smul continuousOn_const)
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
h2 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f z) c R
h3 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f w₀) c R
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)
[PROOFSTEP]
have h4 : (∮ z : ℂ in C(c, R), ((z - w₀) ^ 2)⁻¹) = 0 := by
  simpa using circleIntegral.integral_sub_zpow_of_ne (by decide : (-2 : ℤ) ≠ -1) c w₀ R
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
h2 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f z) c R
h3 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f w₀) c R
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹) = 0
[PROOFSTEP]
simpa using circleIntegral.integral_sub_zpow_of_ne (by decide : (-2 : ℤ) ≠ -1) c w₀ R
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
h2 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f z) c R
h3 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f w₀) c R
⊢ -2 ≠ -1
[PROOFSTEP]
decide
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
h2 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f z) c R
h3 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f w₀) c R
h4 : (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹) = 0
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)
[PROOFSTEP]
simp only [smul_sub, circleIntegral.integral_sub h2 h3, h4, circleIntegral.integral_smul_const, zero_smul, sub_zero]
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)) = ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z
[PROOFSTEP]
refine' circleIntegral.integral_congr (pos_of_mem_ball hw₀).le fun z hz => _
[GOAL]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
z : ℂ
hz : z ∈ sphere c R
⊢ ((z - w₀) ^ 2)⁻¹ • (f z - f w₀) = (z - w₀)⁻¹ • dslope f w₀ z
[PROOFSTEP]
simp only [dslope_of_ne, Metric.sphere_disjoint_ball.ne_of_mem hz hw₀, slope, ← smul_assoc, sq, mul_inv, Ne.def,
  not_false_iff, vsub_eq_sub, Algebra.id.smul_eq_mul]
