Theorem: Cauchy_formula (Colloquia/ConversationWithLean/Colloquium.lean)

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * I) • f c
Tactic:
let y := f c
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * I) • f c

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * I) • f c
Tactic:
have hy : Tendsto f (𝓝 c) (𝓝 y) := by
  rw [← (@nhdsWithin_eq_nhds _ _ c (closedBall c R)).mpr (closedBall_mem_nhds _ h0)]
  exact ContinuousOn.continuousWithinAt hf <| mem_closedBall_self (le_of_lt h0)
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * I) • f c

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = (2 * ↑π * I) • f c
Tactic:
rw [← sub_eq_zero, ← norm_le_zero_iff]
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ 0

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ 0
Tactic:
refine' le_of_forall_le_of_dense fun ε ε0 => _
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
obtain ⟨α, α0, hα⟩ := (nhds_basis_ball.tendsto_iff (nhds_basis_ball)).1 hy _
  (div_pos ε0 Real.two_pi_pos)
State after:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε

State before:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
set δ := α/2
State after:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε

State before:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
have δ0 := half_pos α0
State after:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε

State before:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
have hδ := fun z hz => hα z ((@closedBall_subset_ball ℂ _ c (α/2) α (by linarith)) hz)
State after:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε

State before:
case intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
obtain ⟨r, hr0, hrδ, hrR⟩ : ∃ r, 0 < r ∧ r ≤ δ ∧ r ≤ R :=
  ⟨min δ R, lt_min δ0 h0, min_le_left _ _, min_le_right _ _⟩
State after:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε

State before:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
have hsub : closedBall c R \ ball c r ⊆ closedBall c R :=  diff_subset (closedBall c R) (ball c r)
State after:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε

State before:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
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)
State after:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε

State before:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε
Tactic:
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
State after:
case intro.intro.intro.intro.intro
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * ↑π * I) • f c‖ ≤ ε

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
⊢ Tendsto f (𝓝 c) (𝓝 y)
Tactic:
rw [← (@nhdsWithin_eq_nhds _ _ c (closedBall c R)).mpr (closedBall_mem_nhds _ h0)]
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
⊢ Tendsto f (𝓝[closedBall c R] c) (𝓝 y)

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
⊢ Tendsto f (𝓝[closedBall c R] c) (𝓝 y)
Tactic:
exact ContinuousOn.continuousWithinAt hf <| mem_closedBall_self (le_of_lt h0)
State after:
no goals

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
z : ℂ
hz : z ∈ closedBall c (α / 2)
⊢ α / 2 < α
Tactic:
linarith
State after:
no goals

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ 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‖
Tactic:
congr 2
State after:
case e_a.e_a
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ 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
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ (2 * ↑π * I) • y = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y

State before:
case e_a.e_a
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z
Tactic:
refine circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable hr0
  hrR countable_empty  (hf.mono hsub) fun z hz => hdiff z ?_
State after:
case e_a.e_a
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ (ball c R \ closedBall c r) \ ∅
⊢ z ∈ ball c R

State before:
case e_a.e_a
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ (ball c R \ closedBall c r) \ ∅
⊢ z ∈ ball c R
Tactic:
apply mem_of_subset_of_mem _ hz
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ (ball c R \ closedBall c r) \ ∅
⊢ (ball c R \ closedBall c r) \ ∅ ⊆ ball c R

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ (ball c R \ closedBall c r) \ ∅
⊢ (ball c R \ closedBall c r) \ ∅ ⊆ ball c R
Tactic:
rw [diff_empty]
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ (ball c R \ closedBall c r) \ ∅
⊢ ball c R \ closedBall c r ⊆ ball c R

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ (ball c R \ closedBall c r) \ ∅
⊢ ball c R \ closedBall c r ⊆ ball c R
Tactic:
exact diff_subset (ball c R) (closedBall c r)
State after:
no goals

State before:
case e_a.e_a
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ (2 * ↑π * I) • y = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y
Tactic:
simp only [circleIntegral.integral_smul_const, ne_eq, hr0.ne', not_false_eq_true,
  circleIntegral.integral_sub_center_inv]
State after:
no goals

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ 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)‖
Tactic:
simp only [smul_sub]
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f c‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • f c‖

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f c‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • f c‖
Tactic:
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
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ 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)⁻¹ • f c‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • f c‖

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ 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)⁻¹ • f c‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • f c‖
Tactic:
rw [circleIntegral.integral_sub] <;> refine' (hc'.smul _).circleIntegrable hr0.le
State after:
case hf
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ 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
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun x => f c) (sphere c r)

State before:
case hf
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun x => f x) (sphere c r)
Tactic:
exact hf.mono <| (sphere_subset_closedBall).trans (closedBall_subset_closedBall hrR)
State after:
no goals

State before:
case hg
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z => (z - c)⁻¹) (sphere c r)
⊢ ContinuousOn (fun x => f c) (sphere c r)
Tactic:
exact continuousOn_const
State after:
no goals

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • (f z - y)‖ ≤ 2 * π * r * (r⁻¹ * (ε / (2 * π)))
Tactic:
refine' circleIntegral.norm_integral_le_of_norm_le_const hr0.le fun z hz => _
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ sphere c r
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
z : ℂ
hz : z ∈ sphere c r
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
Tactic:
specialize hzne z hz
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
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 * π))

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
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 * π))
Tactic:
rw [mem_sphere, dist_eq_norm] at hz
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
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 * π))

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
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 * π))
Tactic:
rw [norm_smul, norm_inv, hz, ← dist_eq_norm]
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
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 * π))

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
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 * π))
Tactic:
refine' mul_le_mul_of_nonneg_left (le_of_lt <| hδ _ _) (inv_nonneg.2 hr0.le)
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ z ∈ closedBall c (α / 2)

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ z ∈ closedBall c (α / 2)
Tactic:
rwa [mem_closedBall_iff_norm, hz]
State after:
no goals

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ 2 * π * r * (r⁻¹ * (ε / (2 * π))) = ε
Tactic:
field_simp [hr0.ne', Real.two_pi_pos.ne']
State after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ 2 * π * r * ε = ε * (r * (2 * π))

State before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ 2 * π * r * ε = ε * (r * (2 * π))
Tactic:
ac_rfl
State after:
no goals