awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
U : ι → SetRel α α
h : (𝓤 α).HasBasis p U
s : Set α
x : α
⊢ Membership.mem (γ := Set α) (⋂ (i : ι), ⋂ (_ : p i), ⋃ x ∈ s, ball x (U i)) x ↔ x ∈ closure[inst.toTopologicalSpace] s

Tactic:
simp [mem_closure_iff_nhds_basis (nhds_basis_uniformity h), ball]

Premises used: UniformSpace.ball, nhds_basis_uniformity, mem_closure_iff_nhds_basis
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
⊢ UniformContinuous f ↔ ∀ r ∈ 𝓤 β, {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α

Tactic:
Iff.rfl

Premises used: UniformContinuous, Set.Mem, Iff.rfl, setOf, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
⊢ UniformContinuous f ↔ ∀ r ∈ 𝓤 β, ∀ᶠ (x : α × α) in 𝓤 α, (f x.1, f x.2) ∈ r

Tactic:
Iff.rfl

Premises used: UniformContinuous, Set.Mem, Filter.Eventually, Iff.rfl, setOf, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
rw :
  Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (SProd.sprod (α := Set α) (β := Set α) univ univ)) (𝓤 β) ↔
    UniformContinuous f
rw₁ :
  Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (SProd.sprod (α := Set α) (β := Set α) univ univ)) (𝓤 β) ↔
    Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
rw₂ :
  Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 univ) (𝓤 β) ↔
    Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
rw₃ :
  Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ ⊤) (𝓤 β) ↔ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
rw₄ rw₅ :
  Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
⊢ UniformContinuousOn f univ ↔ UniformContinuous f

Tactic:
rw [UniformContinuousOn, UniformContinuous, univ_prod_univ, principal_univ, inf_top_eq]

Premises used: UniformContinuous, inf_top_eq, Filter.principal_univ, Set.univ_prod_univ, UniformContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
c : α → β
h : ∀ (a b : α), c a = c b
this : Eq.{ua + 1} (α := Set (α × α)) (preimage.{ua, ub} (β := β × β) (fun (x : α × α) ↦ (c x.1, c x.2)) SetRel.id) univ
⊢ 𝓤 α ≤ comap.{ua, ub} (β := β × β) (fun (x : α × α) ↦ (c x.1, c x.2)) (𝓟 SetRel.id)

Tactic:
simp [comap_principal, this]

Premises used: Filter.comap_principal
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
⊢ UniformContinuous.{ua, ua} (α := α) id

Tactic:
tendsto_id

Premises used: UniformContinuous, Filter.tendsto_id
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
b : β
⊢ UniformContinuous.{ua, ub} (β := β) fun (x : α) ↦ b

Tactic:
uniformContinuous_of_const fun _ _ => rfl

Premises used: uniformContinuous_of_const, rfl
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
g : β → γ
f : α → β
hg : UniformContinuous g
hf : UniformContinuous f
⊢ UniformContinuous (g ∘ f)

Tactic:
hg.comp hf

Premises used: UniformContinuous, Filter.Tendsto.comp
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
inst : UniformSpace β
T : β → β
h : UniformContinuous T
⊢ UniformContinuous T^[0]

Tactic:
uniformContinuous_id

Premises used: uniformContinuous_id, Nat.iterate
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
inst : UniformSpace β
T : β → β
h : UniformContinuous T
⊢ UniformContinuous T^[0]

Tactic:
exact uniformContinuous_id

Premises used: uniformContinuous_id
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
inst : UniformSpace β
T : β → β
h : UniformContinuous T
n : ℕ
hn : UniformContinuous T^[n]
⊢ UniformContinuous T^[n + 1]

Tactic:
Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h

Premises used: Function.iterate_succ, Eq.rec, UniformContinuous.comp, Eq.symm
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
inst : UniformSpace β
T : β → β
h : UniformContinuous T
n : ℕ
hn : UniformContinuous T^[n]
⊢ UniformContinuous T^[n + 1]

Tactic:
exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
inst : UniformSpace β
T : β → β
n : ℕ
h : UniformContinuous T
zero : UniformContinuous T^[0]
succ : ∀ (n : ℕ) (hn : UniformContinuous T^[n]), UniformContinuous T^[n + 1]
⊢ UniformContinuous T^[n]

Tactic:
induction n with
  | zero => exact uniformContinuous_id
  | succ n hn => exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h

Premises used: uniformContinuous_id
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
ι' : Sort u_2
p : ι → Prop
s : ι → SetRel α α
ha : (𝓤 α).HasBasis p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : (𝓤 β).HasBasis q t
f : α → β
⊢ (∀ (ib : ι'), q ib → ∃ (ia : ι), p ia ∧ ∀ x ∈ s ia, (f x.1, f x.2) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ (j : ι), p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ t i

Tactic:
simp only [Prod.forall]

Premises used: Prod.forall
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
ι : Sort u_1
inst : UniformSpace α
inst_1 : UniformSpace β
ι' : Sort u_2
p : ι → Prop
s : ι → SetRel α α
ha : (𝓤 α).HasBasis p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : (𝓤 β).HasBasis q t
f : α → β
S : Set α
simp_rw :
  (∀ (ib : ι'), q ib → ∃ (ia : ι), p ia ∧ ∀ (a b : α), (a, b) ∈ s ia ∩ S ×ˢ S → (f a, f b) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ (j : ι), p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i
simp_rw₁ :
  (∀ (ib : ι'), q ib → ∃ (ia : ι), p ia ∧ ∀ (a b : α), (a, b) ∈ S ×ˢ S ∩ s ia → (f a, f b) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ (j : ι), p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i
simp_rw₂ :
  (∀ (ib : ι'), q ib → ∃ (ia : ι), p ia ∧ ∀ (a b : α), (a, b) ∈ S ×ˢ S ∩ s ia → (f a, f b) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ (j : ι), p j ∧ ∀ (a b : α), a ∈ S → b ∈ S → (a, b) ∈ s j → (f a, f b) ∈ t i
simp_rw₃ :
  (∀ (ib : ι'), q ib → ∃ (ia : ι), p ia ∧ ∀ (a b : α), (a, b) ∈ S ×ˢ S ∧ (a, b) ∈ s ia → (f a, f b) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ (j : ι), p j ∧ ∀ (a b : α), a ∈ S → b ∈ S → (a, b) ∈ s j → (f a, f b) ∈ t i
simp_rw₄ :
  (∀ (ib : ι'), q ib → ∃ (ia : ι), p ia ∧ ∀ (a b : α), (a ∈ S ∧ b ∈ S) ∧ (a, b) ∈ s ia → (f a, f b) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ (j : ι), p j ∧ ∀ (a b : α), a ∈ S → b ∈ S → (a, b) ∈ s j → (f a, f b) ∈ t i
⊢ (∀ (ib : ι'), q ib → ∃ (ia : ι), p ia ∧ ∀ x ∈ s ia ∩ S ×ˢ S, (f x.1, f x.2) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ (j : ι), p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i

Tactic:
simp_rw [Prod.forall, Set.inter_comm (s _), forall_mem_comm, mem_inter_iff, mem_prod, and_imp]

Premises used: and_imp, Set.mem_inter_iff, Set.inter_comm, Set.mem_prod, Prod.forall, forall_mem_comm
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformEmbedding f
⊢ IsUniformInducing f

Tactic:
hf.toIsUniformInducing

Premises used: IsUniformEmbedding.toIsUniformInducing
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoLocallyUniformly F f atTop

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

Premises used: Filter.atTop, Filter.eq_or_neBot, Or.elim
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
refine : ∀ (h : Eq.{u_1 + 1} (α := Filter ι) atTop ⊥), TendstoLocallyUniformly F f atTop
refine₁ : NeBot.{u_1} (α := ι) atTop → TendstoLocallyUniformly F f atTop
⊢ TendstoLocallyUniformly F f atTop

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

Premises used: Filter.atTop, Filter.eq_or_neBot, Or.elim
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
h : Eq.{u_1 + 1} (α := Filter ι) atTop ⊥
⊢ TendstoLocallyUniformly F f atTop

Tactic:
simp [h, tendstoLocallyUniformly_iff_forall_tendsto]

Premises used: tendstoLocallyUniformly_iff_forall_tendsto
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
h : Eq.{u_1 + 1} (α := Filter ι) atTop ⊥
⊢ TendstoLocallyUniformly F f atTop

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

Premises used: tendstoLocallyUniformly_iff_forall_tendsto
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
h : NeBot.{u_1} (α := ι) atTop
x : α
n : ι
⊢ F n x ≤ f x

Tactic:
ge_of_tendsto (h_tendsto x) ?_

Premises used: ge_of_tendsto
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
h : NeBot.{u_1} (α := ι) atTop
x : α
n : ι
refine : ∀ᶠ (c : ι) in atTop, F n x ≤ F c x
⊢ F n x ≤ f x

Tactic:
refine ge_of_tendsto (h_tendsto x) ?_

Premises used: ge_of_tendsto
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
h_1 : NeBot.{u_1} (α := ι) atTop
x : α
n : ι
h : ∀ (m : ι) (hnm : m ∈ Set.Ici n), F n x ≤ F m x
⊢ ∀ᶠ (c : ι) in atTop, F n x ≤ F c x

Tactic:
filter_upwards [Ici_mem_atTop n] with m hnm

Premises used: Filter.Ici_mem_atTop
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
h : NeBot.{u_1} (α := ι) atTop
x : α
n m : ι
hnm : m ∈ Set.Ici n
⊢ F n x ≤ F m x

Tactic:
hF_mono hnm x
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
h : NeBot.{u_1} (α := ι) atTop
x : α
n m : ι
hnm : m ∈ Set.Ici n
⊢ F n x ≤ F m x

Tactic:
exact hF_mono hnm x
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
h : NeBot.{u_1} (α := ι) atTop
⊢ ∀ (x : α) (n : ι), F n x ≤ f x

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
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
h : NeBot.{u_1} (α := ι) atTop
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
simp_rw : ∀ ε > 0, ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε
⊢ TendstoLocallyUniformly F f atTop

Tactic:
simp_rw [Metric.tendstoLocallyUniformly_iff, dist_eq_norm']

Premises used: dist_eq_norm', Metric.tendstoLocallyUniformly_iff
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_tendsto : ∀ (x : α), Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
h : NeBot.{u_1} (α := ι) atTop
F_le_f : ∀ (x : α) (n : ι), F n x ≤ f x
ε : ℝ
ε_pos : ε > 0
x : α
⊢ ∀ (x : α), Tendsto (β := ℝ) (fun (e : ι) ↦ ‖F e x - f x‖) atTop (𝓝 0)

Tactic:
simp_rw +singlePass [tendsto_iff_norm_sub_tendsto_zero] at h_tendsto

Premises used: tendsto_iff_norm_sub_tendsto_zero
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : NeBot.{u_1} (α := ι) atTop
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)
obtain : ∀ (n : ι) (hn : ‖F n x - f x‖ < ε), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε
⊢ ∃ 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

Premises used: eventually_lt_nhds, Filter.Eventually.exists, Filter.Tendsto.eventually
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : NeBot.{u_1} (α := ι) atTop
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[inst_1, _] fun (y : α) ↦ ‖F n y - f y‖

Tactic:
fun_prop
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : NeBot.{u_1} (α := ι) atTop
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‖ < ε
refine :
  ∀ᶠ (n_1 : ι) in atTop, ∀ (y : α), Membership.mem (γ := Set α) {y : α | ‖F n y - f y‖ < ε} y → ‖F n_1 y - f y‖ < ε
⊢ ∃ 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, ?_⟩⟩
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_1 : NeBot.{u_1} (α := ι) atTop
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‖ < ε
h : ∀ (m : ι) (hnm : n ≤ m) (z : α) (hz : ‖F n z - f z‖ < ε), ‖F m z - f z‖ < ε
⊢ ∀ᶠ (n_1 : ι) in atTop, ∀ (y : α), Membership.mem (γ := Set α) {y : α | ‖F n y - f y‖ < ε} y → ‖F n_1 y - f y‖ < ε

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

Premises used: Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : NeBot.{u_1} (α := ι) atTop
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:
norm_le_norm_of_abs_le_abs ?_ |>.trans_lt hz

Premises used: norm_le_norm_of_abs_le_abs, LE.le.trans_lt
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_1 : NeBot.{u_1} (α := ι) atTop
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‖ < ε
h : |F m z - f z| ≤ |F n z - f z|
⊢ ‖F m z - f z‖ < ε

Tactic:
refine norm_le_norm_of_abs_le_abs ?_ |>.trans_lt hz

Premises used: norm_le_norm_of_abs_le_abs, LE.le.trans_lt
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h_1 : NeBot.{u_1} (α := ι) atTop
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‖ < ε
h : F n z ≤ F m 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]

Premises used: neg_sub, sub_le_sub_iff_left, abs_of_nonpos, sub_nonpos_of_le
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : NeBot.{u_1} (α := ι) atTop
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:
hF_mono hnm z
-- Module: Mathlib.Topology.UniformSpace.Dini
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : NormedAddCommGroup G
inst_3 : Lattice G
inst_4 : HasSolidNorm G
inst_5 : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
hF_cont : ∀ (i : ι), Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (F i)
hF_mono : Monotone F
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : NeBot.{u_1} (α := ι) atTop
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