awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
⊢ Eq (α := Set (SeparationQuotient γ)) (range ((SeparationQuotient.mk ∘ ⋯.extend f) ∘ i))
    (range (SeparationQuotient.mk ∘ f))
have apply : Eq (α := α → SeparationQuotient γ) ((SeparationQuotient.mk ∘ sorry.extend f) ∘ i) (SeparationQuotient.mk ∘ f)
Tactic: apply congrArg range
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
⊢ Eq (α := α → SeparationQuotient γ) ((SeparationQuotient.mk ∘ ⋯.extend f) ∘ i) (SeparationQuotient.mk ∘ f)
have h₁ : ∀ (x : α), Eq (α := SeparationQuotient γ) (((SeparationQuotient.mk ∘ sorry.extend f) ∘ i) x) ((SeparationQuotient.mk ∘ f) x)
Tactic: funext x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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
⊢ IsUniformInducing (hid.extend f)
have hrr : Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
  (closure (range (SeparationQuotient.mk ∘ f)))
Tactic: have hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆
      closure (range (SeparationQuotient.mk ∘ f)) := by
    refine ((SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
      h.uniformContinuous).continuous).range_subset_closure_image_dense hid.dense).trans
      (closure_mono (subset_of_eq ?_))
    rw [← range_comp]
    apply congrArg range
    funext x
    simpa using (hid.inseparable_extend h.uniformContinuous.continuous.continuousAt)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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_1 : 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)))
this :
  Subtype.val (p := fun (x : SeparationQuotient γ) ↦ x ∈ closure (range sf)) ∘ fwd =
    SeparationQuotient.mk ∘ hid.extend f
⊢ IsUniformInducing (hid.extend f)
have rw : IsUniformInducing (Subtype.val (p := fun (x : SeparationQuotient γ) ↦ x ∈ closure (range sf)) ∘ fwd)
Tactic: rw [← SeparationQuotient.isUniformInducing_mk.of_comp_iff, ← this]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)))
⊢ IsUniformInducing (hid.extend f)
have suffices : Subtype.val (p := fun (x : SeparationQuotient γ) ↦ x ∈ closure (range sf)) ∘ fwd = SeparationQuotient.mk ∘ 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
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)))
⊢ Subtype.val (p := fun (x : SeparationQuotient γ) ↦ x ∈ closure (range sf)) ∘ fwd =
    SeparationQuotient.mk ∘ hid.extend f
have rw : fwd =
  inclusion (s := range (SeparationQuotient.mk ∘ hid.extend f)) (t := closure (range (SeparationQuotient.mk ∘ f))) hrr ∘
    rangeFactorization (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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
have 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
Tactic: refine hid.extend_unique ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
⊢ fwd =
    inclusion (s := range (SeparationQuotient.mk ∘ hid.extend f)) (t := closure (range (SeparationQuotient.mk ∘ f)))
        hrr ∘
      rangeFactorization (SeparationQuotient.mk ∘ hid.extend f)
have 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))
Tactic: refine hid.extend_unique ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (goal)
Goal:
X : Type u_1
inst : UniformSpace X
c u : Set X
IsThickeningcu : IsThickening c u
⊢ ∃ (v : Set X), IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ IsThickening c v ∧ IsThickening (closure v) u
have 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
Tactic: obtain ⟨x, uc, s, huc, ucu, rfl, hn, hs⟩ := IsThickeningcu
Cleared hypotheses: c, IsThickeningcu
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (goal)
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
⊢ ∃ (v : Set X),
    IsOpen v ∧
      closure (ball x uc) ⊆ v ∧ closure v ⊆ u ∧ IsThickening (closure (ball x uc)) v ∧ IsThickening (closure v) u
have 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
Tactic: obtain ⟨(ds : SetRel X X), hdsu, hdso, -, hdsd⟩ := comp_open_symm_mem_uniformity_sets hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (hypothesis)
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
⊢ ∃ (v : Set X),
    IsOpen v ∧
      closure (ball x uc) ⊆ v ∧ closure v ⊆ u ∧ IsThickening (closure (ball x uc)) v ∧ IsThickening (closure v) u
have ho : IsOpen (ds ○ uc ○ ds)
Tactic: have ho : IsOpen (ds ○ uc ○ ds) := (hdso.relComp huc).relComp hdso
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (hypothesis)
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)
⊢ ∃ (v : Set X),
    IsOpen v ∧
      closure (ball x uc) ⊆ v ∧ closure v ⊆ u ∧ IsThickening (closure (ball x uc)) v ∧ IsThickening (closure v) u
have hsub : 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
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (hypothesis)
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
⊢ ∃ (v : Set X),
    IsOpen v ∧
      closure (ball x uc) ⊆ v ∧ closure v ⊆ u ∧ IsThickening (closure (ball x uc)) v ∧ IsThickening (closure v) u
have hsub₁ : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
Tactic: replace hsub := (ball_mono hsub x).trans hn
Cleared hypotheses: hsub
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (hypothesis)
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
⊢ ∃ (v : Set X),
    IsOpen v ∧
      closure (ball x uc) ⊆ v ∧ closure v ⊆ u ∧ IsThickening (closure (ball x uc)) v ∧ IsThickening (closure v) u
have this : ds.IsRefl
Tactic: have : ds.IsRefl := id_subset_iff.1 (refl_le_uniformity hdsu)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (goal)
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
have refine_1 : closure (ball x uc) ⊆ ball x (ds ○ uc ○ ds)
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⟩⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (goal)
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)
⊢ ∃ (v : Set X),
    IsOpen v ∧
      closure (ball x uc) ⊆ v ∧ closure v ⊆ u ∧ IsThickening (closure (ball x uc)) v ∧ IsThickening (closure v) u
have refine_2 : closure (ball x (ds ○ uc ○ ds)) ⊆ ball x (ds ○ (ds ○ uc ○ ds) ○ ds)
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⟩⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (goal)
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)
have refine_1 : closure uc ⊆ ds ○ uc ○ ds
Tactic: refine closure_ball_subset.trans (ball_mono ?_ x)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (goal)
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 uc ⊆ ds ○ uc ○ ds
have refine_1 : ⋂ d ∈ 𝓤 X, d ○ (uc ○ d) ⊆ ds ○ uc ○ ds
Tactic: rw [closure_eq_inter_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (goal)
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)
have refine_2 : closure (ds ○ uc ○ ds) ⊆ ds ○ (ds ○ uc ○ ds) ○ ds
Tactic: refine closure_ball_subset.trans (ball_mono ?_ x)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (goal)
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 (ds ○ uc ○ ds) ⊆ ds ○ (ds ○ uc ○ ds) ○ ds
have refine_2 : ⋂ d ∈ 𝓤 X, d ○ (ds ○ uc ○ ds ○ d) ⊆ ds ○ (ds ○ uc ○ ds) ○ ds
Tactic: rw [closure_eq_inter_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (goal)
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
⊢ closure (interior u3) ⊆ O
have simp_rw : ⋂ d ∈ 𝓤 X, d ○ interior u3 ○ d ⊆ O
Tactic: simp_rw [closure_eq_inter_uniformity, ← comp_assoc]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Uniformizable (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
h : ∃ (u : UniformSpace X), toTopologicalSpace = t
⊢ CompletelyRegularSpace X
have obtain : ∀ (u : UniformSpace X), CompletelyRegularSpace X
Tactic: obtain ⟨u, rfl⟩ := h
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
x : ℝ
⊢ σ (projIcc 0 1 ⋯ x) = projIcc 0 1 ⋯ (1 - x)
have a : (↑(σ (projIcc 0 1 sorry x)) : ℝ) = (↑(projIcc 0 1 sorry (1 - x)) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
x : ℝ
⊢ (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)
have a : ∀ (h₀ : x ≤ 0), (↑(σ (projIcc 0 1 sorry x)) : ℝ) = (↑(projIcc 0 1 sorry (1 - x)) : ℝ)
Tactic: rcases le_total x 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
x : ℝ
a : ∀ (h₀ : x ≤ 0), (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)
⊢ (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)
have a₁ : ∀ (h₀ : 0 ≤ x), (↑(σ (projIcc 0 1 sorry x)) : ℝ) = (↑(projIcc 0 1 sorry (1 - x)) : ℝ)
Tactic: rcases le_total x 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
x : ℝ
h₀ : 0 ≤ x
⊢ (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)
have a : ∀ (h₁ : x ≤ 1), (↑(σ (projIcc 0 1 sorry x)) : ℝ) = (↑(projIcc 0 1 sorry (1 - x)) : ℝ)
Tactic: rcases le_total x 1 with h₁ | h₁
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
x : ℝ
h₀ : 0 ≤ x
a : ∀ (h₁ : x ≤ 1), (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)
⊢ (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)
have a₁ : ∀ (h₁ : 1 ≤ x), (↑(σ (projIcc 0 1 sorry x)) : ℝ) = (↑(projIcc 0 1 sorry (1 - x)) : ℝ)
Tactic: rcases le_total x 1 with h₁ | h₁
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
x : ℝ
h₀ : 0 ≤ x
h₁ : x ≤ 1
⊢ (↑(σ (projIcc 0 1 ⋯ x)) : ℝ) = (↑(projIcc 0 1 ⋯ (1 - x)) : ℝ)
have a : ∀ (x : { x : ℝ // x ∈ I }) (h₀ : 0 ≤ (↑x : ℝ)) (h₁ : (↑x : ℝ) ≤ 1),
  (↑(σ (projIcc 0 1 sorry (↑x : ℝ))) : ℝ) = (↑(projIcc 0 1 sorry (1 - (↑x : ℝ))) : ℝ)
Tactic: lift x to I using ⟨h₀, h₁⟩
Cleared hypotheses: x, h₀, h₁
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : (↑I : Type)
⊢ 1 / 2 ≤ (↑(σ t) : ℝ) ↔ (↑t : ℝ) ≤ 1 / 2
have rw : 1 / 2 ≤ 1 - (↑t : ℝ) ↔ (↑t : ℝ) ≤ 1 / 2
Tactic: rw [coe_symm_eq, le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le, sub_half]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : (↑I : Type)
rw : 1 / 2 ≤ 1 - (↑t : ℝ) ↔ (↑t : ℝ) ≤ 1 / 2
⊢ 1 / 2 ≤ (↑(σ t) : ℝ) ↔ (↑t : ℝ) ≤ 1 / 2
have rw₁ : 1 / 2 + (↑t : ℝ) ≤ 1 ↔ (↑t : ℝ) ≤ 1 / 2
Tactic: rw [coe_symm_eq, le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le, sub_half]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : (↑I : Type)
rw : 1 / 2 ≤ 1 - (↑t : ℝ) ↔ (↑t : ℝ) ≤ 1 / 2
rw₁ : 1 / 2 + (↑t : ℝ) ≤ 1 ↔ (↑t : ℝ) ≤ 1 / 2
⊢ 1 / 2 ≤ (↑(σ t) : ℝ) ↔ (↑t : ℝ) ≤ 1 / 2
have rw₂ : (↑t : ℝ) + 1 / 2 ≤ 1 ↔ (↑t : ℝ) ≤ 1 / 2
Tactic: rw [coe_symm_eq, le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le, sub_half]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : (↑I : Type)
rw : 1 / 2 ≤ 1 - (↑t : ℝ) ↔ (↑t : ℝ) ≤ 1 / 2
rw₁ : 1 / 2 + (↑t : ℝ) ≤ 1 ↔ (↑t : ℝ) ≤ 1 / 2
rw₂ : (↑t : ℝ) + 1 / 2 ≤ 1 ↔ (↑t : ℝ) ≤ 1 / 2
⊢ 1 / 2 ≤ (↑(σ t) : ℝ) ↔ (↑t : ℝ) ≤ 1 / 2
have rw₃ : (↑t : ℝ) ≤ 1 - 1 / 2 ↔ (↑t : ℝ) ≤ 1 / 2
Tactic: rw [coe_symm_eq, le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le, sub_half]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
t : (↑I : Type)
rw : 1 / 2 ≤ 1 - (↑t : ℝ) ↔ (↑t : ℝ) ≤ 1 / 2
rw₁ : 1 / 2 + (↑t : ℝ) ≤ 1 ↔ (↑t : ℝ) ≤ 1 / 2
rw₂ : (↑t : ℝ) + 1 / 2 ≤ 1 ↔ (↑t : ℝ) ≤ 1 / 2
rw₃ : (↑t : ℝ) ≤ 1 - 1 / 2 ↔ (↑t : ℝ) ≤ 1 / 2
⊢ 1 / 2 ≤ (↑(σ t) : ℝ) ↔ (↑t : ℝ) ≤ 1 / 2
have rw₄ : (↑t : ℝ) ≤ 1 / 2 ↔ (↑t : ℝ) ≤ 1 / 2
Tactic: rw [coe_symm_eq, le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le, sub_half]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i : (↑I : Type)
⊢ σ i = 1 ↔ i = 0
have rw : σ i = σ 0 ↔ i = 0
Tactic: rw [← symm_zero, symm_inj]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
i : (↑I : Type)
rw : σ i = σ 0 ↔ i = 0
⊢ σ i = 1 ↔ i = 0
have rw₁ : i = 0 ↔ i = 0
Tactic: rw [← symm_zero, symm_inj]