Theorem: hurwitz2_1 (RMT4/hurwitz.lean)

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0
Tactic:
by_cases h : K = ∅
State after:
case pos
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h : K = ∅
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0

case neg
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h : ¬K = ∅
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h : K = ∅
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0
Tactic:
case pos => simp [h]
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h : ¬K = ∅
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0
Tactic:
case neg =>
  obtain ⟨z₀, h1, h2⟩ : ∃ z₀ ∈ K, ∀ z ∈ K, ‖f z₀‖ ≤ ‖f z‖ :=
    hK.exists_forall_le (nonempty_iff_ne_empty.2 h) (continuous_norm.comp_continuousOn hf1)
  have h3 := tendstoUniformlyOn_iff.1 F_conv (‖f z₀‖) (norm_pos_iff.2 (hf2 _ h1))
  filter_upwards [h3] with n hn z hz h
  specialize hn z hz
  specialize h2 z hz
  simp [h] at hn h2
  linarith
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h : K = ∅
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0
Tactic:
simp [h]
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h : ¬K = ∅
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0
Tactic:
obtain ⟨z₀, h1, h2⟩ : ∃ z₀ ∈ K, ∀ z ∈ K, ‖f z₀‖ ≤ ‖f z‖ :=
  hK.exists_forall_le (nonempty_iff_ne_empty.2 h) (continuous_norm.comp_continuousOn hf1)
State after:
case intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h2 : ∀ z ∈ K, ‖f z₀‖ ≤ ‖f z‖
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0

State before:
case intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h2 : ∀ z ∈ K, ‖f z₀‖ ≤ ‖f z‖
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0
Tactic:
have h3 := tendstoUniformlyOn_iff.1 F_conv (‖f z₀‖) (norm_pos_iff.2 (hf2 _ h1))
State after:
case intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h2 : ∀ z ∈ K, ‖f z₀‖ ≤ ‖f z‖
h3 : ∀ᶠ (n : ι) in p, ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0

State before:
case intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h2 : ∀ z ∈ K, ‖f z₀‖ ≤ ‖f z‖
h3 : ∀ᶠ (n : ι) in p, ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0
Tactic:
filter_upwards [h3] with n hn z hz h
State after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h✝ : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h2 : ∀ z ∈ K, ‖f z₀‖ ≤ ‖f z‖
h3 : ∀ᶠ (n : ι) in p, ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
n : ι
hn : ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
z : ℂ
hz : z ∈ K
h : F n z = 0
⊢ False

State before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h✝ : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h2 : ∀ z ∈ K, ‖f z₀‖ ≤ ‖f z‖
h3 : ∀ᶠ (n : ι) in p, ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
n : ι
hn : ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
z : ℂ
hz : z ∈ K
h : F n z = 0
⊢ False
Tactic:
specialize hn z hz
State after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h✝ : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h2 : ∀ z ∈ K, ‖f z₀‖ ≤ ‖f z‖
h3 : ∀ᶠ (n : ι) in p, ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
n : ι
z : ℂ
hz : z ∈ K
h : F n z = 0
hn : dist (f z) (F n z) < ‖f z₀‖
⊢ False

State before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h✝ : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h2 : ∀ z ∈ K, ‖f z₀‖ ≤ ‖f z‖
h3 : ∀ᶠ (n : ι) in p, ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
n : ι
z : ℂ
hz : z ∈ K
h : F n z = 0
hn : dist (f z) (F n z) < ‖f z₀‖
⊢ False
Tactic:
specialize h2 z hz
State after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h✝ : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h3 : ∀ᶠ (n : ι) in p, ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
n : ι
z : ℂ
hz : z ∈ K
h : F n z = 0
hn : dist (f z) (F n z) < ‖f z₀‖
h2 : ‖f z₀‖ ≤ ‖f z‖
⊢ False

State before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h✝ : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h3 : ∀ᶠ (n : ι) in p, ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
n : ι
z : ℂ
hz : z ∈ K
h : F n z = 0
hn : dist (f z) (F n z) < ‖f z₀‖
h2 : ‖f z₀‖ ≤ ‖f z‖
⊢ False
Tactic:
simp [h] at hn h2
State after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h✝ : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h3 : ∀ᶠ (n : ι) in p, ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
n : ι
z : ℂ
hz : z ∈ K
h : F n z = 0
h2 : Complex.abs (f z₀) ≤ Complex.abs (f z)
hn : Complex.abs (f z) < Complex.abs (f z₀)
⊢ False

State before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h✝ : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h3 : ∀ᶠ (n : ι) in p, ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
n : ι
z : ℂ
hz : z ∈ K
h : F n z = 0
h2 : Complex.abs (f z₀) ≤ Complex.abs (f z)
hn : Complex.abs (f z) < Complex.abs (f z₀)
⊢ False
Tactic:
linarith
State after:
no goals