-- Mathlib/Topology/UniformSpace/Dini.lean
/-- **Dini's theorem**: if `F n` is a monotone increasing collection of continuous functions
converging pointwise to a continuous function `f`, then `F n` converges locally uniformly to `f`. -/
lemma tendstoLocallyUniformly_of_forall_tendsto
    (hF_cont : ∀ i, Continuous (F i)) (hF_mono : Monotone F) (hf : Continuous f)
    (h_tendsto : ∀ x, Tendsto (F · x) atTop (𝓝 (f x))) :
    TendstoLocallyUniformly F f atTop

Proof state:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε

Tactic:
simp_rw +singlePass [tendsto_iff_norm_sub_tendsto_zero] at h_tendsto

Result:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
h_tendsto : ∀ (x : α), Tendsto (fun e => ‖F e x - f x‖) atTop (𝓝 0)
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε

Proof state:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
h_tendsto : ∀ (x : α), Tendsto (fun e => ‖F e x - f x‖) atTop (𝓝 0)
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε

Tactic:
obtain ⟨n, hn⟩ := (h_tendsto x).eventually (eventually_lt_nhds ε_pos) |>.exists

Result:
case intro
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
h_tendsto : ∀ (x : α), Tendsto (fun e => ‖F e x - f x‖) atTop (𝓝 0)
n : ι
hn : ‖F n x - f x‖ < ε
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε

Proof state:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
⊢ ∀ ε > 0, ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε

Tactic:
intro ε ε_pos x

Result:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε

Proof state:
case eq_bot
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
h : atTop = ⊥
⊢ TendstoLocallyUniformly F f atTop

ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
⊢ TendstoLocallyUniformly F f atTop

Tactic:
case eq_bot => simp [h, tendstoLocallyUniformly_iff_forall_tendsto]

Result:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
⊢ TendstoLocallyUniformly F f atTop

Proof state:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
⊢ TendstoLocallyUniformly F f atTop

Tactic:
simp_rw [Metric.tendstoLocallyUniformly_iff, dist_eq_norm']

Result:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
⊢ ∀ ε > 0, ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε

Proof state:
case intro
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
h_tendsto : ∀ (x : α), Tendsto (fun e => ‖F e x - f x‖) atTop (𝓝 0)
n : ι
hn : ‖F n x - f x‖ < ε
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε

Tactic:
refine ⟨{y | ‖F n y - f y‖ < ε}, ⟨isOpen_lt (by fun_prop) continuous_const |>.mem_nhds hn, ?_⟩⟩

Result:
case intro
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
x✝ : atTop.NeBot
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
h_tendsto : ∀ (x : α), Tendsto (fun e => ‖F e x - f x‖) atTop (𝓝 0)
n : ι
hn : ‖F n x - f x‖ < ε
⊢ ∀ᶠ (n_1 : ι) in atTop, ∀ y ∈ {y | ‖F n y - f y‖ < ε}, ‖F n_1 y - f y‖ < ε

Proof state:
case h
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
x : α
n m : ι
hnm : m ∈ Set.Ici n
⊢ F n x ≤ F m x

Tactic:
exact hF_mono hnm x

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
x : α
n : ι
⊢ ∀ᶠ (c : ι) in atTop, F n x ≤ F c x

Tactic:
filter_upwards [Ici_mem_atTop n] with m hnm

Result:
case h
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace α
inst✝ : NormedLatticeAddCommGroup G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous (F i)
hF_mono : Monotone F
hf : Continuous f
h_tendsto : ∀ (x : α), Tendsto (fun x_1 => F x_1 x) atTop (𝓝 (f x))
x✝ : atTop.NeBot
x : α
n m : ι
hnm : m ∈ Set.Ici n
⊢ F n x ≤ F m x