awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
u₂ : UniformSpace α
toTopologicalSpace : TopologicalSpace α
uniformity : Filter (α × α)
symm : Tendsto Prod.swap uniformity uniformity
comp : (uniformity.lift' fun (s : Set (α × α)) ↦ s ○ s) ≤ uniformity
nhds_eq_comap_uniformity : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity
h : 𝓤 α = 𝓤 α
this : Eq.{ua + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace
mk :
  ∀ [toTopologicalSpace_1 : TopologicalSpace α] (uniformity_1 : Filter (α × α))
    (symm_1 : Tendsto Prod.swap uniformity_1 uniformity_1)
    (comp_1 : (uniformity_1.lift' fun (s : Set (α × α)) ↦ s ○ s) ≤ uniformity_1)
    (nhds_eq_comap_uniformity_1 : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity_1) (h : 𝓤 α = 𝓤 α)
    (this : Eq.{ua + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace),
    { toTopologicalSpace := toTopologicalSpace, uniformity := uniformity, symm := symm, comp := comp,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity : UniformSpace α } =
      { toTopologicalSpace := toTopologicalSpace_1, uniformity := uniformity_1, symm := symm_1, comp := comp_1,
        nhds_eq_comap_uniformity := nhds_eq_comap_uniformity_1 }
⊢ { toTopologicalSpace := toTopologicalSpace, uniformity := uniformity, symm := symm, comp := comp,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity : UniformSpace α } =
    u₂

Tactic:
cases u₂
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
toTopologicalSpace : TopologicalSpace α
uniformity : Filter (α × α)
symm : Tendsto Prod.swap uniformity uniformity
comp : (uniformity.lift' fun (s : Set (α × α)) ↦ s ○ s) ≤ uniformity
nhds_eq_comap_uniformity : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity
toTopologicalSpace_1 : TopologicalSpace α
uniformity_1 : Filter (α × α)
symm_1 : Tendsto Prod.swap uniformity_1 uniformity_1
comp_1 : (uniformity_1.lift' fun (s : Set (α × α)) ↦ s ○ s) ≤ uniformity_1
nhds_eq_comap_uniformity_1 : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity_1
h : 𝓤 α = 𝓤 α
this : Eq.{ua + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace, uniformity := uniformity, symm := symm, comp := comp,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity : UniformSpace α } =
    { toTopologicalSpace := toTopologicalSpace_1, uniformity := uniformity_1, symm := symm_1, comp := comp_1,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity_1 }

Tactic:
congr
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h h₁ : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
⊢ u₁ = u₂

Tactic:
ext
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
s : Set (α × α)
⊢ s ∈ 𝓤 α ↔ s ∈ 𝓤 α

Tactic:
h _
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
u₁ u₂ : UniformSpace α
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
s : Set (α × α)
⊢ s ∈ 𝓤 α ↔ s ∈ 𝓤 α

Tactic:
exact h _
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
u : UniformSpace α
t : TopologicalSpace α
h : t = u.toCore.toTopologicalSpace
⊢ ofCoreEq u.toCore t h = u

Tactic:
UniformSpace.ext rfl

Premises used: UniformSpace.ext, rfl
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α_1 : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u_2
i : TopologicalSpace α
u : UniformSpace α
h : i = toTopologicalSpace
x : α
rw : 𝓝 x = comap (Prod.mk x) UniformSpace.uniformity
rw₁ rw₂ : comap (Prod.mk x) UniformSpace.uniformity = comap (Prod.mk x) UniformSpace.uniformity
⊢ 𝓝 x = comap (Prod.mk x) UniformSpace.uniformity

Tactic:
rw [h, u.nhds_eq_comap_uniformity]

Premises used: UniformSpace.nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type u_2
i : TopologicalSpace α
u : UniformSpace α
h : i = toTopologicalSpace
⊢ u.replaceTopology h = u

Tactic:
UniformSpace.ext rfl

Premises used: UniformSpace.ext, rfl
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
⊢ 𝓝 x = comap (Prod.mk x) (𝓤 α)

Tactic:
UniformSpace.nhds_eq_comap_uniformity x

Premises used: uniformity, UniformSpace.nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
⊢ IsOpen[inst.toTopologicalSpace] s ↔ ∀ x ∈ s, {p : α × α | p.1 = x → p.2 ∈ s} ∈ 𝓤 α

Tactic:
simp only [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap_prodMk]

Premises used: Filter.mem_comap_prodMk, nhds_eq_comap_uniformity, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
⊢ 𝓟 SetRel.id ≤ 𝓤 α

Tactic:
(@UniformSpace.toCore α _).refl

Premises used: Set.Mem, UniformSpace.toCore, UniformSpace.Core.refl
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst : UniformSpace α
inst_1 : Nonempty α
⊢ (𝓤 α).NeBot

Tactic:
diagonal_nonempty.principal_neBot.mono refl_le_uniformity

Premises used: Set.Nonempty.principal_neBot, Filter.NeBot.mono, Set.diagonal_nonempty, refl_le_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : SetRel α α
h : s ∈ 𝓤 α
⊢ (x, x) ∈ s

Tactic:
refl_le_uniformity h rfl

Premises used: refl_le_uniformity, rfl
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
h : s ∈ 𝓤 α
⊢ s.IsRefl

Tactic:
⟨fun _ => refl_mem_uniformity h⟩

Premises used: Std.Refl.mk, refl_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x y : α
s : SetRel α α
h : s ∈ 𝓤 α
hx : x = y
⊢ (x, y) ∈ s

Tactic:
refl_le_uniformity h hx

Premises used: refl_le_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
⊢ map Prod.swap (𝓤 α) ≤ 𝓤 α

Tactic:
UniformSpace.symm

Premises used: Set.Mem, Filter.Tendsto, UniformSpace.symm
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
⊢ ((𝓤 α).lift' fun (s : SetRel α α) ↦ s ○ s) ≤ 𝓤 α

Tactic:
UniformSpace.comp

Premises used: UniformSpace.comp, Set.Mem, setOf
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
⊢ ((𝓤 α).lift' fun (s : SetRel α α) ↦ s ○ s) = 𝓤 α

Tactic:
comp_le_uniformity.antisymm <| le_lift'.2 fun _s hs ↦ mem_of_superset hs <|
    have := isRefl_of_mem_uniformity hs; SetRel.left_subset_comp

Premises used: Iff.mpr, SetRel.left_subset_comp, LE.le.antisymm, isRefl_of_mem_uniformity, Filter.le_lift', comp_le_uniformity, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
⊢ Tendsto Prod.swap (𝓤 α) (𝓤 α)

Tactic:
symm_le_uniformity

Premises used: symm_le_uniformity, Filter.Tendsto
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, t ○ t ⊆ s

Tactic:
(mem_lift'_sets <| monotone_id.relComp monotone_id).mp <| comp_le_uniformity hs

Premises used: monotone_id, Monotone.relComp, Filter.mem_lift'_sets, comp_le_uniformity, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun (x : β) ↦ (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun (x : β) ↦ (f₂ x, f₃ x)) l (𝓤 α)
⊢ Tendsto (fun (x : β) ↦ (f₁ x, f₃ x)) l (𝓤 α)

Tactic:
le_trans (le_lift'.2 fun s hs => mem_map.2 ?_) comp_le_uniformity

Premises used: Iff.mpr, Filter.le_lift', Filter.Tendsto, comp_le_uniformity, Filter.mem_map, le_trans
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun (x : β) ↦ (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun (x : β) ↦ (f₂ x, f₃ x)) l (𝓤 α)
refine : ∀ (s : Set (α × α)) (hs : s ∈ 𝓤 α), (fun (x : β) ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s) ∈ l
⊢ Tendsto (fun (x : β) ↦ (f₁ x, f₃ x)) l (𝓤 α)

Tactic:
refine le_trans (le_lift'.2 fun s hs => mem_map.2 ?_) comp_le_uniformity

Premises used: Iff.mpr, Filter.le_lift', comp_le_uniformity, Filter.mem_map, le_trans
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun (x : β) ↦ (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun (x : β) ↦ (f₂ x, f₃ x)) l (𝓤 α)
s : Set (α × α)
hs : s ∈ 𝓤 α
x : β
hx₁₂ : Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₁ x, f₂ x)) ⁻¹' s) x
hx₂₃ : Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₂ x, f₃ x)) ⁻¹' s) x
⊢ Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s)) x

Tactic:
⟨_, hx₁₂, hx₂₃⟩

Premises used: Set.Mem, setOf, SetRel.comp, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun (x : β) ↦ (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun (x : β) ↦ (f₂ x, f₃ x)) l (𝓤 α)
s : Set (α × α)
hs : s ∈ 𝓤 α
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₁ x, f₂ x)) ⁻¹' s) x →
          Membership.mem (γ := Set β)
            {x : β |
              Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₂ x, f₃ x)) ⁻¹' s) x →
                Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s)) x}
            x}
      a
h₁ h₂ :
  ∀ (x : β) (hx₁₂ : Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₁ x, f₂ x)) ⁻¹' s) x)
    (hx₂₃ : Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₂ x, f₃ x)) ⁻¹' s) x),
    Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s)) x
⊢ (fun (x : β) ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s) ∈ l

Tactic:
filter_upwards [mem_map.1 (h₁₂ hs), mem_map.1 (h₂₃ hs)] with x hx₁₂ hx₂₃ using ⟨_, hx₁₂, hx₂₃⟩

Premises used: Iff.mp, Filter.mem_map
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
l : Filter β
f : β → α × α
h : Tendsto f l (𝓤 α)
⊢ Tendsto (fun (x : β) ↦ ((f x).2, (f x).1)) l (𝓤 α)

Tactic:
tendsto_swap_uniformity.comp h

Premises used: tendsto_swap_uniformity, Prod.swap, Filter.Tendsto.comp
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : β → α
l : Filter β
⊢ Tendsto (fun (x : β) ↦ (f x, f x)) l (𝓤 α)

Tactic:
fun _s hs =>
  mem_map.2 <| univ_mem' fun _ => refl_mem_uniformity hs

Premises used: Iff.mpr, refl_mem_uniformity, Filter.Tendsto, Filter.mem_map, Filter.univ_mem'
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
a : α
f : Filter β
⊢ Tendsto (fun (x : β) ↦ (a, a)) f (𝓤 α)

Tactic:
tendsto_diag_uniformity (fun _ => a) f

Premises used: tendsto_diag_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ⊆ s

Tactic:
have : preimage Prod.swap s ∈ 𝓤 α := symm_le_uniformity hs
  ⟨s ∩ preimage Prod.swap s, inter_mem hs this, ⟨fun _ _ ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩⟩, inter_subset_left⟩

Premises used: Std.Symm.mk, Filter.inter_mem, Membership.mem, Set.inter_subset_left, Prod.mk, Inter.inter, symm_le_uniformity, Set.preimage, And.intro, Exists.intro, Prod.swap, _private.0.symm_of_uniformity.match_1
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, (∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t) ∧ t ○ t ⊆ s

Tactic:
let ⟨_t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs
  let ⟨t', ht', _, ht'₂⟩ := symm_of_uniformity ht₁
  ⟨t', ht', SetRel.symm _, Subset.trans (monotone_id.relComp monotone_id ht'₂) ht₂⟩

Premises used: Set.Subset.trans, uniformity, monotone_id, _private.0.comp_symm_of_uniformity.match_2, Membership.mem, Exists, Monotone.relComp, HasSubset.Subset, SetRel.symm, _private.0.comp_symm_of_uniformity.match_1, SetRel.comp, comp_mem_uniformity_sets, And, And.intro, Exists.intro, symm_of_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
rw : 𝓤 α ≤ comap Prod.swap (𝓤 α)
⊢ 𝓤 α ≤ map Prod.swap (𝓤 α)

Tactic:
rw [map_swap_eq_comap_swap]

Premises used: Filter.map_swap_eq_comap_swap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)

Tactic:
tendsto_swap_uniformity.le_comap

Premises used: Filter.Tendsto.le_comap, tendsto_swap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)

Tactic:
exact tendsto_swap_uniformity.le_comap

Premises used: Filter.Tendsto.le_comap, tendsto_swap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
⊢ 𝓤 α = map Prod.swap (𝓤 α)

Tactic:
le_antisymm uniformity_le_symm symm_le_uniformity

Premises used: uniformity_le_symm, symm_le_uniformity, le_antisymm
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
⊢ comap Prod.swap (𝓤 α) = 𝓤 α

Tactic:
(congr_arg _ uniformity_eq_symm).trans <| comap_map Prod.swap_injective

Premises used: uniformity_eq_symm, Filter.comap_map, congr_arg, Prod.swap_injective, Eq.trans
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
apply : V.inv ∈ (𝓤 α).sets
⊢ V.symmetrize ∈ 𝓤 α

Tactic:
apply (𝓤 α).inter_sets h

Premises used: uniformity, Filter.inter_sets
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
rw : V.inv ∈ (comap Prod.swap (𝓤 α)).sets
⊢ V.inv ∈ (𝓤 α).sets

Tactic:
rw [← comap_swap_uniformity]

Premises used: comap_swap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.inv ∈ (comap Prod.swap (𝓤 α)).sets

Tactic:
preimage_mem_comap h

Premises used: Set.Mem, SetRel.inv, setOf, Filter.preimage_mem_comap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.inv ∈ (comap Prod.swap (𝓤 α)).sets

Tactic:
exact preimage_mem_comap h

Premises used: Filter.preimage_mem_comap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
⊢ (𝓤 α).HasBasis (fun (s : SetRel α α) ↦ s ∈ 𝓤 α ∧ s.IsSymm) id

Tactic:
hasBasis_self.2 fun t t_in =>
    ⟨SetRel.symmetrize t, symmetrize_mem_uniformity t_in, inferInstance,
      SetRel.symmetrize_subset_self⟩

Premises used: Iff.mpr, SetRel.symmetrize, inferInstance, symmetrize_mem_uniformity, And.intro, Exists.intro, SetRel.symmetrize_subset_self, Filter.hasBasis_self
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun (s : Set (α × α)) ↦ g (Prod.swap ⁻¹' s)) ≤ f
rw : (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f
⊢ (map Prod.swap (𝓤 α)).lift g ≤ f

Tactic:
rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]

Premises used: Set.image_swap_eq_preimage_swap, Filter.map_lift_eq2
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun (s : Set (α × α)) ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f

Tactic:
h

Premises used: Set.Mem, setOf
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun (s : Set (α × α)) ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f

Tactic:
exact h
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
hg : Monotone (β := Set (α × α)) fun (s : SetRel α α) ↦ s ○ s
hh : Monotone f
⊢ ((𝓤 α).lift fun (s : Set (α × α)) ↦ f (s ○ s)) = Filter.lift ((𝓤 α).lift' fun (s : SetRel α α) ↦ s ○ s) f

Tactic:
rw [lift_lift'_assoc]

Premises used: Filter.lift_lift'_assoc
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone (β := Set (α × α)) fun (s : SetRel α α) ↦ s ○ s

Tactic:
monotone_id.relComp monotone_id

Premises used: monotone_id, Monotone.relComp
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone (β := Set (α × α)) fun (s : SetRel α α) ↦ s ○ s

Tactic:
exact monotone_id.relComp monotone_id

Premises used: monotone_id, Monotone.relComp
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone f

Tactic:
h
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone f

Tactic:
exact h
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, t ○ (t ○ t) ⊆ s

Tactic:
let ⟨_t', ht', ht's⟩ := comp_mem_uniformity_sets hs
  let ⟨t, ht, htt'⟩ := comp_mem_uniformity_sets ht'
  have := isRefl_of_mem_uniformity ht
  ⟨t, ht, (SetRel.comp_subset_comp (SetRel.left_subset_comp.trans htt') htt').trans ht's⟩

Premises used: SetRel.comp_subset_comp, uniformity, SetRel.left_subset_comp, _private.0.comp_symm_of_uniformity.match_2, Membership.mem, Exists, HasSubset.Subset.trans, HasSubset.Subset, isRefl_of_mem_uniformity, SetRel.comp, comp_mem_uniformity_sets, And, _private.0.comp3_mem_uniformity.match_1, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
⊢ ((𝓤 α).lift' fun (s : SetRel α α) ↦ s ○ (s ○ s)) ≤ 𝓤 α

Tactic:
fun _ h =>
  let ⟨_t, htU, ht⟩ := comp3_mem_uniformity h
  mem_of_superset (mem_lift' htU) ht

Premises used: comp3_mem_uniformity, uniformity, Membership.mem, Filter.mem_lift', SetRel.comp, Filter.lift', _private.0.comp_le_uniformity3.match_1, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∃ w ∈ 𝓤 α, w ○ w ⊆ s

Tactic:
comp_mem_uniformity_sets hs

Premises used: comp_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
obtain : ∀ (w : Set (α × α)) (w_in : w ∈ 𝓤 α) (w_sub : w ○ w ⊆ s), ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ⊆ s
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ⊆ s

Tactic:
obtain ⟨w, w_in, w_sub⟩ : ∃ w ∈ 𝓤 α, w ○ w ⊆ s := comp_mem_uniformity_sets hs

Premises used: uniformity, comp_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
right : SetRel.symmetrize w ○ SetRel.symmetrize w ⊆ s
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ⊆ s

Tactic:
use SetRel.symmetrize w, symmetrize_mem_uniformity w_in, inferInstance

Premises used: SetRel.symmetrize, symmetrize_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ SetRel.symmetrize w ⊆ w

Tactic:
have : SetRel.symmetrize w ⊆ w := SetRel.symmetrize_subset_self
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : SetRel.symmetrize w ⊆ w
⊢ SetRel.symmetrize w ○ SetRel.symmetrize w ⊆ w ○ w

Tactic:
gcongr
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : SetRel.symmetrize w ⊆ w
⊢ w ○ w ⊆ s

Tactic:
w_sub
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : SetRel.symmetrize w ⊆ w
calc : SetRel.symmetrize w ○ SetRel.symmetrize w ⊆ w ○ w
⊢ SetRel.symmetrize w ○ SetRel.symmetrize w ⊆ s

Tactic:
calc SetRel.symmetrize w ○ SetRel.symmetrize w
    _ ⊆ w ○ w := by gcongr
    _ ⊆ s := w_sub

Premises used: SetRel.symmetrize
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
h : s ∈ 𝓤 α
⊢ s ⊆ s ○ s

Tactic:
have := isRefl_of_mem_uniformity h; SetRel.left_subset_comp

Premises used: SetRel.left_subset_comp, isRefl_of_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
rcases :
  ∀ (w : Set (α × α)) (w_in : w ∈ 𝓤 α),
    SetRel.IsSymm w → ∀ (w_sub : w ○ w ⊆ s), ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s

Tactic:
rcases comp_symm_mem_uniformity_sets hs with ⟨w, w_in, _, w_sub⟩

Premises used: comp_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
rcases :
  ∀ (t : Set (α × α)) (t_in : t ∈ 𝓤 α) (t_symm : SetRel.IsSymm t) (t_sub : t ○ t ⊆ w),
    ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s

Tactic:
rcases comp_symm_mem_uniformity_sets w_in with ⟨t, t_in, t_symm, t_sub⟩

Premises used: comp_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
right : t ○ t ○ t ⊆ s
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s

Tactic:
use t, t_in, t_symm
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
⊢ t ⊆ t ○ t

Tactic:
have : t ⊆ t ○ t := subset_comp_self_of_mem_uniformity t_in
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ t ○ t ○ t ⊆ w ○ (t ○ t)

Tactic:
gcongr
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ w ○ (t ○ t) ⊆ w ○ w

Tactic:
gcongr
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ w ○ w ⊆ s

Tactic:
w_sub
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
t₁ : t ○ t ○ t ⊆ w ○ (t ○ t)
t₂ : w ○ (t ○ t) ⊆ w ○ w
⊢ t ○ t ○ t ⊆ s

Tactic:
calc
    t ○ t ○ t ⊆ w ○ (t ○ t) := by gcongr
    _ ⊆ w ○ w := by gcongr
    _ ⊆ s := w_sub

Premises used: SetRel.comp
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : SetRel α α
⊢ V ∈ 𝓤 α → x ∈ ball x V

Tactic:
refl_mem_uniformity

Premises used: Set.Mem, setOf, refl_mem_uniformity, UniformSpace.ball, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
V W : Set (β × β)
x y z : β
h : y ∈ ball x V
h' : z ∈ ball y W
⊢ z ∈ ball x (V ○ W)

Tactic:
SetRel.prodMk_mem_comp h h'

Premises used: Set.Mem, setOf, UniformSpace.ball, SetRel.comp, Set.preimage, SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
V W : Set (β × β)
x y : β
h : x ∈ ball y W
h' : W ○ W ⊆ V
⊢ ball x W ⊆ ball y V

Tactic:
fun _z z_in => h' (mem_ball_comp h z_in)

Premises used: UniformSpace.mem_ball_comp, Set.Mem, setOf, Set.Subset, UniformSpace.ball, Set.preimage