awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
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)) (𝓤 α) (𝓤 β)
⊢ UniformContinuousOn f univ ↔ UniformContinuous f
have rw₃ : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ ⊤) (𝓤 β) ↔ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Tactic: rw [UniformContinuousOn, UniformContinuous, univ_prod_univ, principal_univ, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
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)) (𝓤 α) (𝓤 β)
⊢ UniformContinuousOn f univ ↔ UniformContinuous f
have rw₄ : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Tactic: rw [UniformContinuousOn, UniformContinuous, univ_prod_univ, principal_univ, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
β : Type ub
inst : UniformSpace β
T : β → β
n : ℕ
h : UniformContinuous T
⊢ UniformContinuous T^[n]
have zero : UniformContinuous T^[0]
Tactic: induction n with
  | zero => exact uniformContinuous_id
  | succ n hn => exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
β : Type ub
inst : UniformSpace β
T : β → β
n : ℕ
h : UniformContinuous T
zero : UniformContinuous T^[0]
⊢ UniformContinuous T^[n]
have succ : ∀ (n : ℕ) (hn : UniformContinuous T^[n]), UniformContinuous T^[n + 1]
Tactic: induction n with
  | zero => exact uniformContinuous_id
  | succ n hn => exact Function.iterate_succ _ _ ▸ UniformContinuous.comp hn h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
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 α
⊢ (∀ (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
have 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
Tactic: simp_rw [Prod.forall, Set.inter_comm (s _), forall_mem_comm, mem_inter_iff, mem_prod, and_imp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
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
⊢ (∀ (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
have 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
Tactic: simp_rw [Prod.forall, Set.inter_comm (s _), forall_mem_comm, mem_inter_iff, mem_prod, and_imp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
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
⊢ (∀ (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
have 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
Tactic: simp_rw [Prod.forall, Set.inter_comm (s _), forall_mem_comm, mem_inter_iff, mem_prod, and_imp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
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
⊢ (∀ (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
have 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
Tactic: simp_rw [Prod.forall, Set.inter_comm (s _), forall_mem_comm, mem_inter_iff, mem_prod, and_imp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
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
⊢ (∀ (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
have 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
Tactic: simp_rw [Prod.forall, Set.inter_comm (s _), forall_mem_comm, mem_inter_iff, mem_prod, and_imp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (goal)
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
have refine : ∀ (h : Eq.{u_1 + 1} (α := Filter ι) atTop ⊥), TendstoLocallyUniformly F f atTop
Tactic: refine (atTop : Filter ι).eq_or_neBot.elim (fun h ↦ ?eq_bot) (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (goal)
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
⊢ TendstoLocallyUniformly F f atTop
have refine₁ : NeBot.{u_1} (α := ι) atTop → TendstoLocallyUniformly F f atTop
Tactic: refine (atTop : Filter ι).eq_or_neBot.elim (fun h ↦ ?eq_bot) (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (goal)
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
have refine : ∀ᶠ (c : ι) in atTop, F n x ≤ F c x
Tactic: refine ge_of_tendsto (h_tendsto x) ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (goal)
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 : ι
⊢ ∀ᶠ (c : ι) in atTop, F n x ≤ F c x
have h : ∀ (m : ι) (hnm : m ∈ Set.Ici n), F n x ≤ F m x
Tactic: filter_upwards [Ici_mem_atTop n] with m hnm
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (hypothesis)
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
⊢ TendstoLocallyUniformly F f atTop
have F_le_f : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (goal)
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
⊢ TendstoLocallyUniformly F f atTop
have simp_rw : ∀ ε > 0, ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε
Tactic: simp_rw [Metric.tendstoLocallyUniformly_iff, dist_eq_norm']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (hypothesis)
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 : α
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε
have h_tendsto₁ : ∀ (x : α), Tendsto (β := ℝ) (fun (e : ι) ↦ ‖F e x - f x‖) atTop (𝓝 0)
Tactic: simp_rw +singlePass [tendsto_iff_norm_sub_tendsto_zero] at h_tendsto
Cleared hypotheses: h_tendsto
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (goal)
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)
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε
have obtain : ∀ (n : ι) (hn : ‖F n x - f x‖ < ε), ∃ 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
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (goal)
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‖ < ε
⊢ ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in atTop, ∀ y ∈ t, ‖F n y - f y‖ < ε
have refine : ∀ᶠ (n_1 : ι) in atTop, ∀ (y : α), Membership.mem (γ := Set α) {y : α | ‖F n y - f y‖ < ε} y → ‖F n_1 y - f y‖ < ε
Tactic: refine ⟨{y | ‖F n y - f y‖ < ε}, ⟨isOpen_lt (by fun_prop) continuous_const |>.mem_nhds hn, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (goal)
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‖ < ε
⊢ ∀ᶠ (n_1 : ι) in atTop, ∀ (y : α), Membership.mem (γ := Set α) {y : α | ‖F n y - f y‖ < ε} y → ‖F n_1 y - f y‖ < ε
have h : ∀ (m : ι) (hnm : n ≤ m) (z : α) (hz : ‖F n z - f z‖ < ε), ‖F m z - f z‖ < ε
Tactic: filter_upwards [eventually_ge_atTop n] with m hnm z hz
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (goal)
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‖ < ε
have h : |F m z - f z| ≤ |F n z - f z|
Tactic: refine norm_le_norm_of_abs_le_abs ?_ |>.trans_lt hz
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (goal)
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| ≤ |F n z - f z|
have h : F n z ≤ F m z
Tactic: simp only [abs_of_nonpos (sub_nonpos_of_le (F_le_f _ _)), neg_sub, sub_le_sub_iff_left]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Dini (goal)
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
s : Set α
hF_cont : ∀ (i : ι), ContinuousOn (F i) s
hF_mono : ∀ x ∈ s, Monotone.{u_1, u_3} (β := G) fun (x_1 : ι) ↦ F x_1 x
hf : ContinuousOn f s
h_tendsto : ∀ x ∈ s, Tendsto (fun (x_1 : ι) ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoLocallyUniformlyOn F f atTop s
have rw : TendstoLocallyUniformly (fun (i : ι) (x : (↑s : Type u_2)) ↦ F i (↑x : α)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s))
  atTop
Tactic: rw [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
⊢ DiscreteUniformity X ↔ uniformity X = 𝓟 SetRel.id
have rw : inst = ⊥ ↔ uniformity X = 𝓟 SetRel.id
Tactic: rw [discreteUniformity_iff_eq_bot, UniformSpace.ext_iff, Filter.ext_iff, bot_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
rw : inst = ⊥ ↔ uniformity X = 𝓟 SetRel.id
⊢ DiscreteUniformity X ↔ uniformity X = 𝓟 SetRel.id
have rw₁ : (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ uniformity X) ↔ uniformity X = 𝓟 SetRel.id
Tactic: rw [discreteUniformity_iff_eq_bot, UniformSpace.ext_iff, Filter.ext_iff, bot_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
rw : inst = ⊥ ↔ uniformity X = 𝓟 SetRel.id
rw₁ : (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ uniformity X) ↔ uniformity X = 𝓟 SetRel.id
⊢ DiscreteUniformity X ↔ uniformity X = 𝓟 SetRel.id
have rw₂ : (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ uniformity X) ↔
  ∀ (s : Set (X × X)), s ∈ uniformity X ↔ Membership.mem (γ := Filter (X × X)) (𝓟 SetRel.id) s
Tactic: rw [discreteUniformity_iff_eq_bot, UniformSpace.ext_iff, Filter.ext_iff, bot_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
rw : inst = ⊥ ↔ uniformity X = 𝓟 SetRel.id
rw₁ : (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ uniformity X) ↔ uniformity X = 𝓟 SetRel.id
rw₂ :
  (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ uniformity X) ↔
    ∀ (s : Set (X × X)), s ∈ uniformity X ↔ Membership.mem (γ := Filter (X × X)) (𝓟 SetRel.id) s
⊢ DiscreteUniformity X ↔ uniformity X = 𝓟 SetRel.id
have rw₃ : (∀ (s : Set (X × X)), s ∈ uniformity X ↔ Membership.mem (γ := Filter (X × X)) (𝓟 SetRel.id) s) ↔
  ∀ (s : Set (X × X)), s ∈ uniformity X ↔ Membership.mem (γ := Filter (X × X)) (𝓟 SetRel.id) s
Tactic: rw [discreteUniformity_iff_eq_bot, UniformSpace.ext_iff, Filter.ext_iff, bot_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
⊢ Eq.{u_1 + 1} (α := TopologicalSpace X) toTopologicalSpace ⊥
have rw : Eq.{u_1 + 1} (α := TopologicalSpace X) toTopologicalSpace ⊥
Tactic: rw [DiscreteUniformity.eq_bot (X := X), UniformSpace.toTopologicalSpace_bot]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
rw : Eq.{u_1 + 1} (α := TopologicalSpace X) toTopologicalSpace ⊥
⊢ Eq.{u_1 + 1} (α := TopologicalSpace X) toTopologicalSpace ⊥
have rw₁ : Eq.{u_1 + 1} (α := TopologicalSpace X) ⊥ ⊥
Tactic: rw [DiscreteUniformity.eq_bot (X := X), UniformSpace.toTopologicalSpace_bot]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
⊢ DiscreteUniformity X ↔ SetRel.id ∈ uniformity X
have rw : DiscreteUniformity X ↔ inst = ⊥
Tactic: rw [← uniformSpace_eq_bot, discreteUniformity_iff_eq_bot]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_2
inst : UniformSpace X
rw : DiscreteUniformity X ↔ inst = ⊥
⊢ DiscreteUniformity X ↔ SetRel.id ∈ uniformity X
have rw₁ : inst = ⊥ ↔ inst = ⊥
Tactic: rw [← uniformSpace_eq_bot, discreteUniformity_iff_eq_bot]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (goal)
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
⊢ Eq.{u_2 + 1} (α := SetRel Y Y) SetRel.id (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1})
have h : ∀ (x : Y × Y),
  Membership.mem (γ := Set (Y × Y)) SetRel.id x ↔
    Membership.mem (γ := Set (Y × Y)) (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.DiscreteUniformity (hypothesis)
Goal:
X : Type u_1
u : UniformSpace X
inst : DiscreteUniformity X
Y : Type u_2
inst_1 : Finite Y
inst_2 : UniformSpace Y
inst_3 : DiscreteTopology Y
⊢ DiscreteUniformity Y
have h : Eq.{u_2 + 1} (α := SetRel Y Y) SetRel.id (⋂ (y : Y), {p : Y × Y | p.2 = y → Membership.mem (γ := Set Y) {y} p.1})
Tactic: have h : SetRel.id = ⋂ y : Y, {p | p.2 = y → p.1 ∈ ({y} : Set Y)} := by
    ext x
    simp [SetRel.id]