internlm/Lean-Github huggingface dataset:
Theorem: TendstoUniformlyOn.mul_of_compact
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : ¬K = ∅
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
case neg =>
  replace h : K.Nonempty := Set.nonempty_iff_ne_empty.2 h
  have h2 : ContinuousOn (norm ∘ f) K := continuous_norm.comp_continuousOn hf
  have h3 : ContinuousOn (norm ∘ g) K := continuous_norm.comp_continuousOn hg
  obtain ⟨xf, _, h4⟩ : ∃ x ∈ K, ∀ y ∈ K, ‖f y‖ ≤ ‖f x‖ := hK.exists_forall_ge h h2
  obtain ⟨xg, _, h5⟩ : ∃ x ∈ K, ∀ y ∈ K, ‖g y‖ ≤ ‖g x‖ := hK.exists_forall_ge h h3
  exact hF.mul_of_bound hG h4 h5
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_compact
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : K = ∅
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
simpa only [h] using tendstoUniformlyOn_empty
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_compact
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : ¬K = ∅
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
replace h : K.Nonempty := Set.nonempty_iff_ne_empty.2 h
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Theorem: TendstoUniformlyOn.mul_of_compact
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
have h2 : ContinuousOn (norm ∘ f) K := continuous_norm.comp_continuousOn hf
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Theorem: TendstoUniformlyOn.mul_of_compact
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
have h3 : ContinuousOn (norm ∘ g) K := continuous_norm.comp_continuousOn hg
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
h3 : ContinuousOn (norm ∘ g) K
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Theorem: TendstoUniformlyOn.mul_of_compact
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
h3 : ContinuousOn (norm ∘ g) K
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
obtain ⟨xf, _, h4⟩ : ∃ x ∈ K, ∀ y ∈ K, ‖f y‖ ≤ ‖f x‖ := hK.exists_forall_ge h h2
Proof state after:
case intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
h3 : ContinuousOn (norm ∘ g) K
xf : α
left✝ : xf ∈ K
h4 : ∀ y ∈ K, ‖f y‖ ≤ ‖f xf‖
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Theorem: TendstoUniformlyOn.mul_of_compact
Proof state before:
case intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
h3 : ContinuousOn (norm ∘ g) K
xf : α
left✝ : xf ∈ K
h4 : ∀ y ∈ K, ‖f y‖ ≤ ‖f xf‖
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
obtain ⟨xg, _, h5⟩ : ∃ x ∈ K, ∀ y ∈ K, ‖g y‖ ≤ ‖g x‖ := hK.exists_forall_ge h h3
Proof state after:
case intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
h3 : ContinuousOn (norm ∘ g) K
xf : α
left✝¹ : xf ∈ K
h4 : ∀ y ∈ K, ‖f y‖ ≤ ‖f xf‖
xg : α
left✝ : xg ∈ K
h5 : ∀ y ∈ K, ‖g y‖ ≤ ‖g xg‖
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Theorem: TendstoUniformlyOn.mul_of_compact
Proof state before:
case intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hK : IsCompact K
h : Set.Nonempty K
h2 : ContinuousOn (norm ∘ f) K
h3 : ContinuousOn (norm ∘ g) K
xf : α
left✝¹ : xf ∈ K
h4 : ∀ y ∈ K, ‖f y‖ ≤ ‖f xf‖
xg : α
left✝ : xg ∈ K
h5 : ∀ y ∈ K, ‖g y‖ ≤ ‖g xg‖
⊢ TendstoUniformlyOn (F * G) (f * g) p K
Tactic:
exact hF.mul_of_bound hG h4 h5
Proof state after:
no goals
Theorem: TendstoUniformlyOn.div_of_compact
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hgK : ∀ z ∈ K, g z ≠ 0
hK : IsCompact K
⊢ TendstoUniformlyOn (F / G) (f / g) p K
Tactic:
simpa [div_eq_mul_inv] using hF.mul_of_compact (hG.inv_of_compact hg hK hgK) hf (hg.inv₀ hgK) hK
Proof state after:
no goals
Theorem: Filter.Eventually.exists'
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
P : ℝ → Prop
t₀ : ℝ
h : ∀ᶠ (t : ℝ) in 𝓝[>] t₀, P t
⊢ ∃ t > t₀, P t
Tactic:
simpa [and_comm, exists_prop] using (frequently_nhdsWithin_iff.mp h.frequently).exists
Proof state after:
no goals
Theorem: order_eq_zero_iff
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
Tactic:
rw [hp.locally_zero_iff]
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
Theorem: order_eq_zero_iff
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
Tactic:
by_cases h : p = 0
Proof state after:
case pos
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0

case neg
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
Theorem: order_eq_zero_iff
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
Tactic:
case pos => simp [h]
Proof state after:
no goals
Theorem: order_eq_zero_iff
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
Tactic:
case neg =>
  simp [FormalMultilinearSeries.order_eq_zero_iff h, h]
  ext1
  rw [hp.coeff_zero, hz₀]; rfl
Proof state after:
no goals
Theorem: order_eq_zero_iff
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
Tactic:
simp [h]
Proof state after:
no goals
Theorem: order_eq_zero_iff
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
Tactic:
simp [FormalMultilinearSeries.order_eq_zero_iff h, h]
Proof state after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
⊢ p 0 = 0
Theorem: order_eq_zero_iff
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
⊢ p 0 = 0
Tactic:
ext1
Proof state after:
case H
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
x✝ : Fin 0 → ℂ
⊢ (p 0) x✝ = 0 x✝
Theorem: order_eq_zero_iff
Proof state before:
case H
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
x✝ : Fin 0 → ℂ
⊢ (p 0) x✝ = 0 x✝
Tactic:
rw [hp.coeff_zero, hz₀]
Proof state after:
case H
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
x✝ : Fin 0 → ℂ
⊢ 0 = 0 x✝
Theorem: order_eq_zero_iff
Proof state before:
case H
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
x✝ : Fin 0 → ℂ
⊢ 0 = 0 x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: order_pos_iff
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
⊢ 0 < FormalMultilinearSeries.order p ↔ ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ 0
Tactic:
simp [pos_iff_ne_zero, (order_eq_zero_iff hp hz₀).not]
Proof state after:
no goals
Theorem: cindex_pos
Proof state before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
h1 : AnalyticAt ℂ f z₀
h2 : f z₀ = 0
h3 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f ≠ 0
Tactic:
obtain ⟨p, hp⟩ := h1
Proof state after:
case intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
h2 : f z₀ = 0
h3 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f ≠ 0
Theorem: cindex_pos
Proof state before:
case intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
h2 : f z₀ = 0
h3 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f ≠ 0
Tactic:
filter_upwards [cindex_eventually_eq_order hp] with r h4
Proof state after:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r✝ : ℝ
U : Set ℂ
h2 : f z₀ = 0
h3 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
r : ℝ
h4 : cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
⊢ cindex z₀ r f ≠ 0
Theorem: cindex_pos
Proof state before:
case h
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r✝ : ℝ
U : Set ℂ
h2 : f z₀ = 0
h3 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
r : ℝ
h4 : cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
⊢ cindex z₀ r f ≠ 0
Tactic:
simpa [h4, order_eq_zero_iff hp h2] using h3.frequently.filter_mono nhdsWithin_le_nhds
Proof state after:
no goals
Theorem: hurwitz2_1
Proof 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 = ∅
Proof 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
Theorem: hurwitz2_1
Proof 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]
Proof state after:
no goals
Theorem: hurwitz2_1
Proof 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
Proof state after:
no goals
Theorem: hurwitz2_1
Proof 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]
Proof state after:
no goals
Theorem: hurwitz2_1
Proof 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)
Proof 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
Theorem: hurwitz2_1
Proof 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))
Proof 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
Theorem: hurwitz2_1
Proof 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
Proof 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
Theorem: hurwitz2_1
Proof 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
Proof 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
Theorem: hurwitz2_1
Proof 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
Proof 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
Theorem: hurwitz2_1
Proof 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
Proof 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
Theorem: hurwitz2_1
Proof 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
Proof state after:
no goals
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof 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
Proof 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))
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof 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]
Proof state after:
no goals
Theorem: TendstoUniformlyOn.tendsto_circle_integral
Proof 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
Proof state after:
no goals