Theorem: TendstoUniformlyOn.tendsto_circle_integral (RMT4/hurwitz.lean)

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Tactic:
by_cases h : NeBot p
State after:
case pos
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))

case neg
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : ¬NeBot p
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : ¬NeBot p
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Tactic:
case neg => simp at h; simp [h]
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Tactic:
case pos =>
  have f_cont : ContinuousOn f (sphere z₀ r) := F_conv.continuousOn F_cont
  rw [Metric.tendsto_nhds]
  intro ε hε
  have twopir_ne_zero : 2 * Real.pi * r ≠ 0 := by simp [Real.pi_ne_zero, hr.ne.symm]
  have : (2 * Real.pi * r)⁻¹ * ε > 0 :=
    mul_pos (inv_pos.mpr (mul_pos (mul_pos two_pos Real.pi_pos) hr)) hε.lt
  filter_upwards [tendstoUniformlyOn_iff.mp F_conv ((2 * Real.pi * r)⁻¹ * ε) this, F_cont] with n h h'
  simp_rw [dist_comm (f _) _, Complex.dist_eq, ← Complex.norm_eq_abs] at h
  rw [Complex.dist_eq, ← circleIntegral.integral_sub (h'.circleIntegrable hr.le) (f_cont.circleIntegrable hr.le),
    ← Complex.norm_eq_abs]
  have : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε := by
    have : z₀ + r ∈ sphere z₀ r := by simp [hr.le, Real.norm_eq_abs]
    exact ⟨z₀ + r, this, h _ this⟩
  convert circleIntegral.norm_integral_lt_of_norm_le_const_of_lt hr (h'.sub f_cont) (λ z hz => (h z hz).le) this
  field_simp [hr.ne, Real.pi_ne_zero, two_ne_zero]; ring
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : ¬NeBot p
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Tactic:
simp at h
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : p = ⊥
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : p = ⊥
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Tactic:
simp [h]
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Tactic:
have f_cont : ContinuousOn f (sphere z₀ r) := F_conv.continuousOn F_cont
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
⊢ Tendsto (fun i => ∮ (z : ℂ) in C(z₀, r), F i z) p (𝓝 (∮ (z : ℂ) in C(z₀, r), f z))
Tactic:
rw [Metric.tendsto_nhds]
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
⊢ ∀ ε > 0, ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
⊢ ∀ ε > 0, ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Tactic:
intro ε hε
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Tactic:
have twopir_ne_zero : 2 * Real.pi * r ≠ 0 := by simp [Real.pi_ne_zero, hr.ne.symm]
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Tactic:
have : (2 * Real.pi * r)⁻¹ * ε > 0 :=
  mul_pos (inv_pos.mpr (mul_pos (mul_pos two_pos Real.pi_pos) hr)) hε.lt
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
⊢ ∀ᶠ (x : ι) in p, dist (∮ (z : ℂ) in C(z₀, r), F x z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Tactic:
filter_upwards [tendstoUniformlyOn_iff.mp F_conv ((2 * Real.pi * r)⁻¹ * ε) this, F_cont] with n h h'
State after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h : ∀ x ∈ sphere z₀ r, dist (f x) (F n x) < (2 * Real.pi * r)⁻¹ * ε
h' : ContinuousOn (F n) (sphere z₀ r)
⊢ dist (∮ (z : ℂ) in C(z₀, r), F n z) (∮ (z : ℂ) in C(z₀, r), f z) < ε

State before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h : ∀ x ∈ sphere z₀ r, dist (f x) (F n x) < (2 * Real.pi * r)⁻¹ * ε
h' : ContinuousOn (F n) (sphere z₀ r)
⊢ dist (∮ (z : ℂ) in C(z₀, r), F n z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Tactic:
simp_rw [dist_comm (f _) _, Complex.dist_eq, ← Complex.norm_eq_abs] at h
State after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ dist (∮ (z : ℂ) in C(z₀, r), F n z) (∮ (z : ℂ) in C(z₀, r), f z) < ε

State before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ dist (∮ (z : ℂ) in C(z₀, r), F n z) (∮ (z : ℂ) in C(z₀, r), f z) < ε
Tactic:
rw [Complex.dist_eq, ← circleIntegral.integral_sub (h'.circleIntegrable hr.le) (f_cont.circleIntegrable hr.le),
  ← Complex.norm_eq_abs]
State after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ‖∮ (z : ℂ) in C(z₀, r), F n z - f z‖ < ε

State before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ‖∮ (z : ℂ) in C(z₀, r), F n z - f z‖ < ε
Tactic:
have : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε := by
  have : z₀ + r ∈ sphere z₀ r := by simp [hr.le, Real.norm_eq_abs]
  exact ⟨z₀ + r, this, h _ this⟩
State after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ‖∮ (z : ℂ) in C(z₀, r), F n z - f z‖ < ε

State before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ‖∮ (z : ℂ) in C(z₀, r), F n z - f z‖ < ε
Tactic:
convert circleIntegral.norm_integral_lt_of_norm_le_const_of_lt hr (h'.sub f_cont) (λ z hz => (h z hz).le) this
State after:
case h.e'_4
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ε = 2 * Real.pi * r * ((2 * Real.pi * r)⁻¹ * ε)

State before:
case h.e'_4
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ε = 2 * Real.pi * r * ((2 * Real.pi * r)⁻¹ * ε)
Tactic:
field_simp [hr.ne, Real.pi_ne_zero, two_ne_zero]
State after:
case h.e'_4
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ε * (2 * Real.pi * r) = 2 * Real.pi * r * ε

State before:
case h.e'_4
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ε * (2 * Real.pi * r) = 2 * Real.pi * r * ε
Tactic:
ring
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
⊢ 2 * Real.pi * r ≠ 0
Tactic:
simp [Real.pi_ne_zero, hr.ne.symm]
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
Tactic:
have : z₀ + r ∈ sphere z₀ r := by simp [hr.le, Real.norm_eq_abs]
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : z₀ + ↑r ∈ sphere z₀ r
⊢ ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this✝ : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
this : z₀ + ↑r ∈ sphere z₀ r
⊢ ∃ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
Tactic:
exact ⟨z₀ + r, this, h _ this⟩
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hr : 0 < r
F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
F_conv : TendstoUniformlyOn F f p (sphere z₀ r)
h✝ : NeBot p
f_cont : ContinuousOn f (sphere z₀ r)
ε : ℝ
hε : ε > 0
twopir_ne_zero : 2 * Real.pi * r ≠ 0
this : (2 * Real.pi * r)⁻¹ * ε > 0
n : ι
h' : ContinuousOn (F n) (sphere z₀ r)
h : ∀ x ∈ sphere z₀ r, ‖F n x - f x‖ < (2 * Real.pi * r)⁻¹ * ε
⊢ z₀ + ↑r ∈ sphere z₀ r
Tactic:
simp [hr.le, Real.norm_eq_abs]
State after:
no goals