awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
y : α
rcases : ∀ (x : α) (hxs : x ∈ s) (hxy : (x, y) ∈ U), ∃ (i : α) (_ : i ∈ s), y ∈ ball i U
⊢ ∃ (i : α) (_ : i ∈ s), y ∈ ball i U

Tactic:
rcases hs.inter_nhds_nonempty (mem_nhds_right y hU) with ⟨x, hxs, hxy : (x, y) ∈ U⟩

Premises used: Dense.inter_nhds_nonempty, mem_nhds_right
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
y x : α
hxs : x ∈ s
hxy : (x, y) ∈ U
⊢ ∃ (i : α) (_ : i ∈ s), y ∈ ball i U

Tactic:
⟨x, hxs, hxy⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
y x : α
hxs : x ∈ s
hxy : (x, y) ∈ U
⊢ ∃ (i : α) (_ : i ∈ s), y ∈ ball i U

Tactic:
exact ⟨x, hxs, hxy⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
ι : Type u_2
xs : ι → α
xs_dense : DenseRange xs
U : SetRel α α
hU : U ∈ 𝓤 α
rw : Eq.{ua + 1} (α := Set α) (⋃ x ∈ range xs, ball x U) univ
⊢ Eq.{ua + 1} (α := Set α) (⋃ (i : ι), ball (xs i) U) univ

Tactic:
rw [← biUnion_range (f := xs) (g := fun x ↦ UniformSpace.ball x U)]

Premises used: Set.biUnion_range
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
ι : Type u_2
xs : ι → α
xs_dense : DenseRange xs
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ Eq.{ua + 1} (α := Set α) (⋃ x ∈ range xs, ball x U) univ

Tactic:
Dense.biUnion_uniformity_ball xs_dense hU

Premises used: Dense.biUnion_uniformity_ball
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
ι : Type u_2
xs : ι → α
xs_dense : DenseRange xs
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ Eq.{ua + 1} (α := Set α) (⋃ x ∈ range xs, ball x U) univ

Tactic:
exact Dense.biUnion_uniformity_ball xs_dense hU

Premises used: Dense.biUnion_uniformity_ball
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ (𝓤 α).HasBasis (fun (V : SetRel α α) ↦ V ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] V) id

Tactic:
hasBasis_self.2 fun s hs =>
    ⟨interior s, interior_mem_uniformity hs, isOpen_interior, interior_subset⟩

Premises used: Iff.mpr, interior_subset, isOpen_interior, And.intro, interior, Exists.intro, Filter.hasBasis_self, interior_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
p : β → Prop
s : β → SetRel α α
h : (𝓤 α).HasBasis p s
t : SetRel α α
⊢ (∃ (i : β), p i ∧ s i ⊆ t) ↔ ∃ (i : β), p i ∧ ∀ (a b : α), (a, b) ∈ s i → (a, b) ∈ t

Tactic:
simp only [Prod.forall, subset_def]

Premises used: Set.subset_def, Prod.forall
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
simp : (𝓤 α).HasBasis (fun (V : SetRel α α) ↦ (V ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] V) ∧ V.IsSymm) id
⊢ (𝓤 α).HasBasis (fun (V : SetRel α α) ↦ V ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] V ∧ V.IsSymm) id

Tactic:
simp only [← and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ (𝓤 α).HasBasis (fun (V : SetRel α α) ↦ (V ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] V) ∧ V.IsSymm) id

Tactic:
uniformity_hasBasis_open.restrict fun s hs => ⟨SetRel.symmetrize s, ?_⟩

Premises used: SetRel.symmetrize, Filter.HasBasis.restrict, Exists.intro, uniformity_hasBasis_open
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
refine :
  ∀ (s : SetRel α α) (hs : s ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] s),
    (s.symmetrize ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] s.symmetrize) ∧ s.symmetrize.IsSymm ∧ id s.symmetrize ⊆ id s
⊢ (𝓤 α).HasBasis (fun (V : SetRel α α) ↦ (V ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] V) ∧ V.IsSymm) id

Tactic:
refine uniformity_hasBasis_open.restrict fun s hs => ⟨SetRel.symmetrize s, ?_⟩

Premises used: SetRel.symmetrize, Filter.HasBasis.restrict, Exists.intro, uniformity_hasBasis_open
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] s
⊢ (s.symmetrize ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] s.symmetrize) ∧ s.symmetrize.IsSymm ∧ id s.symmetrize ⊆ id s

Tactic:
⟨⟨symmetrize_mem_uniformity hs.1, IsOpen.inter hs.2 (hs.2.preimage continuous_swap)⟩,
      inferInstance, SetRel.symmetrize_subset_self⟩

Premises used: inferInstance, symmetrize_mem_uniformity, continuous_swap, And.right, And.left, And.intro, IsOpen.inter, SetRel.symmetrize_subset_self, IsOpen.preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] s
⊢ (s.symmetrize ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] s.symmetrize) ∧ s.symmetrize.IsSymm ∧ id s.symmetrize ⊆ id s

Tactic:
exact
    ⟨⟨symmetrize_mem_uniformity hs.1, IsOpen.inter hs.2 (hs.2.preimage continuous_swap)⟩,
      inferInstance, SetRel.symmetrize_subset_self⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
obtain :
  ∀ (t : Set (α × α)) (ht₁ : t ∈ 𝓤 α) (ht₂ : t ○ t ⊆ s),
    ∃ t ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] t ∧ SetRel.IsSymm t ∧ t ○ t ⊆ s
⊢ ∃ t ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] t ∧ SetRel.IsSymm t ∧ t ○ t ⊆ s

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs

Premises used: comp_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
obtain :
  ∀ (u : SetRel α α) (hu₄ : u ⊆ t) (hu₁ : u ∈ 𝓤 α) (hu₂ : IsOpen[instTopologicalSpaceProd] u) (hu₃ : u.IsSymm),
    ∃ t ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] t ∧ SetRel.IsSymm t ∧ t ○ t ⊆ s
⊢ ∃ t ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] t ∧ SetRel.IsSymm t ∧ t ○ t ⊆ s

Tactic:
obtain ⟨u, ⟨hu₁, hu₂, hu₃⟩, hu₄ : u ⊆ t⟩ := uniformity_hasBasis_open_symmetric.mem_iff.mp ht₁

Premises used: Filter.HasBasis.mem_iff, uniformity_hasBasis_open_symmetric, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
u : SetRel α α
hu₄ : u ⊆ t
hu₁ : u ∈ 𝓤 α
hu₂ : IsOpen[instTopologicalSpaceProd] u
hu₃ : u.IsSymm
⊢ ∃ t ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] t ∧ SetRel.IsSymm t ∧ t ○ t ⊆ s

Tactic:
⟨u, hu₁, hu₂, hu₃, (SetRel.comp_subset_comp hu₄ hu₄).trans ht₂⟩

Premises used: SetRel.comp_subset_comp, HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
ht₁ : t ∈ 𝓤 α
ht₂ : t ○ t ⊆ s
u : SetRel α α
hu₄ : u ⊆ t
hu₁ : u ∈ 𝓤 α
hu₂ : IsOpen[instTopologicalSpaceProd] u
hu₃ : u.IsSymm
⊢ ∃ t ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] t ∧ SetRel.IsSymm t ∧ t ○ t ⊆ s

Tactic:
exact ⟨u, hu₁, hu₂, hu₃, (SetRel.comp_subset_comp hu₄ hu₄).trans ht₂⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
⊢ u₁ ≤ u₂ ↔ 𝓤 α ≤ 𝓤 α

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
tt : Set (UniformSpace α)
t : UniformSpace α
h : t ∈ tt
⊢ sInf tt ≤ t

Tactic:
show ⨅ u ∈ tt, 𝓤[u] ≤ 𝓤[t] from iInf₂_le t h

Premises used: Set.Mem, iInf₂_le
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
tt : Set (UniformSpace α)
t : UniformSpace α
h : ∀ t' ∈ tt, t ≤ t'
⊢ t ≤ sInf tt

Tactic:
show 𝓤[t] ≤ ⨅ u ∈ tt, 𝓤[u] from le_iInf₂ h

Premises used: Set.Mem, le_iInf₂
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
tt : Set (UniformSpace α)
⊢ IsGLB tt (sInf tt)

Tactic:
⟨fun _ ↦ UniformSpace.sInf_le, fun _ ↦ UniformSpace.le_sInf⟩

Premises used: UniformSpace.sInf_le, UniformSpace.le_sInf, IsGreatest, IsGLB, And.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
x : α
⊢ 𝓝 x = comap (Prod.mk x) ⊤

Tactic:
simp only [nhds_top, comap_top]

Premises used: nhds_top, Filter.comap_top
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
⊢ Tendsto.{ua, ua} (α := α × α) Prod.swap (𝓟 SetRel.id) (𝓟 SetRel.id)

Tactic:
simp [Tendsto, SetRel.id]

Premises used: SetRel.id, Filter.Tendsto
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : α
x : TopologicalSpace α := ⊥
⊢ DiscreteTopology α

Tactic:
have := discreteTopology_bot α
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
s : α
x : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ 𝓝 s = comap (Prod.mk s) (𝓟 SetRel.id)

Tactic:
simp [SetRel.id]

Premises used: SetRel.id
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
x : α
rw : 𝓝 x ⊓ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
rw₁ : comap (Prod.mk x) (𝓤 α) ⊓ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
rw₂ : comap (Prod.mk x) (𝓤 α) ⊓ comap (Prod.mk x) (𝓤 α) = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)
rw₃ rw₄ : comap (Prod.mk x) (𝓤 α) ⊓ comap (Prod.mk x) (𝓤 α) = comap (Prod.mk x) (𝓤 α) ⊓ comap (Prod.mk x) (𝓤 α)
⊢ 𝓝 x = comap (Prod.mk x) (𝓤 α ⊓ 𝓤 α)

Tactic:
rw [@nhds_inf _ u₁.toTopologicalSpace _, @nhds_eq_comap_uniformity _ u₁,
          @nhds_eq_comap_uniformity _ u₂, comap_inf]

Premises used: nhds_inf, Filter.comap_inf, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
ι : Sort u_2
u : ι → UniformSpace α
⊢ 𝓤 α = ⨅ (i : ι), 𝓤 α

Tactic:
iInf_range

Premises used: iInf, uniformity, iInf_range
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
u v : UniformSpace α
⊢ 𝓤 α = 𝓤 α ⊓ 𝓤 α

Tactic:
rfl

Premises used: uniformity, rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
⊢ 𝓤 α = 𝓟 SetRel.id

Tactic:
rfl

Premises used: uniformity, Filter.principal, rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
⊢ 𝓤 α = ⊤

Tactic:
rfl

Premises used: uniformity, rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : Subsingleton α
u : UniformSpace α
rw : Membership.mem (γ := Filter (α × α)) ((fun (u : UniformSpace α) ↦ 𝓤 α) u) univ
⊢ Membership.mem (γ := Filter (α × α)) ((fun (u : UniformSpace α) ↦ 𝓤 α) u) SetRel.id

Tactic:
rw [SetRel.id, ← diagonal, diagonal_eq_univ]

Premises used: SetRel.id, Set.diagonal_eq_univ, Set.diagonal
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : Subsingleton α
u : UniformSpace α
⊢ Membership.mem (γ := Filter (α × α)) ((fun (u : UniformSpace α) ↦ 𝓤 α) u) univ

Tactic:
univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : Subsingleton α
u : UniformSpace α
⊢ Membership.mem (γ := Filter (α × α)) ((fun (u : UniformSpace α) ↦ 𝓤 α) u) univ

Tactic:
exact univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
simp :
  Tendsto.{ua, ub} (α := α × α) ((fun (p : α × α) ↦ (f p.1, f p.2)) ∘ Prod.swap)
    (Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β)) (𝓤 β)
⊢ Tendsto.{ua, ua} (α := α × α) Prod.swap (Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β))
    (Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β))

Tactic:
simp only [tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Tendsto.{ua, ub} (α := α × α) ((fun (p : α × α) ↦ (f p.1, f p.2)) ∘ Prod.swap)
    (Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β)) (𝓤 β)

Tactic:
tendsto_swap_uniformity.comp tendsto_comap

Premises used: tendsto_swap_uniformity, Filter.tendsto_comap, Prod.swap, Filter.Tendsto.comp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Tendsto.{ua, ub} (α := α × α) ((fun (p : α × α) ↦ (f p.1, f p.2)) ∘ Prod.swap)
    (Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β)) (𝓤 β)

Tactic:
exact tendsto_swap_uniformity.comp tendsto_comap

Premises used: tendsto_swap_uniformity, Filter.tendsto_comap, Filter.Tendsto.comp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
rw :
  LE.le.{ua} (α := Filter (α × α))
    ((𝓤 β).lift' ((fun (s : Set (α × α)) ↦ s ○ s) ∘ preimage fun (p : α × α) ↦ (f p.1, f p.2)))
    (Filter.lift'.{ub, ua} (α := β × β) UniformSpace.uniformity
      (Function.comp (β := Set (β × β)) (preimage fun (p : α × α) ↦ (f p.1, f p.2)) fun (s : Set (β × β)) ↦ s ○ s))
rw₁ : Monotone (β := Set (α × α)) fun (s : Set (α × α)) ↦ s ○ s
⊢ LE.le.{ua} (α := Filter (α × α))
    (Filter.lift' (α := α × α) (Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β)) fun (s : Set (α × α)) ↦ s ○ s)
    (Filter.comap.{ua, ub} (β := β × β) (fun (p : α × α) ↦ (f p.1, f p.2))
      (Filter.lift' (α := β × β) UniformSpace.uniformity fun (s : Set (β × β)) ↦ s ○ s))

Tactic:
rw [comap_lift'_eq, comap_lift'_eq2]

Premises used: Filter.comap_lift'_eq, Filter.comap_lift'_eq2
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ LE.le.{ua} (α := Filter (α × α))
    ((𝓤 β).lift' ((fun (s : Set (α × α)) ↦ s ○ s) ∘ preimage fun (p : α × α) ↦ (f p.1, f p.2)))
    (Filter.lift'.{ub, ua} (α := β × β) UniformSpace.uniformity
      (Function.comp (β := Set (β × β)) (preimage fun (p : α × α) ↦ (f p.1, f p.2)) fun (s : Set (β × β)) ↦ s ○ s))

Tactic:
lift'_mono' fun s _ ⟨a₁, a₂⟩ ⟨x, h₁, h₂⟩ => ⟨f x, h₁, h₂⟩

Premises used: Filter.lift'_mono', Set.Mem, setOf, Function.comp, Membership.mem, Prod.mk, Prod.fst, SetRel.comp, _private.0.UniformSpace.comap.match_2, Set.preimage, And.intro, Exists.intro, _private.0.UniformSpace.comap.match_1, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ LE.le.{ua} (α := Filter (α × α))
    ((𝓤 β).lift' ((fun (s : Set (α × α)) ↦ s ○ s) ∘ preimage fun (p : α × α) ↦ (f p.1, f p.2)))
    (Filter.lift'.{ub, ua} (α := β × β) UniformSpace.uniformity
      (Function.comp (β := Set (β × β)) (preimage fun (p : α × α) ↦ (f p.1, f p.2)) fun (s : Set (β × β)) ↦ s ○ s))

Tactic:
exact lift'_mono' fun s _ ⟨a₁, a₂⟩ ⟨x, h₁, h₂⟩ => ⟨f x, h₁, h₂⟩

Premises used: Filter.lift'_mono'
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Monotone (β := Set (α × α)) fun (s : Set (α × α)) ↦ s ○ s

Tactic:
monotone_id.relComp monotone_id

Premises used: monotone_id, Monotone.relComp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Monotone (β := Set (α × α)) fun (s : Set (α × α)) ↦ s ○ s

Tactic:
exact monotone_id.relComp monotone_id

Premises used: monotone_id, Monotone.relComp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
x : α
⊢ 𝓝 x = Filter.comap (Prod.mk x) (Filter.comap (fun (p : α × α) ↦ (f p.1, f p.2)) (𝓤 β))

Tactic:
simp only [nhds_induced, nhds_eq_comap_uniformity, comap_comap, Function.comp_def]

Premises used: Function.comp_def, Filter.comap_comap, nhds_induced, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
x : UniformSpace β
f : α → β
⊢ 𝓤 α = comap (Prod.map f f) (𝓤 β)

Tactic:
rfl

Premises used: uniformity, setOf, Prod.map, rfl, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
f : α → β
U : SetRel β β
x : α
h : ∀ (x_1 : α), x_1 ∈ UniformSpace.ball x (Prod.map f f ⁻¹' U) ↔ x_1 ∈ f ⁻¹' UniformSpace.ball (f x) U
⊢ UniformSpace.ball x (Prod.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U

Tactic:
ext : 1
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
f : α → β
U : SetRel β β
x x_1 : α
⊢ x_1 ∈ UniformSpace.ball x (Prod.map f f ⁻¹' U) ↔ x_1 ∈ f ⁻¹' UniformSpace.ball (f x) U

Tactic:
simp only [UniformSpace.ball, mem_preimage, Prod.map_apply]

Premises used: UniformSpace.ball, Prod.map_apply, Set.mem_preimage
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
h : ∀ (x : UniformSpace α), 𝓤 α = 𝓤 α
⊢ Eq.{u_2 + 1} (α := (u : UniformSpace α) → UniformSpace α) (UniformSpace.comap id) id

Tactic:
ext : 2
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
x : UniformSpace α
h : comap (Prod.map id id) (𝓤 α) = 𝓤 α
h₁ : comap id (𝓤 α) = 𝓤 α
h₂ h₃ : 𝓤 α = 𝓤 α
⊢ 𝓤 α = 𝓤 α

Tactic:
rw [uniformity_comap, Prod.map_id, comap_id]

Premises used: Filter.comap_id, uniformity_comap, Prod.map_id
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
uγ : UniformSpace γ
f : α → β
g : β → γ
h : 𝓤 α = 𝓤 α
⊢ comap (g ∘ f) uγ = comap f (comap g uγ)

Tactic:
ext1
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ 𝓤 α = 𝓤 α

Tactic:
simp only [uniformity_comap, Filter.comap_comap, Prod.map_comp_map]

Premises used: Prod.map_comp_map, Filter.comap_comap, uniformity_comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
γ : Type u_3
u₁ u₂ : UniformSpace γ
f : α → γ
⊢ comap f (u₁ ⊓ u₂) = comap f u₁ ⊓ comap f u₂

Tactic:
UniformSpace.ext Filter.comap_inf

Premises used: UniformSpace.ext, Filter.comap_inf
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
h : 𝓤 α = 𝓤 α
⊢ comap f (⨅ (i : ι), u i) = ⨅ (i : ι), comap f (u i)

Tactic:
ext : 1
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
⊢ 𝓤 α = 𝓤 α

Tactic:
simp [uniformity_comap, iInf_uniformity]

Premises used: iInf_uniformity, uniformity_comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
γ : Type u_3
f : α → γ
⊢ Monotone.{u_3, u_2} (β := UniformSpace α) fun (u : UniformSpace γ) ↦ comap f u

Tactic:
fun _ _ hu =>
  Filter.comap_mono hu

Premises used: Set.Mem, Monotone, Filter.comap_mono
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type u_2
β : Type u_3
uα : UniformSpace α
uβ : UniformSpace β
f : α → β
⊢ UniformContinuous f ↔ uα ≤ UniformSpace.comap f uβ

Tactic:
Filter.map_le_iff_le_comap

Premises used: UniformContinuous, Set.Mem, Filter.Tendsto, Filter.map_le_iff_le_comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
u v : UniformSpace α
rw : u ≤ v ↔ u ≤ UniformSpace.comap id v
rw₁ : u ≤ v ↔ u ≤ id v
rw₂ rw₃ : u ≤ v ↔ u ≤ v
⊢ u ≤ v ↔ UniformContinuous.{ua, ua} (α := α) id

Tactic:
rw [uniformContinuous_iff, uniformSpace_comap_id, id]

Premises used: id, uniformContinuous_iff, uniformSpace_comap_id
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
f : α → β
u : UniformSpace β
⊢ UniformContinuous f

Tactic:
tendsto_comap

Premises used: UniformContinuous, uniformity, Filter.tendsto_comap, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
γ : Type uc
f : γ → β
g : α → γ
v : UniformSpace β
u : UniformSpace α
h : UniformContinuous (f ∘ g)
⊢ UniformContinuous g

Tactic:
tendsto_comap_iff.2 h

Premises used: Iff.mpr, UniformContinuous, uniformity, Filter.tendsto_comap_iff, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
rw : (𝓤 α).lift' (ball a) ≤ (𝓤 α).lift' (ball a)
⊢ 𝓝 a ≤ 𝓝 a

Tactic:
rw [@nhds_eq_uniformity α u₁ a, @nhds_eq_uniformity α u₂ a]

Premises used: nhds_eq_uniformity
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ (𝓤 α).lift' (ball a) ≤ (𝓤 α).lift' (ball a)

Tactic:
lift'_mono h le_rfl

Premises used: le_rfl, Filter.lift'_mono
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ (𝓤 α).lift' (ball a) ≤ (𝓤 α).lift' (ball a)

Tactic:
exact lift'_mono h le_rfl

Premises used: le_rfl, Filter.lift'_mono
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
⊢ LE.le.{ua} (α := TopologicalSpace α) toTopologicalSpace toTopologicalSpace

Tactic:
le_of_nhds_le_nhds <| to_nhds_mono h

Premises used: le_of_nhds_le_nhds, UniformSpace.to_nhds_mono
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
f : α → β
u : UniformSpace β
⊢ toTopologicalSpace = TopologicalSpace.induced f toTopologicalSpace

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
u : UniformSpace α
⊢ u = ⊥ ↔ SetRel.id ∈ 𝓤 α

Tactic:
le_bot_iff.symm.trans le_principal_iff

Premises used: le_bot_iff, Filter.le_principal_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
ι : Sort u_2
p : ι → Prop
s : ι → SetRel α α
u : UniformSpace α
h : (𝓤 α).HasBasis p s
⊢ u = ⊥ ↔ ∃ (i : ι), p i ∧ Pairwise fun (x y : α) ↦ (x, y) ∉ s i

Tactic:
simp [uniformSpace_eq_bot, h.mem_iff, subset_def, Pairwise, not_imp_not]

Premises used: Filter.HasBasis.mem_iff, Set.subset_def, UniformSpace.uniformSpace_eq_bot, Pairwise, not_imp_not
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
⊢ Eq.{ua + 1} (α := TopologicalSpace α) toTopologicalSpace ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
⊢ Eq.{ua + 1} (α := TopologicalSpace α) toTopologicalSpace ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
ι : Sort u_2
u : ι → UniformSpace α
a : α
⊢ 𝓝 a = 𝓝 a

Tactic:
simp only [@nhds_eq_comap_uniformity _ (iInf u), nhds_iInf,
    iInf_uniformity, @nhds_eq_comap_uniformity _ (u _), Filter.comap_iInf]

Premises used: nhds_iInf, iInf_uniformity, Filter.comap_iInf, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
s : Set (UniformSpace α)
rw : Eq.{ua + 1} (α := TopologicalSpace α) toTopologicalSpace (⨅ i ∈ s, toTopologicalSpace)
⊢ Eq.{ua + 1} (α := TopologicalSpace α) toTopologicalSpace (⨅ i ∈ s, toTopologicalSpace)

Tactic:
rw [sInf_eq_iInf]

Premises used: sInf_eq_iInf
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
s : Set (UniformSpace α)
⊢ Eq.{ua + 1} (α := TopologicalSpace α) toTopologicalSpace (⨅ i ∈ s, toTopologicalSpace)

Tactic:
simp only [← toTopologicalSpace_iInf]

Premises used: UniformSpace.toTopologicalSpace_iInf
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
u v : UniformSpace α
⊢ Eq.{ua + 1} (α := TopologicalSpace α) toTopologicalSpace (toTopologicalSpace ⊓ toTopologicalSpace)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
⊢ Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f

Tactic:
continuous_iff_le_induced.mpr <| UniformSpace.toTopologicalSpace_mono <|
    uniformContinuous_iff.1 hf

Premises used: Iff.mpr, continuous_iff_le_induced, uniformContinuous_iff, Iff.mp, UniformSpace.toTopologicalSpace_mono
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
hf : UniformContinuous f
⊢ UniformContinuousOn f s

Tactic:
tendsto_inf_left hf

Premises used: Filter.tendsto_inf_left, UniformContinuousOn
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s t : Set α
hf : UniformContinuousOn f s
ht : t ⊆ s
⊢ 𝓟 (t ×ˢ t) ≤ 𝓟 (s ×ˢ s)

Tactic:
simp [ht]