awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace β
s : Set α
⊢ Isometry (α := α →ᵤ[{s}] β) (β := UniformFun.{u_1, u_2} (↑s : Type u_1) β)
    (Function.comp (β := (↑s : Type u_1) → β)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
        (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
      (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) (⇑(toFun {s}) : (a : α →ᵤ[{s}] β) → α → β) :
        (α →ᵤ[{s}] β) → (↑s : Type u_1) → β))

Tactic:
simp [Isometry, edist_def, UniformFun.edist_def, iSup_subtype]

Premises used: iSup_subtype, UniformFun.edist_def, UniformOnFun.edist_def, Isometry
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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)
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)
⊢ 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 (⋃₀ 𝔖)

Premises used: Set.sUnion, Set.Elem, isEmpty_or_nonempty
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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 : 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:
simp_all [edist_def]

Premises used: UniformOnFun.edist_def
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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_1 : Nonempty.{u_1 + 1} (↑(⋃₀ 𝔖) : Type u_1)
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
⊢ BddAbove (α := ℝ)
    (Set.range fun (x : (↑(⋃₀ 𝔖) : Type u_1)) ↦
      dist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x : α) : β)
        ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x : α) : β))

Tactic:
use (Metric.ediam (.univ : Set β)).toReal

Premises used: Set.univ, Metric.ediam, ENNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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)
⊢ 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:
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]

Premises used: ENNReal.ofReal_le_iff_le_toReal, BoundedSpace.bounded_univ, Metric.edist_le_ediam_of_mem, eq_comm, Bornology.IsBounded.ediam_ne_top, edist_dist, mem_upperBounds
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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 : α) : β))

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]
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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)

Tactic:
ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_

Premises used: ENNReal.eq_of_forall_le_nnreal_iff
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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 : α) : β))
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∞)
⊢ 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:
refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_

Premises used: ENNReal.eq_of_forall_le_nnreal_iff
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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 : α) : β))
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:
simp [edist_def, ciSup_le_iff this]

Premises used: ciSup_le_iff, UniformOnFun.edist_def
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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.image (α := α →ᵤ β)
      (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β) (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
      Set.univ)

Tactic:
lipschitzWith_one_ofFun_toFun (𝔖 := 𝔖) (β := β) |>.isBounded_image (.all Set.univ)

Premises used: Bornology.IsBounded.all, UniformOnFun.lipschitzWith_one_ofFun_toFun, Set.univ, LipschitzWith.isBounded_image
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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 β
h :
  Eq (α := Set (α →ᵤ[𝔖] β)) Set.univ
    (Set.image (α := α →ᵤ β)
      (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β) (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
      Set.univ)
⊢ Bornology.IsBounded (α := α →ᵤ[𝔖] β) Set.univ

Tactic:
convert! lipschitzWith_one_ofFun_toFun (𝔖 := 𝔖) (β := β) |>.isBounded_image (.all Set.univ)

Premises used: Bornology.IsBounded.all, UniformOnFun.lipschitzWith_one_ofFun_toFun, Set.univ, LipschitzWith.isBounded_image
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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 β
h :
  ∀ (f : α →ᵤ[𝔖] β),
    Membership.mem (γ := Set (α →ᵤ[𝔖] β)) Set.univ f ↔
      Membership.mem (γ := Set (α →ᵤ[𝔖] β))
        (Set.image (α := α →ᵤ β)
          (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β) (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
          Set.univ)
        f
⊢ Eq (α := Set (α →ᵤ[𝔖] β)) Set.univ
    (Set.image (α := α →ᵤ β)
      (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β) (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
      Set.univ)

Tactic:
ext f
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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 : α →ᵤ[𝔖] β
h : ∃ (y : α →ᵤ β), (ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) ((UniformFun.toFun : (a : α →ᵤ β) → α → β) y) = f
⊢ Membership.mem (γ := Set (α →ᵤ[𝔖] β)) Set.univ f ↔
    Membership.mem (γ := Set (α →ᵤ[𝔖] β))
      (Set.image (α := α →ᵤ β)
        (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β) (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))
        Set.univ)
      f

Tactic:
simp only [Set.mem_univ, Function.comp_apply, Set.image_univ, Set.mem_range, true_iff]

Premises used: Set.image_univ, Set.mem_range, true_iff, Set.mem_univ, Function.comp_apply
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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 : α →ᵤ[𝔖] β
⊢ (ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β)
      ((UniformFun.toFun : (a : α →ᵤ β) → α → β)
        ((UniformFun.ofFun : (a : α → β) → α →ᵤ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) : α →ᵤ β)) =
    f

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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 : α →ᵤ[𝔖] β
⊢ ∃ (y : α →ᵤ β), (ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) ((UniformFun.toFun : (a : α →ᵤ β) → α → β) y) = f

Tactic:
exact ⟨UniformFun.ofFun (toFun 𝔖 f), by simp⟩
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
inst_1 : PseudoMetricSpace β
inst_2 : TopologicalSpace α
f g : α →ᵤ[𝔖] β
inst_3 : CompactSpace.{u_1} (↑(⋃₀ 𝔖) : Type u_1)
hf : ContinuousOn.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) (⋃₀ 𝔖)
hg : ContinuousOn.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g) (⋃₀ 𝔖)
⊢ edist
      { toFun := (⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f), continuous_toFun := ⋯ :
        ContinuousMap.{u_1, u_2} (↑(⋃₀ 𝔖) : Type u_1) β }
      { toFun := (⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g), continuous_toFun := ⋯ :
        ContinuousMap.{u_1, u_2} (↑(⋃₀ 𝔖) : Type u_1) β } =
    edist f g

Tactic:
simp [ContinuousMap.edist_eq_iSup, iSup_subtype, edist_def]

Premises used: iSup_subtype, UniformOnFun.edist_def, ContinuousMap.edist_eq_iSup
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : TopologicalSpace α
s : Set α
f g : α →ᵤ[{s}] β
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
hf : ContinuousOn.{u_1, u_2} (Y := β) ((toFun {s} : (a : α →ᵤ[{s}] β) → α → β) f) s
hg : ContinuousOn.{u_1, u_2} (Y := β) ((toFun {s} : (a : α →ᵤ[{s}] β) → α → β) g) s
⊢ edist
      { toFun := s.restrict (π := fun (a : α) ↦ β) ((toFun {s} : (a : α →ᵤ[{s}] β) → α → β) f), continuous_toFun := ⋯ :
        ContinuousMap.{u_1, u_2} (↑s : Type u_1) β }
      { toFun := s.restrict (π := fun (a : α) ↦ β) ((toFun {s} : (a : α →ᵤ[{s}] β) → α → β) g), continuous_toFun := ⋯ :
        ContinuousMap.{u_1, u_2} (↑s : Type u_1) β } =
    edist f g

Tactic:
simp [ContinuousMap.edist_eq_iSup, iSup_subtype, edist_def]

Premises used: iSup_subtype, UniformOnFun.edist_def, ContinuousMap.edist_eq_iSup
-- Module: Mathlib.Topology.Metrizable.Basic
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
u : UniformSpace X
hu : (𝓤 X).IsCountablyGenerated
⊢ PseudoMetrizableSpace X

Tactic:
⟨⟨u, rfl, hu⟩⟩

Premises used: TopologicalSpace.PseudoMetrizableSpace.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Metrizable.Basic
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
t : TopologicalSpace X
inst_4 : PseudoMetrizableSpace X
⊢ toTopologicalSpace = t

Tactic:
rfl
-- Module: Mathlib.Topology.Metrizable.Basic
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
t : TopologicalSpace X
inst_4 : PseudoMetrizableSpace X
⊢ toTopologicalSpace = t

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_5
inst : TopologicalSpace X
h : PseudoMetrizableSpace X
⊢ (𝓤 X).IsCountablyGenerated

Tactic:
h.exists_countably_generated.choose_spec.2

Premises used: Exists.choose_spec, uniformity, And.right, Classical.choose, TopologicalSpace.PseudoMetrizableSpace.exists_countably_generated
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
inst_4 : PseudoMetrizableSpace X
inst_5 : PseudoMetrizableSpace Y
⊢ PseudoMetrizableSpace (X × Y)

Tactic:
let : UniformSpace X := pseudoMetrizableSpaceUniformity X
  have : (uniformity X).IsCountablyGenerated :=
    pseudoMetrizableSpaceUniformity_countably_generated X
  let : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
  have : (uniformity Y).IsCountablyGenerated :=
    pseudoMetrizableSpaceUniformity_countably_generated Y
  inferInstance

Premises used: inferInstance, TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated, TopologicalSpace.pseudoMetrizableSpaceUniformity
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PseudoMetrizableSpace Y
f : X → Y
hf : IsInducing f
⊢ PseudoMetrizableSpace X

Tactic:
let u : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
  have : (uniformity Y).IsCountablyGenerated :=
    pseudoMetrizableSpaceUniformity_countably_generated Y
  ⟨⟨u.comap f, u.toTopologicalSpace_comap.trans hf.eq_induced.symm,
    Filter.comap.isCountablyGenerated (uniformity Y) (Prod.map f f)⟩⟩

Premises used: TopologicalSpace.PseudoMetrizableSpace.mk, UniformSpace.toTopologicalSpace_comap, uniformity, Prod.map, And.intro, Exists.intro, TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated, UniformSpace.comap, Eq.symm, Topology.IsInducing.eq_induced, Filter.comap.isCountablyGenerated, Eq.trans, TopologicalSpace.pseudoMetrizableSpaceUniformity
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
h : PseudoMetrizableSpace X
⊢ FirstCountableTopology X

Tactic:
let : UniformSpace X := pseudoMetrizableSpaceUniformity X
  have : (uniformity X).IsCountablyGenerated :=
    pseudoMetrizableSpaceUniformity_countably_generated X
  inferInstance

Premises used: inferInstance, TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated, TopologicalSpace.pseudoMetrizableSpaceUniformity
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
inst_4 : PseudoMetrizableSpace X
s : Set X
⊢ PseudoMetrizableSpace.{u_2} (↑s : Type u_2)

Tactic:
IsInducing.subtypeVal.pseudoMetrizableSpace

Premises used: Topology.IsInducing.pseudoMetrizableSpace, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_4} (A i)
⊢ PseudoMetrizableSpace ((i : ι) → A i)

Tactic:
let := fun i => pseudoMetrizableSpaceUniformity (A i)
  have := fun i => pseudoMetrizableSpaceUniformity_countably_generated (A i)
  inferInstance

Premises used: inferInstance, TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated, TopologicalSpace.pseudoMetrizableSpaceUniformity
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
inst_4 : PseudoMetrizableSpace X
⊢ RegularSpace X

Tactic:
let := pseudoMetrizableSpaceUniformity X
  inferInstance

Premises used: inferInstance, TopologicalSpace.pseudoMetrizableSpaceUniformity
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
inst_4 : MetrizableSpace X
⊢ T2Space X

Tactic:
letI : UniformSpace X := pseudoMetrizableSpaceUniformity X
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Metrizable.Basic
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
A : ι → Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Finite ι
inst_3 : (i : ι) → TopologicalSpace (A i)
inst_4 : MetrizableSpace X
s : Set X
⊢ MetrizableSpace.{u_2} (↑s : Type u_2)

Tactic:
IsEmbedding.subtypeVal.metrizableSpace

Premises used: Topology.IsEmbedding.metrizableSpace, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Metrizable.Basic
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)))
rw₂ rw₃ : closure[inst] u ⊆ 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) ⋯)))

Tactic:
rw [← Set.range_comp, Set.val_comp_inclusion, Subtype.range_coe]

Premises used: Set.range_comp, Set.val_comp_inclusion, Subtype.range_coe
-- Module: Mathlib.Topology.Metrizable.Basic
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
⊢ (𝓤 X).IsCountablyGenerated

Tactic:
have := pseudoMetrizableSpaceUniformity_countably_generated X
-- Module: Mathlib.Topology.Metrizable.Basic
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
suffices : SeparableSpace X
⊢ SecondCountableTopology X

Tactic:
suffices _ : SeparableSpace X from secondCountable_of_separable X
-- Module: Mathlib.Topology.Metrizable.Basic
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
obtain : ∀ (V : ℕ → SetRel X X) (hVb : (𝓤 X).HasAntitoneBasis V) (hVs : ∀ (n : ℕ), (V n).IsSymm), SeparableSpace X
⊢ SeparableSpace X

Tactic:
obtain ⟨V, hVb, hVs⟩ := has_seq_basis X

Premises used: UniformSpace.has_seq_basis
-- Module: Mathlib.Topology.Metrizable.Basic
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
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
⊢ 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))

Premises used: UniformSpace.ball_mem_nhds, LindelofSpace.elim_nhds_subcover, Filter.HasAntitoneBasis.mem, UniformSpace.ball