awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x_1 : α × α
x y : α
hp : (x, y) ∈ s
⊢ Monotone (β := Set (α × α)) fun (s : SetRel α α) ↦
    SProd.sprod (α := Set α) (β := Set α) {y : α | (y, x) ∈ s} {y_1 : α | (y, y_1) ∈ s}

Tactic:
fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩

Premises used: Set.Mem, Monotone, setOf, Set.prod, Set.Subset, And.right, And.left, And.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x_1 : α × α
x y : α
hp : (x, y) ∈ s
⊢ Monotone (β := Set (α × α)) fun (s : SetRel α α) ↦
    SProd.sprod (α := Set α) (β := Set α) {y : α | (y, x) ∈ s} {y_1 : α | (y, y_1) ∈ s}

Tactic:
exact fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
⊢ ∀ p ∈ s, ∃ t ⊆ cl_d, IsOpen[instTopologicalSpaceProd] t ∧ p ∈ t

Tactic:
have : ∀ p ∈ s, ∃ t, t ⊆ cl_d ∧ IsOpen t ∧ p ∈ t := fun ⟨x, y⟩ hp =>
    mem_nhds_iff.mp <|
      show cl_d ∈ 𝓝 (x, y) by
        rw [nhds_eq_uniformity_prod, mem_lift'_sets]
        · exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩
        · exact fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
this : ∀ p ∈ s, ∃ t ⊆ cl_d, IsOpen[instTopologicalSpaceProd] t ∧ p ∈ t
choose :
  ∀ (t : (p : α × α) → p ∈ s → Set (α × α))
    (ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen[instTopologicalSpaceProd] (t p a) ∧ p ∈ t p a),
    ∃ (t : SetRel α α),
      IsOpen[instTopologicalSpaceProd] t ∧
        s ⊆ t ∧ t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
⊢ ∃ (t : SetRel α α),
    IsOpen[instTopologicalSpaceProd] t ∧
      s ⊆ t ∧ t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}

Tactic:
choose t ht using this
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen[instTopologicalSpaceProd] (t p a) ∧ p ∈ t p a
x : α × α
a b : α
hp : (a, b) ∈ s
simp : ∃ (a_1 : α) (b_1 : α) (i : (a_1, b_1) ∈ s), (a, b) ∈ t (a_1, b_1) i
⊢ Membership.mem (γ := Set (α × α)) (⋃ (p : α × α), ⋃ (h : p ∈ s), t p h) (a, b)

Tactic:
simp only [mem_iUnion, Prod.exists]

Premises used: Set.mem_iUnion, Prod.exists
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen[instTopologicalSpaceProd] (t p a) ∧ p ∈ t p a
x : α × α
a b : α
hp : (a, b) ∈ s
⊢ ∃ (a_1 : α) (b_1 : α) (i : (a_1, b_1) ∈ s), (a, b) ∈ t (a_1, b_1) i

Tactic:
⟨a, b, hp, (ht (a, b) hp).right.right⟩

Premises used: Prod.mk, And.right, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen[instTopologicalSpaceProd] (t p a) ∧ p ∈ t p a
x : α × α
a b : α
hp : (a, b) ∈ s
⊢ ∃ (a_1 : α) (b_1 : α) (i : (a_1, b_1) ∈ s), (a, b) ∈ t (a_1, b_1) i

Tactic:
exact ⟨a, b, hp, (ht (a, b) hp).right.right⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen[instTopologicalSpaceProd] (t p a) ∧ p ∈ t p a
⊢ ∃ (t : SetRel α α),
    IsOpen[instTopologicalSpaceProd] t ∧
      s ⊆ t ∧ t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}

Tactic:
exact ⟨(⋃ p : α × α, ⋃ h : p ∈ s, t p h : SetRel α α),
    isOpen_iUnion fun p : α × α => isOpen_iUnion fun hp => (ht p hp).right.left,
    fun ⟨a, b⟩ hp => by
      simp only [mem_iUnion, Prod.exists]; exact ⟨a, b, hp, (ht (a, b) hp).right.right⟩,
    iUnion_subset fun p => iUnion_subset fun hp => (ht p hp).left⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
rcases : ∀ (w : Set (α × α)) (w_in : w ∈ 𝓤 α) (w_symm : SetRel.IsSymm w) (w_sub : w ○ w ⊆ V), V ∈ 𝓝 (x, x)
⊢ V ∈ 𝓝 (x, x)

Tactic:
rcases comp_symm_mem_uniformity_sets V_in with ⟨w, w_in, w_symm, w_sub⟩

Premises used: comp_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
rw : ball x w ×ˢ ball x w ∈ 𝓝 x ×ˢ 𝓝 x
⊢ ball x w ×ˢ ball x w ∈ 𝓝 (x, x)

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 x ×ˢ 𝓝 x

Tactic:
prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)

Premises used: UniformSpace.ball_mem_nhds, Filter.prod_mem_prod
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 x ×ˢ 𝓝 x

Tactic:
exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)

Premises used: UniformSpace.ball_mem_nhds, Filter.prod_mem_prod
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 (x, x)

Tactic:
have : ball x w ×ˢ ball x w ∈ 𝓝 (x, x) := by
    rw [nhds_prod_eq]
    exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
apply : ball x w ×ˢ ball x w ⊆ V
⊢ V ∈ 𝓝 (x, x)

Tactic:
apply mem_of_superset this

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
u v : α
u_in : (u, v).1 ∈ ball x w
v_in : (u, v).2 ∈ ball x w
⊢ (u, v) ∈ V

Tactic:
w_sub (mem_comp_of_mem_ball u_in v_in)

Premises used: UniformSpace.mem_comp_of_mem_ball
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
u v : α
u_in : (u, v).1 ∈ ball x w
v_in : (u, v).2 ∈ ball x w
⊢ (u, v) ∈ V

Tactic:
exact w_sub (mem_comp_of_mem_ball u_in v_in)

Premises used: UniformSpace.mem_comp_of_mem_ball
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ ⨆ (x : α), 𝓝 (x, x) ≤ 𝓤 α

Tactic:
iSup_le nhds_le_uniformity

Premises used: Set.Mem, nhds_le_uniformity, iSup_le
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ 𝓝ˢ (diagonal α) ≤ 𝓤 α

Tactic:
(nhdsSet_diagonal α).trans_le iSup_nhds_le_uniformity

Premises used: iSup_nhds_le_uniformity, Eq.trans_le, nhdsSet_diagonal
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : (𝓤 α).IsCountablyGenerated
⊢ ∃ (V : ℕ → SetRel α α), (𝓤 α).HasAntitoneBasis V ∧ ∀ (n : ℕ), (V n).IsSymm

Tactic:
let ⟨U, hsym, hbasis⟩ := (@UniformSpace.hasBasis_symmetric α _).exists_antitone_subbasis
  ⟨U, hbasis, fun n => (hsym n).2⟩

Premises used: Filter.HasBasis.exists_antitone_subbasis, uniformity, Exists, And, And.right, And.intro, Exists.intro, _private.0.UniformSpace.has_seq_basis.match_1, UniformSpace.hasBasis_symmetric, Filter.HasAntitoneBasis
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set (α × α)
h :
  ∀ (x y : α),
    (x, y) ∈ closure[instTopologicalSpaceProd] s ↔
      Membership.mem (γ := Set (α × α))
        (⋂ (V : Set (α × α)),
          ⋂ (_ : Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} V), V ○ s ○ V)
        (x, y)
⊢ closure[instTopologicalSpaceProd] s =
    ⋂ (V : Set (α × α)),
      ⋂ (_ : Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} V), V ○ s ○ V

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set (α × α)
x y : α
⊢ (x, y) ∈ closure[instTopologicalSpaceProd] s ↔
    Membership.mem (γ := Set (α × α))
      (⋂ (V : Set (α × α)),
        ⋂ (_ : Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} V), V ○ s ○ V)
      (x, y)

Tactic:
simp +contextual only
    [mem_closure_iff_nhds_basis (UniformSpace.hasBasis_nhds_prod x y), mem_iInter, mem_setOf_eq,
      and_imp, mem_comp_comp, ← mem_inter_iff, inter_comm, Set.Nonempty]

Premises used: and_imp, Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_iInter, Set.inter_comm, Set.Nonempty, UniformSpace.mem_comp_comp, UniformSpace.hasBasis_nhds_prod, mem_closure_iff_nhds_basis
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ (𝓤 α).HasBasis (fun (V : SetRel α α) ↦ V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V) id

Tactic:
Filter.hasBasis_self.2 fun t h => ?_

Premises used: Iff.mpr, Filter.hasBasis_self
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
refine : ∀ (t : Set (α × α)) (h : t ∈ 𝓤 α), ∃ r ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] r ∧ r ⊆ t
⊢ (𝓤 α).HasBasis (fun (V : SetRel α α) ↦ V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V) id

Tactic:
refine Filter.hasBasis_self.2 fun t h => ?_

Premises used: Iff.mpr, Filter.hasBasis_self
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
rcases :
  ∀ (w : Set (α × α)) (w_in : w ∈ 𝓤 α) (w_symm : SetRel.IsSymm w) (r : w ○ w ○ w ⊆ t),
    ∃ r ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] r ∧ r ⊆ t
⊢ ∃ r ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] r ∧ r ⊆ t

Tactic:
rcases comp_comp_symm_mem_uniformity_sets h with ⟨w, w_in, w_symm, r⟩

Premises used: comp_comp_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ ∃ r ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] r ∧ r ⊆ t

Tactic:
⟨closure w, mem_of_superset w_in subset_closure, isClosed_closure, ?_⟩

Premises used: subset_closure, closure, And.intro, Exists.intro, isClosed_closure, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
refine : closure[instTopologicalSpaceProd] w ⊆ t
⊢ ∃ r ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] r ∧ r ⊆ t

Tactic:
refine ⟨closure w, mem_of_superset w_in subset_closure, isClosed_closure, ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ closure[instTopologicalSpaceProd] w ⊆ t

Tactic:
Subset.trans ?_ r

Premises used: Set.Subset.trans
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
refine : closure[instTopologicalSpaceProd] w ⊆ w ○ w ○ w
⊢ closure[instTopologicalSpaceProd] w ⊆ t

Tactic:
refine Subset.trans ?_ r

Premises used: Set.Subset.trans
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
rw :
  ⋂ (V : Set (α × α)),
      ⋂ (_ : Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} V), V ○ w ○ V ⊆
    w ○ w ○ w
⊢ closure[instTopologicalSpaceProd] w ⊆ w ○ w ○ w

Tactic:
rw [closure_eq_uniformity]

Premises used: closure_eq_uniformity
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
h₁ :
  ⋂ (_ : Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} w), w ○ w ○ w ⊆ w ○ w ○ w
i : Set (α × α)
⊢ ⋂ (V : Set (α × α)),
      ⋂ (_ : Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} V), V ○ w ○ V ⊆
    w ○ w ○ w

Tactic:
apply iInter_subset_of_subset

Premises used: Set.iInter_subset_of_subset
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} w

Tactic:
⟨w_in, w_symm⟩

Premises used: Set.Mem, setOf, And.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} w

Tactic:
exact ⟨w_in, w_symm⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ 𝓤 α = (𝓤 α).lift' closure[instTopologicalSpaceProd]

Tactic:
Eq.symm <| uniformity_hasBasis_closed.lift'_closure_eq_self fun _ => And.right

Premises used: uniformity_hasBasis_closed, Filter.HasBasis.lift'_closure_eq_self, And.right, Eq.symm
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
U : ι → SetRel α α
h : (𝓤 α).HasBasis p U
⊢ (𝓤 α).HasBasis p fun (i : ι) ↦ closure[instTopologicalSpaceProd] (U i)

Tactic:
(@uniformity_eq_uniformity_closure α _).symm ▸ h.lift'_closure

Premises used: uniformity_eq_uniformity_closure, Eq.rec, Eq.symm, Filter.HasBasis.lift'_closure
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
⊢ (𝓤 α).HasBasis (fun (V : SetRel α α) ↦ V ∈ 𝓤 α) closure[instTopologicalSpaceProd]

Tactic:
(𝓤 α).basis_sets.uniformity_closure

Premises used: uniformity, Filter.basis_sets, Filter.HasBasis.uniformity_closure
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
t : SetRel α α
x x_1 : Set (α × α)
hV : x ⊆ x_1
⊢ x ○ t ○ x ⊆ x_1 ○ t ○ x_1

Tactic:
gcongr
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
t : SetRel α α
⊢ Eq.{ua + 1} (α := Set (α × α)) (⋂ V ∈ 𝓤 α, V ○ t ○ V) (⋂ V ∈ 𝓤 α, V ○ (t ○ V))

Tactic:
simp [SetRel.comp_assoc]

Premises used: SetRel.comp_assoc
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
let : ∀ (s : Set (α × α)) (hs : s ∈ 𝓤 α) (hs_comp : s ○ (s ○ s) ⊆ d), 𝓤 α ≤ (𝓟 ∘ interior) d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
let :
  ∀ (t : SetRel α α) (ht : IsOpen[instTopologicalSpaceProd] t) (hst : s ⊆ t)
    (ht_comp : t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}), 𝓤 α ≤ (𝓟 ∘ interior) d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
⊢ s ⊆ interior d

Tactic:
have : s ⊆ interior d :=
        calc
          s ⊆ t := hst
          _ ⊆ interior d :=
            ht.subset_interior_iff.mpr fun x (hx : x ∈ t) =>
              let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx
              hs_comp ⟨x, h₁, y, h₂, h₃⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this : s ⊆ interior d
⊢ ∀ a ∈ s, a ∈ interior d

Tactic:
this

Premises used: Set.Subset
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this : s ⊆ interior d
h : ∀ (a : α × α), Membership.mem (γ := Set (α × α)) {x : α × α | x ∈ s → x ∈ interior d} a
h₁ : ∀ a ∈ s, a ∈ interior d
⊢ interior d ∈ 𝓤 α

Tactic:
filter_upwards [hs] using this
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this : s ⊆ interior d
⊢ interior d ∈ 𝓤 α

Tactic:
have : interior d ∈ 𝓤 α := by filter_upwards [hs] using this
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this_1 : s ⊆ interior d
this : interior d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
simp [this]
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
rw : interior s ∈ (𝓤 α).lift' interior
⊢ interior s ∈ 𝓤 α

Tactic:
rw [uniformity_eq_uniformity_interior]

Premises used: uniformity_eq_uniformity_interior
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ interior s ∈ (𝓤 α).lift' interior

Tactic:
mem_lift' hs

Premises used: Filter.mem_lift'
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ interior s ∈ (𝓤 α).lift' interior

Tactic:
exact mem_lift' hs

Premises used: Filter.mem_lift'
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
h : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] t ∧ t ⊆ s

Tactic:
let ⟨t, ⟨ht_mem, htc⟩, hts⟩ := uniformity_hasBasis_closed.mem_iff.1 h
  ⟨t, ht_mem, htc, hts⟩

Premises used: uniformity_hasBasis_closed, Filter.HasBasis.mem_iff, uniformity, _private.0.mem_uniformity_isClosed.match_1, Membership.mem, Exists, HasSubset.Subset, IsClosed, And, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
rw : (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
⊢ IsOpen[inst.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s

Tactic:
rw [isOpen_iff_ball_subset]

Premises used: isOpen_iff_ball_subset
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
mp : (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
mpr : (∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s) → ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
⊢ (∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
x : α
hx : x ∈ s
mp :
  ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hV' : ball x V ⊆ s), ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s

Tactic:
obtain ⟨V, hV, hV'⟩ := h x hx
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s

Tactic:
⟨interior V, interior_mem_uniformity hV, isOpen_interior,
        (ball_mono interior_subset x).trans hV'⟩

Premises used: interior_subset, isOpen_interior, UniformSpace.ball_mono, HasSubset.Subset.trans, And.intro, interior, Exists.intro, interior_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s

Tactic:
exact
      ⟨interior V, interior_mem_uniformity hV, isOpen_interior,
        (ball_mono interior_subset x).trans hV'⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
mpr : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hV' : ball x V ⊆ s), ∃ V ∈ 𝓤 α, ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
obtain ⟨V, hV, -, hV'⟩ := h x hx
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
⟨V, hV, hV'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
h : ∀ x ∈ s, ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ball x V ⊆ s
x : α
hx : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hV' : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
exact ⟨V, hV, hV'⟩
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : SetRel α α
⊢ closure[inst.toTopologicalSpace] (ball x V) ⊆ ball x (closure[instTopologicalSpaceProd] V)

Tactic:
(Continuous.prodMk_right x).closure_preimage_subset V

Premises used: Continuous.prodMk_right, UniformSpace.ball, Continuous.closure_preimage_subset
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
⊢ Eq.{ua + 1} (α := Set α) (⋃ x ∈ s, ball x U) univ

Tactic:
iUnion₂_eq_univ_iff.2 fun y => ?_

Premises used: Iff.mpr, Set.iUnion₂_eq_univ_iff
-- Module: Mathlib.Topology.UniformSpace.Basic
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
refine : ∀ (y : α), ∃ (i : α) (_ : i ∈ s), y ∈ ball i U
⊢ Eq.{ua + 1} (α := Set α) (⋃ x ∈ s, ball x U) univ

Tactic:
refine iUnion₂_eq_univ_iff.2 fun y => ?_

Premises used: Iff.mpr, Set.iUnion₂_eq_univ_iff