E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ 0
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * I) • y
rw [← sub_eq_zero, ← norm_le_zero_iff]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ 0
refine' le_of_forall_le_of_dense fun ε ε0 => _
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
⊢ ∃ δ, δ > 0 ∧ ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)

case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
obtain ⟨δ, δ0, hδ⟩ : ∃ δ > (0 : ℝ), ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
⊢ ∃ δ, δ > 0 ∧ ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)

case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
exact ((nhdsWithin_hasBasis nhds_basis_closedBall _).tendsto_iff nhds_basis_ball).1 hy _
  (div_pos ε0 Real.two_pi_pos)
case intro.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
obtain ⟨r, hr0, hrδ, hrR⟩ : ∃ r, 0 < r ∧ r ≤ δ ∧ r ≤ R :=
  ⟨min δ R, lt_min δ0 h0, min_le_left _ _, min_le_right _ _⟩
case intro.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
case intro.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
have hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c} :=
  diff_subset_diff_right (singleton_subset_iff.2 <| mem_ball_self hr0)
case intro.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
case intro.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
have hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c} :=
  diff_subset_diff_right (singleton_subset_iff.2 <| mem_closedBall_self hr0.le)
case intro.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
case intro.intro.intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ ≤ ε
have hzne : ∀ z ∈ sphere c r, z ≠ c := fun z hz =>
  ne_of_mem_of_not_mem hz fun h => hr0.ne' <| dist_self c ▸ Eq.symm h
case e_a.e_a
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z

case e_a.e_a
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ (2 * ↑π * I) • y = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • y‖ =
    ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y‖
congr 2
no goals
case e_a.e_a
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z
exact circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable hr0
  hrR hs (hc.mono hsub) fun z hz => hd z ⟨hsub' hz.1, hz.2⟩
no goals
case e_a.e_a
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ (2 * ↑π * I) • y = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y
simp [hr0.ne']
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • y‖
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • (f z - y)‖
simp only [smul_sub]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • y‖
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • y‖
have hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r) :=
  (continuousOn_id.sub continuousOn_const).inv₀ fun z hz => sub_ne_zero.2 <| hzne _ hz
case hf
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun x => f x) (sphere c r)

case hg
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun x => y) (sphere c r)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • y‖
rw [circleIntegral.integral_sub] <;> refine' (hc'.smul _).circleIntegrable hr0.le
no goals
case hf
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun x => f x) (sphere c r)
exact hc.mono <| subset_inter
  (sphere_subset_closedBall.trans <| closedBall_subset_closedBall hrR) hzne
no goals
case hg
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun x => y) (sphere c r)
exact continuousOn_const
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
z : ℂ
hz : z ∈ sphere c r
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • (f z - y)‖ ≤ 2 * π * r * (r⁻¹ * (ε / (2 * π)))
refine' circleIntegral.norm_integral_le_of_norm_le_const hr0.le fun z hz => _
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : z ∈ sphere c r
hzne : z ≠ c
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
z : ℂ
hz : z ∈ sphere c r
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
specialize hzne z hz
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : z ∈ sphere c r
hzne : z ≠ c
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
rw [mem_sphere, dist_eq_norm] at hz
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ r⁻¹ * dist (f z) y ≤ r⁻¹ * (ε / (2 * π))
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
rw [norm_smul, norm_inv, hz, ← dist_eq_norm]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ z ∈ closedBall c δ
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ r⁻¹ * dist (f z) y ≤ r⁻¹ * (ε / (2 * π))
refine' mul_le_mul_of_nonneg_left (hδ _ ⟨_, hzne⟩).le (inv_nonneg.2 hr0.le)
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ z ∈ closedBall c δ
rwa [mem_closedBall_iff_norm, hz]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ 2 * π * r * ε = ε * (r * (2 * π))
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ 2 * π * r * (r⁻¹ * (ε / (2 * π))) = ε
field_simp [hr0.ne', Real.two_pi_pos.ne']
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ (z : ℂ), z ∈ (ball c R \ {c}) \ s → DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ (z : ℂ), z ∈ closedBall c δ \ {c} → dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ (z : ℂ), z ∈ sphere c r → z ≠ c
⊢ 2 * π * r * ε = ε * (r * (2 * π))
ac_rfl