awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
inst_2 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
f : γ → α →ᵤ[𝔖] β
K : ℝ≥0
mp :
  (∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y) →
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y
⊢ (∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y) ↔
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y
have mpr : (∀ (c : α),
    ∀ x ∈ 𝔖,
      c ∈ x →
        ∀ (x y : γ),
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
            (↑K : ℝ≥0∞) * edist x y) →
  ∀ (x y : γ) (x_1 : α),
    ∀ x_2 ∈ 𝔖,
      x_1 ∈ x_2 →
        edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
            ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
          (↑K : ℝ≥0∞) * edist x y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
inst_2 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
f : γ → α →ᵤ[𝔖] β
K : ℝ≥0
s : Set γ
⊢ LipschitzOnWith K f s ↔
    ∀ c ∈ ⋃₀ 𝔖, LipschitzOnWith.{u_3, u_2} (β := β) K (fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c) s
have simp : (∀ (c : α),
    ∀ x ∈ 𝔖,
      c ∈ x →
        LipschitzWith.{u_3, u_2} (β := β) K fun (x : (↑s : Type u_3)) ↦
          (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f (↑x : γ)) c) ↔
  ∀ (c : α),
    ∀ x ∈ 𝔖,
      c ∈ x →
        LipschitzWith.{u_3, u_2} (α := (↑s : Type u_3)) (β := β) K
          (s.restrict (π := fun (a : γ) ↦ β) fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c)
Tactic: simp [lipschitzOnWith_iff_restrict, lipschitzWith_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
inst_2 : PseudoMetricSpace β
inst_3 : BoundedSpace β
f g : α →ᵤ[𝔖] β
⊢ edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ[𝔖] β) ↦
          (⨆ (x : (↑(⋃₀ 𝔖) : Type u_1)),
              dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β) :
            ℝ))
        f g)
have inl : IsEmpty.{u_1 + 1} (↑(⋃₀ 𝔖) : Type u_1) →
  edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ[𝔖] β) ↦
          (⨆ (x : (↑(⋃₀ 𝔖) : Type u_1)),
              dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β) :
            ℝ))
        f g)
Tactic: cases isEmpty_or_nonempty (⋃₀ 𝔖)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
inst_2 : PseudoMetricSpace β
inst_3 : BoundedSpace β
f g : α →ᵤ[𝔖] β
inl :
  IsEmpty.{u_1 + 1} (↑(⋃₀ 𝔖) : Type u_1) →
    edist f g =
      ENNReal.ofReal
        ((fun (f g : α →ᵤ[𝔖] β) ↦
            (⨆ (x : (↑(⋃₀ 𝔖) : Type u_1)),
                dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
                  ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β) :
              ℝ))
          f g)
⊢ edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ[𝔖] β) ↦
          (⨆ (x : (↑(⋃₀ 𝔖) : Type u_1)),
              dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β) :
            ℝ))
        f g)
have inr : Nonempty.{u_1 + 1} (↑(⋃₀ 𝔖) : Type u_1) →
  edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ[𝔖] β) ↦
          (⨆ (x : (↑(⋃₀ 𝔖) : Type u_1)),
              dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β) :
            ℝ))
        f g)
Tactic: cases isEmpty_or_nonempty (⋃₀ 𝔖)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
inst_2 : PseudoMetricSpace β
inst_3 : BoundedSpace β
f g : α →ᵤ[𝔖] β
h : Nonempty.{u_1 + 1} (↑(⋃₀ 𝔖) : Type u_1)
⊢ BddAbove (α := ℝ)
    (Set.range fun (x : (↑(⋃₀ 𝔖) : Type u_1)) ↦
      dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
        ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β))
have h : Membership.mem (γ := Set ℝ)
  (upperBounds
    (Set.range fun (x : (↑(⋃₀ 𝔖) : Type u_1)) ↦
      dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
        ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β)))
  (Metric.ediam.{u_2} (X := β) Set.univ).toReal
Tactic: use (Metric.ediam (.univ : Set β)).toReal
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
inst_2 : PseudoMetricSpace β
inst_3 : BoundedSpace β
f g : α →ᵤ[𝔖] β
h : Nonempty.{u_1 + 1} (↑(⋃₀ 𝔖) : Type u_1)
⊢ edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ[𝔖] β) ↦
          (⨆ (x : (↑(⋃₀ 𝔖) : Type u_1)),
              dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β) :
            ℝ))
        f g)
have this : BddAbove (α := ℝ)
  (Set.range fun (x : (↑(⋃₀ 𝔖) : Type u_1)) ↦
    dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
      ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β))
Tactic: have : BddAbove (.range fun x : ⋃₀ 𝔖 ↦ dist (toFun 𝔖 f x) (toFun 𝔖 g x)) := by
        use (Metric.ediam (.univ : Set β)).toReal
        simp +contextual [mem_upperBounds, eq_comm (a := dist _ _), ← edist_dist,
          ← ENNReal.ofReal_le_iff_le_toReal BoundedSpace.bounded_univ.ediam_ne_top,
          Metric.edist_le_ediam_of_mem]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
inst_2 : PseudoMetricSpace β
inst_3 : BoundedSpace β
f g : α →ᵤ[𝔖] β
h : Nonempty.{u_1 + 1} (↑(⋃₀ 𝔖) : Type u_1)
this :
  BddAbove (α := ℝ)
    (Set.range fun (x : (↑(⋃₀ 𝔖) : Type u_1)) ↦
      dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
        ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β))
⊢ edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ[𝔖] β) ↦
          (⨆ (x : (↑(⋃₀ 𝔖) : Type u_1)),
              dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β) :
            ℝ))
        f g)
have inr : ∀ (r : ℝ≥0),
  edist f g ≤ (↑r : ℝ≥0∞) ↔
    ENNReal.ofReal
        ((fun (f g : α →ᵤ[𝔖] β) ↦
            (⨆ (x : (↑(⋃₀ 𝔖) : Type u_1)),
                dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
                  ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β) :
              ℝ))
          f g) ≤
      (↑r : ℝ≥0∞)
Tactic: refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
inst_2 : PseudoMetricSpace β
inst_3 : BoundedSpace β
⊢ Bornology.IsBounded (α := α →ᵤ[𝔖] β) Set.univ
have h : Eq (α := Set (α →ᵤ[𝔖] β)) Set.univ
  (Set.image (α := α →ᵤ β)
    (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β) (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
    Set.univ)
Tactic: convert! lipschitzWith_one_ofFun_toFun (𝔖 := 𝔖) (β := β) |>.isBounded_image (.all Set.univ)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
inst_2 : PseudoMetricSpace β
inst_3 : BoundedSpace β
⊢ Eq (α := Set (α →ᵤ[𝔖] β)) Set.univ
    (Set.image (α := α →ᵤ β)
      (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β) (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
      Set.univ)
have h : ∀ (f : α →ᵤ[𝔖] β),
  Membership.mem (γ := Set (α →ᵤ[𝔖] β)) Set.univ f ↔
    Membership.mem (γ := Set (α →ᵤ[𝔖] β))
      (Set.image (α := α →ᵤ β)
        (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β) (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
        Set.univ)
      f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
inst_2 : PseudoMetricSpace β
inst_3 : BoundedSpace β
f : α →ᵤ[𝔖] β
⊢ Membership.mem (γ := Set (α →ᵤ[𝔖] β)) Set.univ f ↔
    Membership.mem (γ := Set (α →ᵤ[𝔖] β))
      (Set.image (α := α →ᵤ β)
        (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β) (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
        Set.univ)
      f
have h : ∃ (y : α →ᵤ β), (ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) ((UniformFun.toFun : (a : α →ᵤ β) → α → β) y) = f
Tactic: simp only [Set.mem_univ, Function.comp_apply, Set.image_univ, Set.mem_range, true_iff]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs_1 : IsSeparable s
u : Set X
hu : u.Countable
hs : s ⊆ closure[inst] u
this : Countable.{u_2 + 1} (↑u : Type u_2)
⊢ closure[inst] u ⊆
    closure[inst]
      (Set.image (α := (↑(closure[inst] u) : Type u_2)) (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] u))
        (range (inclusion (s := u) (t := closure[inst] u) ⋯)))
have rw : closure[inst] u ⊆
  closure[inst]
    (range (ι := (↑u : Type u_2))
      (Function.comp (β := (↑(closure[inst] u) : Type u_2)) (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] u))
        (inclusion (s := u) (t := closure[inst] u) sorry)))
Tactic: rw [← Set.range_comp, Set.val_comp_inclusion, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs_1 : IsSeparable s
u : Set X
hu : u.Countable
hs : s ⊆ closure[inst] u
this : Countable.{u_2 + 1} (↑u : Type u_2)
rw :
  closure[inst] u ⊆
    closure[inst]
      (range (ι := (↑u : Type u_2))
        (Function.comp (β := (↑(closure[inst] u) : Type u_2)) (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] u))
          (inclusion (s := u) (t := closure[inst] u) ⋯)))
⊢ closure[inst] u ⊆
    closure[inst]
      (Set.image (α := (↑(closure[inst] u) : Type u_2)) (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] u))
        (range (inclusion (s := u) (t := closure[inst] u) ⋯)))
have rw₁ : closure[inst] u ⊆ closure[inst] (range (ι := (↑u : Type u_2)) (Subtype.val (p := fun (x : X) ↦ x ∈ u)))
Tactic: rw [← Set.range_comp, Set.val_comp_inclusion, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs_1 : IsSeparable s
u : Set X
hu : u.Countable
hs : s ⊆ closure[inst] u
this : Countable.{u_2 + 1} (↑u : Type u_2)
rw :
  closure[inst] u ⊆
    closure[inst]
      (range (ι := (↑u : Type u_2))
        (Function.comp (β := (↑(closure[inst] u) : Type u_2)) (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] u))
          (inclusion (s := u) (t := closure[inst] u) ⋯)))
rw₁ : closure[inst] u ⊆ closure[inst] (range (ι := (↑u : Type u_2)) (Subtype.val (p := fun (x : X) ↦ x ∈ u)))
⊢ closure[inst] u ⊆
    closure[inst]
      (Set.image (α := (↑(closure[inst] u) : Type u_2)) (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] u))
        (range (inclusion (s := u) (t := closure[inst] u) ⋯)))
have rw₂ : closure[inst] u ⊆ closure[inst] u
Tactic: rw [← Set.range_comp, Set.val_comp_inclusion, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (hypothesis)
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this : UniformSpace X := pseudoMetrizableSpaceUniformity X
⊢ SecondCountableTopology X
have this₁ : (𝓤 X).IsCountablyGenerated
Tactic: have := pseudoMetrizableSpaceUniformity_countably_generated X
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
⊢ SecondCountableTopology X
have suffices : SeparableSpace X
Tactic: suffices _ : SeparableSpace X from secondCountable_of_separable X
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
⊢ SeparableSpace X
have obtain : ∀ (V : ℕ → SetRel X X) (hVb : (𝓤 X).HasAntitoneBasis V) (hVs : ∀ (n : ℕ), (V n).IsSymm), SeparableSpace X
Tactic: obtain ⟨V, hVb, hVs⟩ := has_seq_basis X
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
⊢ SeparableSpace X
have choose : ∀ (U : (n : ℕ) → Set X) (hUc : ∀ (n : ℕ), (U n).Countable)
  (hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ), SeparableSpace X
Tactic: choose U hUc hUu using fun n =>
    LindelofSpace.elim_nhds_subcover (fun x => ball x (V n))
      (fun x => ball_mem_nhds x (hVb.mem n))
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : (n : ℕ) → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ
⊢ SeparableSpace X
have refine : ∀ (x : X), x ∈ closure[inst_4] (iUnion U)
Tactic: refine ⟨Set.iUnion U, Set.countable_iUnion hUc, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : (n : ℕ) → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ
x : X
⊢ x ∈ closure[inst_4] (iUnion U)
have rw : ∀ (i : ℕ), True → ∃ x_1 ∈ V i, ∃ (a : X), (x, a) = x_1 ∧ a ∈ iUnion U
Tactic: rw [mem_closure_iff_frequently, nhds_eq_comap_uniformity, frequently_comap, hVb.frequently_iff]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : (n : ℕ) → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ
x : X
n : ℕ
h : True
⊢ ∃ x_1 ∈ V n, ∃ (a : X), (x, a) = x_1 ∧ a ∈ iUnion U
have obtain : ∀ (i : X) (hi : i ∈ U n) (hx : x ∈ ball i (V n)), ∃ x_1 ∈ V n, ∃ (a : X), (x, a) = x_1 ∧ a ∈ iUnion U
Tactic: obtain ⟨i, hi, hx⟩ := Set.mem_iUnion₂.1 (Set.eq_univ_iff_forall.1 (hUu n) x)
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (hypothesis)
Goal:
ι : Type u_1
X_1 : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst_4 : TopologicalSpace X
inst_5 : LindelofSpace X
inst_6 : PseudoMetrizableSpace X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : (n : ℕ) → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), Eq.{u_5 + 1} (α := Set X) (⋃ x ∈ U n, ball x (V n)) univ
x : X
n : ℕ
h : True
i : X
hi : i ∈ U n
hx : x ∈ ball i (V n)
⊢ ∃ x_1 ∈ V n, ∃ (a : X), (x, a) = x_1 ∧ a ∈ iUnion U
have hx₁ : Membership.mem (γ := Set X) {y : X | (y, i) ∈ V n} x
Tactic: rw [ball_eq_of_symmetry] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this : UniformSpace X := pseudoMetrizableSpaceUniformity X
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[inst] t
have this₁ : (𝓤 X).IsCountablyGenerated
Tactic: have := pseudoMetrizableSpaceUniformity_countably_generated X
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[inst] t
have hs₁ : ∀ U ∈ 𝓤 X, ∃ (t : Set X), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
Tactic: apply subset_countable_closure_of_almost_dense_set
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
hU : U ∈ 𝓤 X
⊢ ∃ (t : Set X), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
have hs₁ : ∀ (t : Set X) (htc : t.Countable) (hst : s ⊆ closure[inst] t), ∃ (t : Set X), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
Tactic: obtain ⟨t, htc, hst⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
hU : U ∈ 𝓤 X
t : Set X
htc : t.Countable
hst : s ⊆ closure[inst] t
⊢ ∃ (t : Set X), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
have hs : ∀ (x : X) (hx : x ∈ s), Membership.mem (γ := Set X) (⋃ x ∈ t, ball x U) x
Tactic: refine ⟨t, htc, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
hU : U ∈ 𝓤 X
t : Set X
htc : t.Countable
hst : s ⊆ closure[inst] t
x : X
hx : x ∈ s
⊢ Membership.mem (γ := Set X) (⋃ x ∈ t, ball x U) x
have hs : ∀ (y : X) (hyx : y ∈ ball x (symmetrize U)) (hyt : y ∈ t), Membership.mem (γ := Set X) (⋃ x ∈ t, ball x U) x
Tactic: obtain ⟨y, hyx, hyt⟩ := mem_closure_iff_ball.1 (hst hx) (symmetrize_mem_uniformity hU)
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
⊢ SeparableSpace.{u_2} (↑s : Type u_2)
have rcases : ∀ (t : Set X) (hts : t ⊆ s) (htc : t.Countable) (hst : s ⊆ closure[inst] t), SeparableSpace.{u_2} (↑s : Type u_2)
Tactic: rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, hst⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set X
hts : t ⊆ s
htc : t.Countable
hst : s ⊆ closure[inst] t
⊢ SeparableSpace.{u_2} (↑s : Type u_2)
have lift : ∀ (t : Set (↑s : Type u_2)) (htc : (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t).Countable)
  (hst : s ⊆ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)), SeparableSpace.{u_2} (↑s : Type u_2)
Tactic: lift t to Set s using hts
Cleared hypotheses: t, hts, htc, hst
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set (↑s : Type u_2)
htc : (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t).Countable
hst : s ⊆ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
⊢ SeparableSpace.{u_2} (↑s : Type u_2)
have refine : Dense t
Tactic: refine ⟨⟨t, countable_of_injective_of_countable_image Subtype.coe_injective.injOn htc, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set (↑s : Type u_2)
htc : (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t).Countable
hst : s ⊆ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
⊢ Dense t
have rwa : ∀ (x : { x : X // x ∈ s }), (↑x : X) ∈ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
Tactic: rwa [IsInducing.subtypeVal.dense_iff, Subtype.forall]
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set (↑s : Type u_2)
htc : (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t).Countable
hst : s ⊆ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
rwa : ∀ (x : { x : X // x ∈ s }), (↑x : X) ∈ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
⊢ Dense t
have rwa₁ : ∀ (a : X) (b : a ∈ s),
  (↑(Subtype.mk (p := fun (a : X) ↦ a ∈ s) a b) : X) ∈ closure[inst] (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' t)
Tactic: rwa [IsInducing.subtypeVal.dense_iff, Subtype.forall]