Theorem: hurwitz2_2 (RMT4/hurwitz.lean)

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
by_cases h : NeBot p
State after:
case pos
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

case neg
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : ¬NeBot p
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : ¬NeBot p
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
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 ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : ¬NeBot p
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
simp at h
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : p = ⊥
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : p = ⊥
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
simp [h]
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H1 : IsCompact (sphere z₀ r) := isCompact_sphere z₀ r
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H2 : TendstoUniformlyOn F f p (sphere z₀ r) :=
  (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).1 hf _ hr2 H1
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H3 : DifferentiableOn ℂ f U := hf.differentiableOn hF hU
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H4 : ContinuousOn f (sphere z₀ r) := H3.continuousOn.mono hr2
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H5 : ∀ᶠ n in p, ContinuousOn (F n) (sphere z₀ r) := by
  filter_upwards [hF] with n h using h.continuousOn.mono hr2
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H6 : ∀ᶠ n in p, ContinuousOn (deriv (F n)) (sphere z₀ r) := by
  filter_upwards [hF] with n h using (h.deriv hU).continuousOn.mono hr2
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r) :=
  (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).1 (hf.deriv hF hU) _ hr2 H1
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
have H8 : ContinuousOn (deriv f) (sphere z₀ r) :=
  (H3.deriv hU).continuousOn.mono hr2
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
H8 : ContinuousOn (deriv f) (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
H8 : ContinuousOn (deriv f) (sphere z₀ r)
⊢ Tendsto (cindex z₀ r ∘ F) p (𝓝 (cindex z₀ r f))
Tactic:
refine Tendsto.const_mul _ (TendstoUniformlyOn.tendsto_circle_integral hr1 ?_ ?_)
State after:
case refine_1
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
H8 : ContinuousOn (deriv f) (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ContinuousOn (fun z => deriv (F n) z / F n z) (sphere z₀ r)

case refine_2
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
H8 : ContinuousOn (deriv f) (sphere z₀ r)
⊢ TendstoUniformlyOn (fun k z => deriv (F k) z / F k z) (fun z => deriv f z / f z) p (sphere z₀ r)

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
Tactic:
filter_upwards [hF] with n h using h.continuousOn.mono hr2
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
Tactic:
filter_upwards [hF] with n h using (h.deriv hU).continuousOn.mono hr2
State after:
no goals

State before:
case refine_1
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
H8 : ContinuousOn (deriv f) (sphere z₀ r)
⊢ ∀ᶠ (n : ι) in p, ContinuousOn (fun z => deriv (F n) z / F n z) (sphere z₀ r)
Tactic:
filter_upwards [hurwitz2_1 H1 H2 H4 hf1, H6, H5] with n hn H6 H5 using ContinuousOn.div H6 H5 hn
State after:
no goals

State before:
case refine_2
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
hU : IsOpen U
hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U
hf : TendstoLocallyUniformlyOn F f p U
hr1 : 0 < r
hr2 : sphere z₀ r ⊆ U
hf1 : ∀ z ∈ sphere z₀ r, f z ≠ 0
h : NeBot p
H1 : IsCompact (sphere z₀ r)
H2 : TendstoUniformlyOn F f p (sphere z₀ r)
H3 : DifferentiableOn ℂ f U
H4 : ContinuousOn f (sphere z₀ r)
H5 : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (sphere z₀ r)
H6 : ∀ᶠ (n : ι) in p, ContinuousOn (deriv (F n)) (sphere z₀ r)
H7 : TendstoUniformlyOn (deriv ∘ F) (deriv f) p (sphere z₀ r)
H8 : ContinuousOn (deriv f) (sphere z₀ r)
⊢ TendstoUniformlyOn (fun k z => deriv (F k) z / F k z) (fun z => deriv f z / f z) p (sphere z₀ r)
Tactic:
exact TendstoUniformlyOn.div_of_compact H7 H2 H8 H4 hf1 H1
State after:
no goals