awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr :
  Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))
suffices :
  Subtype.val (p := fun (x : SeparationQuotient γ) ↦ x ∈ closure (range sf)) ∘ fwd =
    SeparationQuotient.mk ∘ hid.extend f
⊢ IsUniformInducing (hid.extend f)

Tactic:
suffices Subtype.val ∘ fwd = SeparationQuotient.mk ∘ hid.extend f by
    rw [← SeparationQuotient.isUniformInducing_mk.of_comp_iff, ← this]
    exact (isUniformInducing_val _).comp hfu
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr :
  Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))
rw :
  fwd =
    inclusion (s := range (SeparationQuotient.mk ∘ hid.extend f)) (t := closure (range (SeparationQuotient.mk ∘ f)))
        hrr ∘
      rangeFactorization (SeparationQuotient.mk ∘ hid.extend f)
⊢ Subtype.val (p := fun (x : SeparationQuotient γ) ↦ x ∈ closure (range sf)) ∘ fwd =
    SeparationQuotient.mk ∘ hid.extend f

Tactic:
rw [← coe_comp_rangeFactorization (SeparationQuotient.mk ∘ hid.extend f),
    ← val_comp_inclusion hrr, Function.comp_assoc, Subtype.val_injective.comp_left.eq_iff]

Premises used: Set.val_comp_inclusion, Subtype.val_injective, Function.Injective.eq_iff, Function.comp, Set.coe_comp_rangeFactorization, SeparationQuotient.mk, Function.Injective.comp_left, IsDenseInducing.extend, Function.comp_assoc
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr :
  Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))
⊢ fwd =
    inclusion (s := range (SeparationQuotient.mk ∘ hid.extend f)) (t := closure (range (SeparationQuotient.mk ∘ f)))
        hrr ∘
      rangeFactorization (SeparationQuotient.mk ∘ hid.extend f)

Tactic:
hid.extend_unique ?_ ?_

Premises used: IsDenseInducing.extend_unique
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr :
  Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))
refine_1 :
  ∀ (x : α),
    (inclusion (s := range (SeparationQuotient.mk ∘ hid.extend f)) (t := closure (range (SeparationQuotient.mk ∘ f)))
            hrr ∘
          rangeFactorization (SeparationQuotient.mk ∘ hid.extend f))
        (i x) =
      ff x
refine_2 :
  Continuous[inst_1.toTopologicalSpace, _]
    (inclusion (s := range (SeparationQuotient.mk ∘ hid.extend f)) (t := closure (range (SeparationQuotient.mk ∘ f)))
        hrr ∘
      rangeFactorization (SeparationQuotient.mk ∘ hid.extend f))
⊢ fwd =
    inclusion (s := range (SeparationQuotient.mk ∘ hid.extend f)) (t := closure (range (SeparationQuotient.mk ∘ f)))
        hrr ∘
      rangeFactorization (SeparationQuotient.mk ∘ hid.extend f)

Tactic:
refine hid.extend_unique ?_ ?_

Premises used: IsDenseInducing.extend_unique
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr :
  Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))
⊢ ∀ (x : α),
    (inclusion (s := range (SeparationQuotient.mk ∘ hid.extend f)) (t := closure (range (SeparationQuotient.mk ∘ f)))
            hrr ∘
          rangeFactorization (SeparationQuotient.mk ∘ hid.extend f))
        (i x) =
      ff x

Tactic:
simp [ff, hid.inseparable_extend h.uniformContinuous.continuous.continuousAt, sf]

Premises used: UniformContinuous.continuous, Continuous.continuousAt, IsDenseInducing.inseparable_extend, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr :
  Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))
⊢ Continuous[inst_1.toTopologicalSpace, _]
    (inclusion (s := range (SeparationQuotient.mk ∘ hid.extend f)) (t := closure (range (SeparationQuotient.mk ∘ f)))
        hrr ∘
      rangeFactorization (SeparationQuotient.mk ∘ hid.extend f))

Tactic:
(continuous_inclusion hrr).comp
      (SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
        h.uniformContinuous).continuous).rangeFactorization

Premises used: SeparationQuotient.continuous_mk, Set.Mem, uniformContinuous_uniformly_extend, Continuous.comp, Continuous.rangeFactorization, UniformContinuous.continuous, IsDenseInducing.dense, continuous_inclusion, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr :
  Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))
⊢ Continuous[inst_1.toTopologicalSpace, _]
    (inclusion (s := range (SeparationQuotient.mk ∘ hid.extend f)) (t := closure (range (SeparationQuotient.mk ∘ f)))
        hrr ∘
      rangeFactorization (SeparationQuotient.mk ∘ hid.extend f))

Tactic:
exact (continuous_inclusion hrr).comp
      (SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
        h.uniformContinuous).continuous).rangeFactorization

Premises used: SeparationQuotient.continuous_mk, uniformContinuous_uniformly_extend, Continuous.comp, Continuous.rangeFactorization, UniformContinuous.continuous, IsDenseInducing.dense, continuous_inclusion, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
c u : Set X
IsThickeningcu : IsThickening c u
obtain :
  ∀ (x : X) (uc s : SetRel X X) (huc : IsOpen uc) (ucu : uc ∈ 𝓤 X) (hn : ball x (s ○ uc ○ s) ⊆ u) (hs : s ∈ 𝓤 X),
    ∃ (v : Set X),
      IsOpen v ∧
        closure (ball x uc) ⊆ v ∧ closure v ⊆ u ∧ IsThickening (closure (ball x uc)) v ∧ IsThickening (closure v) u
⊢ ∃ (v : Set X), IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ IsThickening c v ∧ IsThickening (closure v) u

Tactic:
obtain ⟨x, uc, s, huc, ucu, rfl, hn, hs⟩ := IsThickeningcu

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
obtain :
  ∀ (ds : SetRel X X) (hdsu : ds ∈ 𝓤 X) (hdso : IsOpen ds) (hdsd : ds ○ ds ⊆ s),
    ∃ (v : Set X),
      IsOpen v ∧
        closure (ball x uc) ⊆ v ∧ closure v ⊆ u ∧ IsThickening (closure (ball x uc)) v ∧ IsThickening (closure v) u
⊢ ∃ (v : Set X),
    IsOpen v ∧
      closure (ball x uc) ⊆ v ∧ closure v ⊆ u ∧ IsThickening (closure (ball x uc)) v ∧ IsThickening (closure v) u

Tactic:
obtain ⟨(ds : SetRel X X), hdsu, hdso, -, hdsd⟩ := comp_open_symm_mem_uniformity_sets hs

Premises used: SetRel, comp_open_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
⊢ IsOpen (ds ○ uc ○ ds)

Tactic:
have ho : IsOpen (ds ○ uc ○ ds) := (hdso.relComp huc).relComp hdso
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
⊢ ds ○ (ds ○ uc ○ ds) ○ ds = ds ○ ds ○ uc ○ (ds ○ ds)

Tactic:
simp [comp_assoc]

Premises used: SetRel.comp_assoc
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
⊢ ds ○ (ds ○ uc ○ ds) ○ ds ⊆ s ○ uc ○ s

Tactic:
have hsub := calc ds ○ (ds ○ uc ○ ds) ○ ds
    _ = (ds ○ ds) ○ uc ○ (ds ○ ds) := by simp [comp_assoc]
    _ ⊆ s ○ uc ○ s := comp_subset_comp (comp_subset_comp_left hdsd) hdsd
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ds ○ (ds ○ uc ○ ds) ○ ds ⊆ s ○ uc ○ s
⊢ ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u

Tactic:
replace hsub := (ball_mono hsub x).trans hn
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
⊢ ds.IsRefl

Tactic:
have : ds.IsRefl := id_subset_iff.1 (refl_le_uniformity hdsu)
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ ∃ (v : Set X),
    IsOpen v ∧
      closure (ball x uc) ⊆ v ∧ closure v ⊆ u ∧ IsThickening (closure (ball x uc)) v ∧ IsThickening (closure v) u

Tactic:
⟨ball x (ds ○ uc ○ ds), isOpen_ball x ho, ?_, subset_trans ?_ hsub,
      ⟨x, uc, ds, huc, ucu, rfl, subset_rfl, hdsu⟩,
      ⟨x, ds ○ uc ○ ds, ds, ho, mem_of_superset ucu (right_subset_comp.trans left_subset_comp),
        rfl, hsub, hdsu⟩⟩

Premises used: subset_trans, SetRel.left_subset_comp, UniformSpace.isOpen_ball, SetRel.right_subset_comp, HasSubset.Subset.trans, UniformSpace.ball, SetRel.comp, And.intro, Exists.intro, subset_rfl, rfl, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
refine_1 : closure (ball x uc) ⊆ ball x (ds ○ uc ○ ds)
refine_2 : closure (ball x (ds ○ uc ○ ds)) ⊆ ball x (ds ○ (ds ○ uc ○ ds) ○ ds)
⊢ ∃ (v : Set X),
    IsOpen v ∧
      closure (ball x uc) ⊆ v ∧ closure v ⊆ u ∧ IsThickening (closure (ball x uc)) v ∧ IsThickening (closure v) u

Tactic:
refine ⟨ball x (ds ○ uc ○ ds), isOpen_ball x ho, ?_, subset_trans ?_ hsub,
      ⟨x, uc, ds, huc, ucu, rfl, subset_rfl, hdsu⟩,
      ⟨x, ds ○ uc ○ ds, ds, ho, mem_of_superset ucu (right_subset_comp.trans left_subset_comp),
        rfl, hsub, hdsu⟩⟩
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ closure (ball x uc) ⊆ ball x (ds ○ uc ○ ds)

Tactic:
closure_ball_subset.trans (ball_mono ?_ x)

Premises used: UniformSpace.ball_mono, HasSubset.Subset.trans, closure_ball_subset
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
refine_1 : closure uc ⊆ ds ○ uc ○ ds
⊢ closure (ball x uc) ⊆ ball x (ds ○ uc ○ ds)

Tactic:
refine closure_ball_subset.trans (ball_mono ?_ x)

Premises used: UniformSpace.ball_mono, HasSubset.Subset.trans, closure_ball_subset
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
refine_1 : ⋂ d ∈ 𝓤 X, d ○ (uc ○ d) ⊆ ds ○ uc ○ ds
⊢ closure uc ⊆ ds ○ uc ○ ds

Tactic:
rw [closure_eq_inter_uniformity]

Premises used: closure_eq_inter_uniformity
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ ds ○ (uc ○ ds) ⊆ ds ○ uc ○ ds

Tactic:
simp [comp_assoc]

Premises used: SetRel.comp_assoc
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ ⋂ d ∈ 𝓤 X, d ○ (uc ○ d) ⊆ ds ○ uc ○ ds

Tactic:
exact iInter₂_subset_of_subset ds hdsu (by simp [comp_assoc])

Premises used: Set.iInter₂_subset_of_subset
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ closure (ball x (ds ○ uc ○ ds)) ⊆ ball x (ds ○ (ds ○ uc ○ ds) ○ ds)

Tactic:
closure_ball_subset.trans (ball_mono ?_ x)

Premises used: UniformSpace.ball_mono, HasSubset.Subset.trans, closure_ball_subset
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
refine_2 : closure (ds ○ uc ○ ds) ⊆ ds ○ (ds ○ uc ○ ds) ○ ds
⊢ closure (ball x (ds ○ uc ○ ds)) ⊆ ball x (ds ○ (ds ○ uc ○ ds) ○ ds)

Tactic:
refine closure_ball_subset.trans (ball_mono ?_ x)

Premises used: UniformSpace.ball_mono, HasSubset.Subset.trans, closure_ball_subset
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
refine_2 : ⋂ d ∈ 𝓤 X, d ○ (ds ○ uc ○ ds ○ d) ⊆ ds ○ (ds ○ uc ○ ds) ○ ds
⊢ closure (ds ○ uc ○ ds) ⊆ ds ○ (ds ○ uc ○ ds) ○ ds

Tactic:
rw [closure_eq_inter_uniformity]

Premises used: closure_eq_inter_uniformity
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ ds ○ (ds ○ uc ○ ds ○ ds) ⊆ ds ○ (ds ○ uc ○ ds) ○ ds

Tactic:
simp [comp_assoc]

Premises used: SetRel.comp_assoc
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ ⋂ d ∈ 𝓤 X, d ○ (ds ○ uc ○ ds ○ d) ⊆ ds ○ (ds ○ uc ○ ds) ○ ds

Tactic:
exact iInter₂_subset_of_subset ds hdsu (by simp [comp_assoc])

Premises used: Set.iInter₂_subset_of_subset
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
x : X
K : Set X
hK : IsClosed K
hx : x ∉ K
O : Set (X × X)
hOu : O ∈ 𝓤 X
hOo : IsOpen O
hbO : ball x O ⊆ Kᶜ
u3 : SetRel X X
hu3u : u3 ∈ 𝓤 X
left : u3.IsSymm
hu3O_1 : u3 ○ u3 ○ u3 ⊆ O
hu3O : u3 ○ interior u3 ○ u3 ⊆ O
simp_rw : ⋂ d ∈ 𝓤 X, d ○ interior u3 ○ d ⊆ O
⊢ closure (interior u3) ⊆ O

Tactic:
simp_rw [closure_eq_inter_uniformity, ← comp_assoc]

Premises used: closure_eq_inter_uniformity, SetRel.comp_assoc
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
x : X
K : Set X
hK : IsClosed K
hx : x ∉ K
O : Set (X × X)
hOu : O ∈ 𝓤 X
hOo : IsOpen O
hbO : ball x O ⊆ Kᶜ
u3 : SetRel X X
hu3u : u3 ∈ 𝓤 X
left : u3.IsSymm
hu3O_1 : u3 ○ u3 ○ u3 ⊆ O
hu3O : u3 ○ interior u3 ○ u3 ⊆ O
⊢ ⋂ d ∈ 𝓤 X, d ○ interior u3 ○ d ⊆ O

Tactic:
(iInter₂_subset u3 hu3u).trans hu3O

Premises used: Set.iInter₂_subset, HasSubset.Subset.trans
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
inst : UniformSpace X
x : X
K : Set X
hK : IsClosed K
hx : x ∉ K
O : Set (X × X)
hOu : O ∈ 𝓤 X
hOo : IsOpen O
hbO : ball x O ⊆ Kᶜ
u3 : SetRel X X
hu3u : u3 ∈ 𝓤 X
left : u3.IsSymm
hu3O_1 : u3 ○ u3 ○ u3 ⊆ O
hu3O : u3 ○ interior u3 ○ u3 ⊆ O
⊢ ⋂ d ∈ 𝓤 X, d ○ interior u3 ○ d ⊆ O

Tactic:
exact (iInter₂_subset u3 hu3u).trans hu3O

Premises used: Set.iInter₂_subset, HasSubset.Subset.trans
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
t : TopologicalSpace X
h : ∃ (u : UniformSpace X), toTopologicalSpace = t
obtain : ∀ (u : UniformSpace X), CompletelyRegularSpace X
⊢ CompletelyRegularSpace X

Tactic:
obtain ⟨u, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Uniformizable
Goal:
X : Type u_1
u : UniformSpace X
⊢ CompletelyRegularSpace X

Tactic:
infer_instance