awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β → γ
h : ∀ (a : α) (c : β) (b : α) (d : β), Inseparable a b → Inseparable c d → f a c = f b d
⊢ UniformContinuous (uncurry (lift₂ f h)) ↔ UniformContinuous (uncurry f)

Tactic:
uniformContinuous_dom₂

Premises used: SeparationQuotient.uniformContinuous_dom₂, SeparationQuotient.lift₂, Quotient, SeparationQuotient, Quotient.liftOn₂'
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
⊢ Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (𝓤 (SeparationQuotient α)) = 𝓤 α

Tactic:
comap_map_mk_uniformity

Premises used: Filter.map, uniformity, SeparationQuotient.comap_map_mk_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
h : UniformContinuous f
a : α
rw : (if hc : UniformContinuous f then lift f ⋯ else fun (x : SeparationQuotient α) ↦ f ⋯.some) (mk a) = f a
rw₁ : lift f ⋯ (mk a) = f a
rw₂ rw₃ : f a = f a
⊢ lift' f (mk a) = f a

Tactic:
rw [lift', dif_pos h, lift_mk]

Premises used: dif_pos, SeparationQuotient.lift_mk, SeparationQuotient.lift'
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
pos : ∀ (hf : UniformContinuous f), UniformContinuous (α := SeparationQuotient α) (lift' f)
neg : ∀ (hf : ¬UniformContinuous f), UniformContinuous (α := SeparationQuotient α) (lift' f)
⊢ UniformContinuous (α := SeparationQuotient α) (lift' f)

Tactic:
by_cases hf : UniformContinuous f

Premises used: UniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
hf : UniformContinuous f
pos :
  UniformContinuous.{u, v} (α := SeparationQuotient α) (β := β)
    (if hc : UniformContinuous f then lift f ⋯ else fun (x : SeparationQuotient α) ↦ f ⋯.some)
pos₁ : UniformContinuous (lift f ⋯)
pos₂ pos₃ pos₄ pos₅ : UniformContinuous f
⊢ UniformContinuous (α := SeparationQuotient α) (lift' f)

Tactic:
rwa [lift', dif_pos hf, uniformContinuous_lift]

Premises used: SeparationQuotient.uniformContinuous_lift, dif_pos, SeparationQuotient.lift'
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
hf : ¬UniformContinuous f
neg : UniformContinuous.{u, v} (β := β) fun (x : SeparationQuotient α) ↦ f ⋯.some
⊢ UniformContinuous (α := SeparationQuotient α) (lift' f)

Tactic:
rw [lift', dif_neg hf]

Premises used: dif_neg, SeparationQuotient.lift'
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous.{u, v} (β := β) fun (x : SeparationQuotient α) ↦ f ⋯.some

Tactic:
uniformContinuous_of_const fun a _ => rfl

Premises used: uniformContinuous_of_const, rfl
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous.{u, v} (β := β) fun (x : SeparationQuotient α) ↦ f ⋯.some

Tactic:
exact uniformContinuous_of_const fun a _ => rfl

Premises used: uniformContinuous_of_const
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
h : UniformContinuous f
a : α
rw : Eq (α := SeparationQuotient β) ((mk ∘ f) a) (mk (f a))
⊢ Eq (α := SeparationQuotient β) (map f (mk a)) (mk (f a))

Tactic:
rw [map, lift'_mk (uniformContinuous_mk.comp h)]

Premises used: SeparationQuotient.uniformContinuous_mk, SeparationQuotient.map, UniformContinuous.comp, SeparationQuotient.lift'_mk
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ Eq (α := SeparationQuotient β) ((mk ∘ f) a) (mk (f a))

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
⊢ UniformContinuous (α := SeparationQuotient α) (β := SeparationQuotient β) (map f)

Tactic:
uniformContinuous_lift' _

Premises used: SeparationQuotient.map, SeparationQuotient.uniformContinuous_lift'
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : mk ∘ f = g ∘ mk
h :
  ∀ (x : SeparationQuotient α) (a : α),
    map f (Quot.mk (⇑(inseparableSetoid α) : α → α → Prop) a) = g (Quot.mk (⇑(inseparableSetoid α) : α → α → Prop) a)
⊢ map f = g

Tactic:
ext ⟨a⟩
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : mk ∘ f = g ∘ mk
x : SeparationQuotient α
a : α
⊢ map f ⟦a⟧ = ⟦f a⟧

Tactic:
map_mk hf a

Premises used: SeparationQuotient.mk, SeparationQuotient.map_mk
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : mk ∘ f = g ∘ mk
x : SeparationQuotient α
a : α
⊢ ⟦f a⟧ = g ⟦a⟧

Tactic:
congr_fun comm a

Premises used: SeparationQuotient, SeparationQuotient.mk, congr_fun
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : mk ∘ f = g ∘ mk
x : SeparationQuotient α
a : α
⊢ map f (Quot.mk (⇑(inseparableSetoid α) : α → α → Prop) a) = g (Quot.mk (⇑(inseparableSetoid α) : α → α → Prop) a)

Tactic:
calc
    map f ⟦a⟧ = ⟦f a⟧ := map_mk hf a
    _ = g ⟦a⟧ := congr_fun comm a

Premises used: SeparationQuotient.map, Quotient.mk, congr_fun, SeparationQuotient.map_mk
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
⊢ Eq.{u + 1} (α := SeparationQuotient α → SeparationQuotient α) (map id) id

Tactic:
map_unique uniformContinuous_id rfl

Premises used: uniformContinuous_id, SeparationQuotient.map_unique, rfl
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
⊢ Eq (α := α → SeparationQuotient γ) (mk ∘ g ∘ f)
    (comp (β := SeparationQuotient α) (comp (β := SeparationQuotient β) (map g) (map f)) mk)

Tactic:
simp only [Function.comp_def, map_mk, hf, hg]

Premises used: Function.comp_def, SeparationQuotient.map_mk
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u_1
u : UniformSpace α
h : 𝓤 α = ⊤
⊢ IndiscreteTopology α

Tactic:
⟨(UniformSpace.ext h.symm : ⊤ = u) ▸ rfl⟩

Premises used: IndiscreteTopology.mk, Eq.rec, UniformSpace.ext, Eq.symm, rfl
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u_1
u : UniformSpace α
inst : IndiscreteTopology α
⊢ u = ⊤

Tactic:
UniformSpace.ext ?_

Premises used: UniformSpace.ext
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u_1
u : UniformSpace α
inst : IndiscreteTopology α
refine : 𝓤 α = 𝓤 α
⊢ u = ⊤

Tactic:
refine UniformSpace.ext ?_

Premises used: UniformSpace.ext
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u_1
u : UniformSpace α
inst : IndiscreteTopology α
rw : (𝓤 α).ker = univ
⊢ 𝓤 α = 𝓤 α

Tactic:
rw [top_uniformity, ← Filter.ker_eq_univ]

Premises used: Filter.ker_eq_univ, top_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u_1
u : UniformSpace α
inst : IndiscreteTopology α
h : ∀ (x : α × α), x ∈ (𝓤 α).ker ↔ Membership.mem (γ := Set (α × α)) univ x
⊢ (𝓤 α).ker = univ

Tactic:
ext x
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u_1
u : UniformSpace α
inst : IndiscreteTopology α
x : α × α
h : Inseparable x.1 x.2 ↔ Membership.mem (γ := Set (α × α)) univ x
⊢ x ∈ (𝓤 α).ker ↔ Membership.mem (γ := Set (α × α)) univ x

Tactic:
rw [← inseparable_iff_ker_uniformity]

Premises used: inseparable_iff_ker_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u_1
u : UniformSpace α
inst : IndiscreteTopology α
x : α × α
⊢ Inseparable x.1 x.2 ↔ Membership.mem (γ := Set (α × α)) univ x

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u_1
u : UniformSpace α
⊢ u = ⊤ ↔ IndiscreteTopology α

Tactic:
⟨fun h ↦ IndiscreteTopology.mk <| h ▸ UniformSpace.toTopologicalSpace_top (α := α),
  fun _ ↦ eq_top_uniformSpace⟩

Premises used: IndiscreteTopology.mk, UniformSpace.toTopologicalSpace_top, Eq.rec, IndiscreteTopology.eq_top_uniformSpace, Iff.intro, Eq.symm
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
β : Type v
inst : UniformSpace β
α : Type u_1
u : UniformSpace α
inst_1 : IndiscreteTopology β
f : α → β
rw : Tendsto.{u_1, v} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) ⊤
⊢ UniformContinuous f

Tactic:
rw [UniformContinuous, eq_top_uniformSpace (α := β), top_uniformity]

Premises used: UniformContinuous, IndiscreteTopology.eq_top_uniformSpace, top_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
β : Type v
inst : UniformSpace β
α : Type u_1
u : UniformSpace α
inst_1 : IndiscreteTopology β
f : α → β
⊢ Tendsto.{u_1, v} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) ⊤

Tactic:
Filter.tendsto_top

Premises used: Filter.tendsto_top
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
β : Type v
inst : UniformSpace β
α : Type u_1
u : UniformSpace α
inst_1 : IndiscreteTopology β
f : α → β
⊢ Tendsto.{u_1, v} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) ⊤

Tactic:
exact Filter.tendsto_top

Premises used: Filter.tendsto_top
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
s : SetRel X X
t u v : Set X
inst : s.IsTrans
htu : t ×ˢ u ⊆ s
huv : u ×ˢ v ⊆ s
hu : u.Nonempty
a b : X
hab : (a, b) ∈ t ×ˢ v
⊢ a ∈ t ∧ b ∈ v

Tactic:
simp only [mem_prod] at hab

Premises used: Set.mem_prod
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
s : SetRel X X
t u v : Set X
inst : s.IsTrans
htu : t ×ˢ u ⊆ s
huv : u ×ˢ v ⊆ s
hu : u.Nonempty
a b : X
hab : a ∈ t ∧ b ∈ v
obtain : ∀ (x : X) (hx : x ∈ u), (a, b) ∈ s
⊢ (a, b) ∈ s

Tactic:
obtain ⟨x, hx⟩ := hu
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
s : SetRel X X
t u v : Set X
inst : s.IsTrans
htu : t ×ˢ u ⊆ s
huv : u ×ˢ v ⊆ s
a b : X
hab : a ∈ t ∧ b ∈ v
x : X
hx : x ∈ u
⊢ (a, b) ∈ s

Tactic:
s.trans (@htu ⟨a, x⟩ ⟨hab.left, hx⟩) (@huv ⟨x, b⟩ ⟨hx, hab.right⟩)

Premises used: SetRel.trans, And.right, And.left, And.intro
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
s : SetRel X X
t u v : Set X
inst : s.IsTrans
htu : t ×ˢ u ⊆ s
huv : u ×ˢ v ⊆ s
a b : X
hab : a ∈ t ∧ b ∈ v
x : X
hx : x ∈ u
⊢ (a, b) ∈ s

Tactic:
exact s.trans (@htu ⟨a, x⟩ ⟨hab.left, hx⟩) (@huv ⟨x, b⟩ ⟨hx, hab.right⟩)

Premises used: SetRel.trans, And.right, And.left, And.intro
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
s : SetRel X X
f g h : Filter X
inst : g.NeBot
inst_1 : s.IsTrans
hfg : s ∈ f ×ˢ g
hgh : s ∈ g ×ˢ h
⊢ s ∈ f ×ˢ h

Tactic:
Eventually.trans_prod (p := (fun x y ↦ (x, y) ∈ s)) (q := (fun x y ↦ (x, y) ∈ s))
    (r := (fun x y ↦ (x, y) ∈ s)) hfg hgh fun _ _ _ ↦ s.trans

Premises used: SetRel.trans, Set.Mem, Filter.Eventually, setOf, Filter.Eventually.trans_prod
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
V : SetRel X X
inst : V.IsTrans
x y : X
hy : y ∈ ball x V
⊢ ball y V ⊆ ball x V

Tactic:
ball_subset_of_comp_subset hy SetRel.comp_subset_self

Premises used: SetRel.comp_subset_self, UniformSpace.ball_subset_of_comp_subset
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
V : SetRel X X
inst : V.IsSymm
inst_1 : V.IsTrans
x y : X
hy : y ∈ ball x V
⊢ ball x V = ball y V

Tactic:
le_antisymm (ball_subset_of_mem ?_) (ball_subset_of_mem hy)

Premises used: le_antisymm, ball_subset_of_mem
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
V : SetRel X X
inst : V.IsSymm
inst_1 : V.IsTrans
x y : X
hy : y ∈ ball x V
refine : x ∈ ball y V
⊢ ball x V = ball y V

Tactic:
refine le_antisymm (ball_subset_of_mem ?_) (ball_subset_of_mem hy)

Premises used: le_antisymm, ball_subset_of_mem
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
V : SetRel X X
inst : V.IsSymm
inst_1 : V.IsTrans
x y : X
hy rwa rwa₁ rwa₂ rwa₃ : y ∈ ball x V
⊢ x ∈ ball y V

Tactic:
rwa [← mem_ball_symmetry]

Premises used: UniformSpace.mem_ball_symmetry
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
rw : (∃ V ∈ 𝓤 X, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s

Tactic:
rw [UniformSpace.mem_nhds_iff]

Premises used: UniformSpace.mem_nhds_iff
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
mp : (∃ V ∈ 𝓤 X, ball x V ⊆ s) → ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
mpr : (∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 X, ball x V ⊆ s
⊢ (∃ V ∈ 𝓤 X, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
V_sub : ball x V ⊆ s
⊢ ∃ (i : SetRel X X), (i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans) ∧ id i ⊆ V

Tactic:
rw [IsUltraUniformity.hasBasis.mem_iff'] at V_in

Premises used: Filter.HasBasis.mem_iff', IsUltraUniformity.hasBasis
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
V_sub : ball x V ⊆ s
V_in₁ : ∃ (i : SetRel X X), (i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans) ∧ id i ⊆ V
⊢ ball x V ⊆ s

Tactic:
rw [IsUltraUniformity.hasBasis.mem_iff'] at V_in

Premises used: Filter.HasBasis.mem_iff', IsUltraUniformity.hasBasis
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
V : Set (X × X)
V_in : ∃ (i : SetRel X X), (i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans) ∧ id i ⊆ V
V_sub : ball x V ⊆ s
mp :
  ∀ (U : SetRel X X) (U_sub : id U ⊆ V) (U_in : U ∈ 𝓤 X) (U_sym : U.IsSymm) (U_trans : U.IsTrans),
    ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s

Tactic:
obtain ⟨U, ⟨U_in, U_sym, U_trans⟩, U_sub⟩ := V_in
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
V : Set (X × X)
V_sub : ball x V ⊆ s
U : SetRel X X
U_sub : id U ⊆ V
U_in : U ∈ 𝓤 X
U_sym : U.IsSymm
U_trans : U.IsTrans
⊢ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s

Tactic:
⟨U, U_in, U_sym, U_trans, (UniformSpace.ball_mono U_sub _).trans V_sub⟩

Premises used: UniformSpace.ball_mono, HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
V : Set (X × X)
V_sub : ball x V ⊆ s
U : SetRel X X
U_sub : id U ⊆ V
U_in : U ∈ 𝓤 X
U_sym : U.IsSymm
U_trans : U.IsTrans
⊢ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s

Tactic:
refine ⟨U, U_in, U_sym, U_trans, (UniformSpace.ball_mono U_sub _).trans V_sub⟩
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
left : SetRel.IsSymm V
left_1 : SetRel.IsTrans V
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 X, ball x V ⊆ s

Tactic:
⟨V, V_in, V_sub⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
left : SetRel.IsSymm V
left_1 : SetRel.IsTrans V
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 X, ball x V ⊆ s

Tactic:
exact ⟨V, V_in, V_sub⟩
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
x : X
V : SetRel X X
inst_1 : V.IsTrans
h' : V ∈ 𝓤 X
rw : ∀ x_1 ∈ ball x V, ∃ V_1 ∈ 𝓤 X, ball x_1 V_1 ⊆ ball x V
⊢ IsOpen[inst.toTopologicalSpace] (ball x V)

Tactic:
rw [isOpen_iff_ball_subset]

Premises used: isOpen_iff_ball_subset
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
x : X
V : SetRel X X
inst_1 : V.IsTrans
h' : V ∈ 𝓤 X
y : X
hy : y ∈ ball x V
⊢ ∃ V_1 ∈ 𝓤 X, ball y V_1 ⊆ ball x V

Tactic:
⟨V, h', ball_subset_of_mem hy⟩

Premises used: And.intro, Exists.intro, ball_subset_of_mem
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
x : X
V : SetRel X X
inst_1 : V.IsTrans
h' : V ∈ 𝓤 X
y : X
hy : y ∈ ball x V
⊢ ∃ V_1 ∈ 𝓤 X, ball y V_1 ⊆ ball x V

Tactic:
exact ⟨V, h', ball_subset_of_mem hy⟩
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
x : X
V : SetRel X X
inst_1 : V.IsSymm
inst_2 : V.IsTrans
h' : V ∈ 𝓤 X
rw : ∀ x_1 ∈ (ball x V)ᶜ, ∃ V_1 ∈ 𝓤 X, ball x_1 V_1 ⊆ (ball x V)ᶜ
⊢ IsClosed[inst.toTopologicalSpace] (ball x V)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_ball_subset]

Premises used: isOpen_iff_ball_subset, isOpen_compl_iff
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
x : X
V : SetRel X X
inst_1 : V.IsSymm
inst_2 : V.IsTrans
h' : V ∈ 𝓤 X
⊢ ∀ x_1 ∈ (ball x V)ᶜ, ∃ V_1 ∈ 𝓤 X, ball x_1 V_1 ⊆ (ball x V)ᶜ

Tactic:
fun y hy ↦ ⟨V, h', fun z hyz hxz ↦ hy <| V.trans hxz <| V.symm hyz⟩

Premises used: SetRel.trans, SetRel.symm, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
x : X
V : SetRel X X
inst_1 : V.IsSymm
inst_2 : V.IsTrans
h' : V ∈ 𝓤 X
⊢ ∀ x_1 ∈ (ball x V)ᶜ, ∃ V_1 ∈ 𝓤 X, ball x_1 V_1 ⊆ (ball x V)ᶜ

Tactic:
exact fun y hy ↦ ⟨V, h', fun z hyz hxz ↦ hy <| V.trans hxz <| V.symm hyz⟩
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
x : X
V : SetRel X X
inst_1 : V.IsSymm
inst_2 : V.IsTrans
h' : V ∈ 𝓤 X
⊢ IsClopen (ball x V)

Tactic:
⟨isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformity _ ‹_›, isOpen_ball_of_mem_uniformity _ ‹_›⟩

Premises used: UniformSpace.isOpen_ball_of_mem_uniformity, UniformSpace.isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformity, And.intro, IsClopen
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ x ∈ s ∧ IsClopen s) id

Tactic:
(nhds_basis_uniformity' (IsUltraUniformity.hasBasis)).to_hasBasis' ?_ ?_

Premises used: nhds_basis_uniformity', Filter.HasBasis.to_hasBasis', IsUltraUniformity.hasBasis
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
refine_1 :
  ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → ∃ (i' : Set X), (x ∈ i' ∧ IsClopen i') ∧ id i' ⊆ ball x (id i)
refine_2 : ∀ (i' : Set X), x ∈ i' ∧ IsClopen i' → id i' ∈ 𝓝 x
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ x ∈ s ∧ IsClopen s) id

Tactic:
refine (nhds_basis_uniformity' (IsUltraUniformity.hasBasis)).to_hasBasis' ?_ ?_

Premises used: nhds_basis_uniformity', Filter.HasBasis.to_hasBasis', IsUltraUniformity.hasBasis
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
V : SetRel X X
refine_1 :
  ∀ (hV : V ∈ 𝓤 X) (h_symm : V.IsSymm) (h_trans : V.IsTrans),
    ∃ (i' : Set X), (x ∈ i' ∧ IsClopen i') ∧ id i' ⊆ ball x (id V)
⊢ V ∈ 𝓤 X ∧ V.IsSymm ∧ V.IsTrans → ∃ (i' : Set X), (x ∈ i' ∧ IsClopen i') ∧ id i' ⊆ ball x (id V)

Tactic:
⟨hV, h_symm, h_trans⟩
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
V : SetRel X X
hV : V ∈ 𝓤 X
h_symm : V.IsSymm
h_trans : V.IsTrans
⊢ ∃ (i' : Set X), (x ∈ i' ∧ IsClopen i') ∧ id i' ⊆ ball x (id V)

Tactic:
⟨ball x V, ⟨mem_ball_self _ hV,
      isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity _ hV⟩, le_rfl⟩

Premises used: le_rfl, UniformSpace.isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity, UniformSpace.mem_ball_self, UniformSpace.ball, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
V : SetRel X X
hV : V ∈ 𝓤 X
h_symm : V.IsSymm
h_trans : V.IsTrans
⊢ ∃ (i' : Set X), (x ∈ i' ∧ IsClopen i') ∧ id i' ⊆ ball x (id V)

Tactic:
exact ⟨ball x V, ⟨mem_ball_self _ hV,
      isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity _ hV⟩, le_rfl⟩
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
u : Set X
hx : x ∈ u
hu : IsClopen u
⊢ id u ∈ 𝓝 x

Tactic:
simp [hu.right.mem_nhds_iff, hx]

Premises used: IsOpen.mem_nhds_iff, And.right
-- Module: Mathlib.Topology.UniformSpace.Ultra.Basic
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
⊢ (𝓝 x).HasBasis (fun (t : Set X) ↦ Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} t ∧ x ∈ t) id

Tactic:
simpa [and_comm] using nhds_basis_clopens x

Premises used: and_comm, UniformSpace.nhds_basis_clopens
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity Y
f : X → Y
hf : IsUniformInducing f
⊢ IsUltraUniformity X

Tactic:
hf.comap_uniformSpace ▸ .comap inferInstance f

Premises used: IsUniformInducing.comap_uniformSpace, Eq.rec, inferInstance, IsUltraUniformity.comap
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
s : SetRel X X
inst_2 : s.IsSymm
x : CauchyFilter X
⊢ ∀ (b : CauchyFilter X),
    Membership.mem (γ := SetRel (CauchyFilter X) (CauchyFilter X)) (gen s) (x, b) →
      Membership.mem (γ := SetRel (CauchyFilter X) (CauchyFilter X)) (gen s) (b, x)

Tactic:
simp [CauchyFilter.gen, s.mem_filter_prod_comm]

Premises used: CauchyFilter.gen, SetRel.mem_filter_prod_comm
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
h_symm :
  ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (α := CauchyFilter X) ((CauchyFilter.gen ∘ id) i)
h_trans :
  ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans (α := CauchyFilter X) ((CauchyFilter.gen ∘ id) i)
⊢ IsUltraUniformity.{u_1} (CauchyFilter X)

Tactic:
apply mk_of_hasBasis (CauchyFilter.basis_uniformity IsUltraUniformity.hasBasis)

Premises used: CauchyFilter.basis_uniformity, IsUltraUniformity.mk_of_hasBasis, IsUltraUniformity.hasBasis
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
x : SetRel X X
h : x ∈ 𝓤 X ∧ x.IsSymm ∧ x.IsTrans
left : x ∈ 𝓤 X
hU : x.IsSymm
right : x.IsTrans
simp : SetRel.IsSymm (α := CauchyFilter X) (CauchyFilter.gen x)
⊢ SetRel.IsSymm (α := CauchyFilter X) ((CauchyFilter.gen ∘ id) x)

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Ultra.Completion
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
x : SetRel X X
h : x ∈ 𝓤 X ∧ x.IsSymm ∧ x.IsTrans
left : x ∈ 𝓤 X
hU : x.IsSymm
right : x.IsTrans
⊢ SetRel.IsSymm (α := CauchyFilter X) (CauchyFilter.gen x)

Tactic:
infer_instance