awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
rcases :
  ∀ (u : Set β) (hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}) (u_open : IsOpen[inst_1] u) (xu : x ∈ u),
    ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r

Tactic:
rcases _root_.mem_nhds_iff.1 (inter_mem A B) with ⟨u, hu, u_open, xu⟩

Premises used: mem_nhds_iff, Filter.inter_mem, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}
u_open : IsOpen[inst_1] u
xu : x ∈ u
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r

Tactic:
⟨u, u_open, xu, fun y hy ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}
u_open : IsOpen[inst_1] u
xu : x ∈ u
refine : ∀ (y : β) (hy : y ∈ u), (f y, g y) ∈ r
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r

Tactic:
refine ⟨u, u_open, xu, fun y hy ↦ ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}
u_open : IsOpen[inst_1] u
xu : x ∈ u
y : β
hy : y ∈ u
⊢ (f y, f x) ∈ t

Tactic:
have I1 : (f y, f x) ∈ t := SetRel.symm t (hu hy).1
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}
u_open : IsOpen[inst_1] u
xu : x ∈ u
y : β
hy : y ∈ u
I1 : (f y, f x) ∈ t
⊢ (g x, g y) ∈ t

Tactic:
have I2 : (g x, g y) ∈ t := (hu hy).2
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}
u_open : IsOpen[inst_1] u
xu : x ∈ u
y : β
hy : y ∈ u
I1 : (f y, f x) ∈ t
I2 : (g x, g y) ∈ t
⊢ (f y, g x) ∈ t

Tactic:
rw [hfg hx] at I1
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}
u_open : IsOpen[inst_1] u
xu : x ∈ u
y : β
hy : y ∈ u
I1 : (f y, f x) ∈ t
I2 : (g x, g y) ∈ t
I1₁ : (f y, g x) ∈ t
⊢ (g x, g y) ∈ t

Tactic:
rw [hfg hx] at I1
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}
u_open : IsOpen[inst_1] u
xu : x ∈ u
y : β
hy : y ∈ u
I1 : (f y, g x) ∈ t
I2 : (g x, g y) ∈ t
⊢ (f y, g y) ∈ r

Tactic:
htr (SetRel.prodMk_mem_comp I1 I2)

Premises used: SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SetRel.IsSymm t
htr : t ○ t ⊆ r
A : {z : β | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z : β | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z : β | (f x, f z) ∈ t} ∩ {z : β | (g x, g z) ∈ t}
u_open : IsOpen[inst_1] u
xu : x ∈ u
y : β
hy : y ∈ u
I1 : (f y, g x) ∈ t
I2 : (g x, g y) ∈ t
⊢ (f y, g y) ∈ r

Tactic:
exact htr (SetRel.prodMk_mem_comp I1 I2)

Premises used: SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
⊢ ∀ x ∈ s, ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r

Tactic:
have A : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r := by
    intro x hx
    obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
    have A : {z | (f x, f z) ∈ t} ∈ 𝓝 x := (hf x hx).preimage_mem_nhds (mem_nhds_left (f x) ht)
    have B : {z | (g x, g z) ∈ t} ∈ 𝓝 x := (hg x hx).preimage_mem_nhds (mem_nhds_left (g x) ht)
    rcases _root_.mem_nhds_iff.1 (inter_mem A B) with ⟨u, hu, u_open, xu⟩
    refine ⟨u, u_open, xu, fun y hy ↦ ?_⟩
    have I1 : (f y, f x) ∈ t := SetRel.symm t (hu hy).1
    have I2 : (g x, g y) ∈ t := (hu hy).2
    rw [hfg hx] at I1
    exact htr (SetRel.prodMk_mem_comp I1 I2)
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
A : ∀ x ∈ s, ∃ (t : Set β), IsOpen[inst_1] t ∧ x ∈ t ∧ ∀ z ∈ t, (f z, g z) ∈ r
choose! :
  ∀ (t : (x : β) → Set β) (t_open : ∀ x ∈ s, IsOpen[inst_1] (t x)) (xt : ∀ x ∈ s, x ∈ t x)
    (ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r), ∃ (t : Set β), IsOpen[inst_1] t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r

Tactic:
choose! t t_open xt ht using A
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : (x : β) → Set β
t_open : ∀ x ∈ s, IsOpen[inst_1] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r

Tactic:
⟨⋃ x ∈ s, t x, isOpen_biUnion t_open, fun x hx ↦ mem_biUnion hx (xt x hx), ?_⟩

Premises used: Set.mem_biUnion, And.intro, Exists.intro, isOpen_biUnion, Set.iUnion
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : (x : β) → Set β
t_open : ∀ x ∈ s, IsOpen[inst_1] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
refine : ∀ (x : β), Membership.mem (γ := Set β) (⋃ x ∈ s, t x) x → (f x, g x) ∈ r
⊢ ∃ (t : Set β), IsOpen[inst_1] t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r

Tactic:
refine ⟨⋃ x ∈ s, t x, isOpen_biUnion t_open, fun x hx ↦ mem_biUnion hx (xt x hx), ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : (x : β) → Set β
t_open : ∀ x ∈ s, IsOpen[inst_1] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
x : β
hx : Membership.mem (γ := Set β) (⋃ x ∈ s, t x) x
⊢ ∃ i ∈ s, x ∈ t i

Tactic:
simp only [mem_iUnion, exists_prop] at hx

Premises used: Set.mem_iUnion, exists_prop
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : (x : β) → Set β
t_open : ∀ x ∈ s, IsOpen[inst_1] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
x : β
hx : ∃ i ∈ s, x ∈ t i
rcases : ∀ (y : β) (ys : y ∈ s) (hy : x ∈ t y), (f x, g x) ∈ r
⊢ (f x, g x) ∈ r

Tactic:
rcases hx with ⟨y, ys, hy⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : (x : β) → Set β
t_open : ∀ x ∈ s, IsOpen[inst_1] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
x y : β
ys : y ∈ s
hy : x ∈ t y
⊢ (f x, g x) ∈ r

Tactic:
ht y ys x hy
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : TopologicalSpace β
r : SetRel α α
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
t : (x : β) → Set β
t_open : ∀ x ∈ s, IsOpen[inst_1] (t x)
xt : ∀ x ∈ s, x ∈ t x
ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r
x y : β
ys : y ∈ s
hy : x ∈ t y
⊢ (f x, g x) ∈ r

Tactic:
exact ht y ys x hy
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
inst : UniformSpace β
f g : α → β
l : Filter α
b : β
hf : Tendsto f l (𝓝 b)
hg : Tendsto (fun (x : α) ↦ (f x, g x)) l (𝓤 β)
⊢ Tendsto g l (𝓝 b)

Tactic:
Uniform.tendsto_nhds_right.2 <| (Uniform.tendsto_nhds_right.1 hf).uniformity_trans hg

Premises used: Iff.mpr, Filter.Tendsto.uniformity_trans, Uniform.tendsto_nhds_right, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
inst : UniformSpace β
f g : α → β
l : Filter α
b : β
hfg : Tendsto (fun (x : α) ↦ (f x, g x)) l (𝓤 β)
⊢ Tendsto f l (𝓝 b) ↔ Tendsto g l (𝓝 b)

Tactic:
⟨fun h => h.congr_uniformity hfg, fun h => h.congr_uniformity hfg.uniformity_symm⟩

Premises used: Filter.Tendsto.congr_uniformity, Iff.intro, Filter.Tendsto.uniformity_symm
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
f : Filter α
⊢ (∀ (i' : ι), p i' → ∃ i ∈ f, id i ×ˢ id i ⊆ s i') ↔ ∀ (i : ι), p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i

Tactic:
simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, forall_mem_comm]

Premises used: Set.mem_prod_eq, Set.subset_def, and_imp, id, Prod.forall, forall_mem_comm
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
⊢ Cauchy f ↔ f.NeBot ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s

Tactic:
(𝓤 α).basis_sets.cauchy_iff

Premises used: Set.Mem, uniformity, Filter.basis_sets, Filter.HasBasis.cauchy_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
⊢ (f.NeBot ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s) ↔ f.NeBot ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s

Tactic:
simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, forall_mem_comm]

Premises used: Set.mem_prod_eq, Set.subset_def, and_imp, Prod.forall, forall_mem_comm
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
hl : l.NeBot
⊢ Cauchy l ↔ l ×ˢ l ≤ 𝓤 α

Tactic:
simp only [Cauchy, hl, true_and]

Premises used: Cauchy, true_and
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
⊢ l.NeBot

Tactic:
haveI := h.1
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
this : l.NeBot
⊢ (↑(Ultrafilter.of l) : Filter α) ≤ l

Tactic:
have := Ultrafilter.of_le l
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
this_1 : l.NeBot
this : (↑(Ultrafilter.of l) : Filter α) ≤ l
⊢ Cauchy (↑(Ultrafilter.of l) : Filter α)

Tactic:
⟨Ultrafilter.neBot _, (Filter.prod_mono this this).trans h.2⟩

Premises used: Cauchy, Filter.prod_mono, Ultrafilter.neBot, And.right, And.intro, LE.le.trans
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
this_1 : l.NeBot
this : (↑(Ultrafilter.of l) : Filter α) ≤ l
⊢ Cauchy (↑(Ultrafilter.of l) : Filter α)

Tactic:
exact ⟨Ultrafilter.neBot _, (Filter.prod_mono this this).trans h.2⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
rw : (map f l).NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
rw₁ : l.NeBot ∧ map f l ×ˢ map f l ≤ 𝓤 α ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
rw₂ :
  l.NeBot ∧ map (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) ≤ 𝓤 α ↔
    l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
rw₃ rw₄ :
  l.NeBot ∧ map (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) ≤ 𝓤 α ↔
    l.NeBot ∧ map (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) ≤ 𝓤 α
⊢ Cauchy (map f l) ↔ l.NeBot ∧ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)

Tactic:
rw [Cauchy, map_neBot_iff, prod_map_map_eq, Tendsto]

Premises used: Cauchy, Filter.Tendsto, Filter.prod_map_map_eq, Filter.map_neBot_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
hl : l.NeBot
f : β → α
⊢ Cauchy (map f l) ↔ Tendsto (fun (p : β × β) ↦ (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)

Tactic:
cauchy_map_iff.trans <| and_iff_right hl

Premises used: cauchy_map_iff, and_iff_right, Iff.trans
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f g : Filter α
hg : g.NeBot
h_c : Cauchy f
h_le : g ≤ f
⊢ Cauchy g

Tactic:
⟨hg, le_trans (Filter.prod_mono h_le h_le) h_c.right⟩

Premises used: Cauchy, Filter.prod_mono, And.right, And.intro, le_trans
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f g : Filter α
h_c : Cauchy f
h : g.NeBot
h_le : g ≤ f
⊢ Cauchy g

Tactic:
h_c.mono h_le

Premises used: Cauchy.mono
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
a : α
⊢ Cauchy (𝓝 a)

Tactic:
⟨nhds_neBot, nhds_prod_eq.symm.trans_le (nhds_le_uniformity a)⟩

Premises used: nhds_neBot, Cauchy, Eq.trans_le, nhds_le_uniformity, And.intro, nhds_prod_eq, Eq.symm
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
a : α
⊢ Cauchy (pure a)

Tactic:
cauchy_nhds.mono (pure_le_nhds a)

Premises used: pure_le_nhds, Cauchy.mono, cauchy_nhds
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
inst : l.NeBot
f : β → α
a : α
h : Tendsto f l (𝓝 a)
⊢ Cauchy (map f l)

Tactic:
cauchy_nhds.mono h

Premises used: Cauchy.mono, cauchy_nhds
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
β : Type v
u v : UniformSpace β
F : Filter β
huv : u ≤ v
hF : Cauchy F
⊢ Cauchy F

Tactic:
⟨hF.1, hF.2.trans huv⟩

Premises used: Cauchy, And.right, And.left, And.intro, LE.le.trans
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
β : Type v
u v : UniformSpace β
F : Filter β
rw : F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ⊓ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
rw₁ : F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
rw₂ rw₃ : (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
⊢ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β

Tactic:
rw [inf_uniformity (u := u), le_inf_iff, and_and_left]

Premises used: and_and_left, le_inf_iff, inf_uniformity
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
β : Type v
ι : Sort u_1
inst : Nonempty ι
u : ι → UniformSpace β
l : Filter β
rw : l.NeBot ∧ l ×ˢ l ≤ ⨅ (i : ι), 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
rw₁ : (l.NeBot ∧ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β) ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
rw₂ : (l.NeBot ∧ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β) ↔ (∀ (x : ι), l.NeBot) ∧ ∀ (x : ι), l ×ˢ l ≤ 𝓤 β
rw₃ rw₄ : (l.NeBot ∧ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β) ↔ l.NeBot ∧ ∀ (x : ι), l ×ˢ l ≤ 𝓤 β
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β

Tactic:
rw [iInf_uniformity, le_iInf_iff, forall_and, forall_const]

Premises used: le_iInf_iff, iInf_uniformity, forall_const, forall_and
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
β : Type v
ι : Sort u_1
u : ι → UniformSpace β
l : Filter β
inst : l.NeBot
simp_rw : l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β
simp_rw₁ : l ×ˢ l ≤ ⨅ (i : ι), 𝓤 β ↔ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy l

Tactic:
simp_rw [cauchy_iff_le (uniformSpace := _), iInf_uniformity, le_iInf_iff]

Premises used: le_iInf_iff, iInf_uniformity, cauchy_iff_le
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
β : Type v
u : UniformSpace β
α : Type u_1
f : α → β
l : Filter α
simp : l.NeBot ∧ l ×ˢ l ≤ 𝓤 α ↔ l.NeBot ∧ l ×ˢ l ≤ Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β)
⊢ Cauchy l ↔ Cauchy (map f l)

Tactic:
simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap]

Premises used: Cauchy, Filter.map_le_iff_le_comap, Filter.prod_map_map_eq, Filter.map_neBot_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
β : Type v
u : UniformSpace β
α : Type u_1
f : α → β
l : Filter α
⊢ l.NeBot ∧ l ×ˢ l ≤ 𝓤 α ↔ l.NeBot ∧ l ×ˢ l ≤ Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β)

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
F : Filter (α × β)
simp_rw : Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)
simp_rw₁ : Cauchy F ↔ Cauchy F ∧ Cauchy F
⊢ Cauchy F ↔ Cauchy (map Prod.fst F) ∧ Cauchy (map Prod.snd F)

Tactic:
simp_rw +instances [instUniformSpaceProd, ← cauchy_comap_uniformSpace, ← cauchy_inf_uniformSpace]

Premises used: instUniformSpaceProd, cauchy_inf_uniformSpace, cauchy_comap_uniformSpace
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
⊢ f.NeBot

Tactic:
have := hf.1
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this : f.NeBot
⊢ g.NeBot

Tactic:
have := hg.1
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this_1 : f.NeBot
this : g.NeBot
⊢ Cauchy (f ×ˢ g)

Tactic:
simpa [cauchy_prod_iff, hf.1] using ⟨hf, hg⟩

Premises used: cauchy_prod_iff, And.left
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
rcases : ∀ (U : Set (α × α)) (U_mem : U ∈ 𝓤 α) (hU : U ○ U ⊆ {p : α × α | p.1 = x → p.2 ∈ s}), s ∈ f
⊢ s ∈ f

Tactic:
rcases comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 hs) with ⟨U, U_mem, hU⟩

Premises used: mem_nhds_uniformity_iff_right, comp_mem_uniformity_sets, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p : α × α | p.1 = x → p.2 ∈ s}
rcases : ∀ (t : Set α) (t_mem : t ∈ f) (ht : t ×ˢ t ⊆ U) (y : α) (hxy : (x, y) ∈ U) (hy : y ∈ t), s ∈ f
⊢ s ∈ f

Tactic:
rcases adhs U U_mem with ⟨t, t_mem, ht, y, hxy, hy⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p : α × α | p.1 = x → p.2 ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
apply : t ⊆ s
⊢ s ∈ f

Tactic:
apply mem_of_superset t_mem

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p : α × α | p.1 = x → p.2 ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ t ⊆ s

Tactic:
fun z hz => hU (SetRel.prodMk_mem_comp hxy (ht <| mk_mem_prod hy hz)) rfl

Premises used: Set.Mem, Set.Subset, SetRel.prodMk_mem_comp, Set.mk_mem_prod, rfl
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p : α × α | p.1 = x → p.2 ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ t ⊆ s

Tactic:
exact fun z hz => hU (SetRel.prodMk_mem_comp hxy (ht <| mk_mem_prod hy hz)) rfl

Premises used: SetRel.prodMk_mem_comp, Set.mk_mem_prod, rfl
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s

Tactic:
(cauchy_iff.1 hf).2 s hs

Premises used: cauchy_iff, And.right, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
obtain : ∀ (t : Set α) (t_mem : t ∈ f) (ht : t ×ˢ t ⊆ s), ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t

Tactic:
obtain ⟨t, t_mem, ht⟩ : ∃ t ∈ f, t ×ˢ t ⊆ s := (cauchy_iff.1 hf).2 s hs

Premises used: cauchy_iff, And.right, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
right : ∃ (y : α), (x, y) ∈ s ∧ y ∈ t
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t

Tactic:
use t, t_mem, ht
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ (y : α), (x, y) ∈ s ∧ y ∈ t

Tactic:
forall_mem_nonempty_iff_neBot.2 adhs _ (inter_mem_inf (mem_nhds_left x hs) t_mem)

Premises used: Iff.mpr, Filter.inter_mem_inf, Set.Mem, Filter.forall_mem_nonempty_iff_neBot, mem_nhds_left, Set.Nonempty