-- 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))
⊢ TendstoLocallyUniformly F f atTop

Tactic:
refine (atTop : Filter ι).eq_or_neBot.elim (fun h ↦ ?eq_bot) (fun _ ↦ ?_)

Result:
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

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
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‖ < ε
m : ι
hnm : n ≤ m
z : α
hz : ‖F n z - f z‖ < ε
⊢ |F m z - f z| ≤ |F n z - f z|

Tactic:
simp only [abs_of_nonpos (sub_nonpos_of_le (F_le_f _ _)), neg_sub, sub_le_sub_iff_left]

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
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‖ < ε
m : ι
hnm : n ≤ m
z : α
hz : ‖F n z - f z‖ < ε
⊢ F n z ≤ F m z

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‖ < ε
⊢ ∀ᶠ (n_1 : ι) in atTop, ∀ y ∈ {y | ‖F n y - f y‖ < ε}, ‖F n_1 y - f y‖ < ε

Tactic:
filter_upwards [eventually_ge_atTop n] with m hnm z hz

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
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‖ < ε
m : ι
hnm : n ≤ m
z : α
hz : ‖F n z - f z‖ < ε
⊢ ‖F m z - f z‖ < ε

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 : ι
⊢ F n x ≤ f x

Tactic:
refine ge_of_tendsto (h_tendsto 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
x : α
n : ι
⊢ ∀ᶠ (c : ι) in atTop, F n x ≤ F c x

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
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‖ < ε
m : ι
hnm : n ≤ m
z : α
hz : ‖F n z - f z‖ < ε
⊢ F n z ≤ F m z

Tactic:
exact hF_mono hnm z

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
⊢ TendstoLocallyUniformly F f atTop

Tactic:
have F_le_f (x : α) (n : ι) : F n x ≤ f x := by
  refine ge_of_tendsto (h_tendsto x) ?_
  filter_upwards [Ici_mem_atTop n] with m hnm
  exact hF_mono hnm 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
⊢ TendstoLocallyUniformly F f atTop

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
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‖ < ε
m : ι
hnm : n ≤ m
z : α
hz : ‖F n z - f z‖ < ε
⊢ ‖F m z - f z‖ < ε

Tactic:
refine norm_le_norm_of_abs_le_abs ?_ |>.trans_lt hz

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
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‖ < ε
m : ι
hnm : n ≤ m
z : α
hz : ‖F n z - f z‖ < ε
⊢ |F m z - f z| ≤ |F n z - f z|

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))
h : atTop = ⊥
⊢ TendstoLocallyUniformly F f atTop

Tactic:
simp [h, tendstoLocallyUniformly_iff_forall_tendsto]

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
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‖ < ε
⊢ Continuous fun y => ‖F n y - f y‖

Tactic:
fun_prop

Result:
no goals