awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this_3 : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
δ : ℝ
δ0 : 0 < δ
h_fin : Set.Finite.{u_1} (α := (↑s : Type u_1)) {UV : (↑s : Type u_1) | δ ≤ ε UV}
this :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (UV : (↑s : Type u_1)),
      δ ≤ ε UV → dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
y : X
hy :
  ∀ (UV : (↑s : Type u_1)),
    δ ≤ ε UV → dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
UV : (↑s : Type u_1)
refine_1 :
  ∀ (hle : δ ≤ ε UV),
    dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
refine_1₁ :
  ∀ (hle : ε UV ≤ δ),
    dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
⊢ dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ

Tactic:
rcases le_total δ (ε UV) with hle | hle

Premises used: le_total
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this_3 : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
δ : ℝ
δ0 : 0 < δ
h_fin : Set.Finite.{u_1} (α := (↑s : Type u_1)) {UV : (↑s : Type u_1) | δ ≤ ε UV}
this :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (UV : (↑s : Type u_1)),
      δ ≤ ε UV → dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
y : X
hy :
  ∀ (UV : (↑s : Type u_1)),
    δ ≤ ε UV → dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
UV : (↑s : Type u_1)
hle : δ ≤ ε UV
⊢ dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ

Tactic:
hy _ hle
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this_3 : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
δ : ℝ
δ0 : 0 < δ
h_fin : Set.Finite.{u_1} (α := (↑s : Type u_1)) {UV : (↑s : Type u_1) | δ ≤ ε UV}
this :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (UV : (↑s : Type u_1)),
      δ ≤ ε UV → dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
y : X
hy :
  ∀ (UV : (↑s : Type u_1)),
    δ ≤ ε UV → dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
UV : (↑s : Type u_1)
hle : ε UV ≤ δ
rwa rwa₁ rwa₂ rwa₃ : ε UV ≤ δ
⊢ ε UV - 0 ≤ δ

Tactic:
rwa [sub_zero]

Premises used: sub_zero
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this_3 : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
δ : ℝ
δ0 : 0 < δ
h_fin : Set.Finite.{u_1} (α := (↑s : Type u_1)) {UV : (↑s : Type u_1) | δ ≤ ε UV}
this :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (UV : (↑s : Type u_1)),
      δ ≤ ε UV → dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
y : X
hy :
  ∀ (UV : (↑s : Type u_1)),
    δ ≤ ε UV → dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
UV : (↑s : Type u_1)
hle : δ ≤ ε UV
⊢ dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ

Tactic:
exacts [hy _ hle, (Real.dist_le_of_mem_Icc (hf0ε _ _) (hf0ε _ _)).trans (by rwa [sub_zero])]

Premises used: Real.dist_le_of_mem_Icc, LE.le.trans
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
⊢ comap F (𝓝 (F x)) ≤ 𝓝 x

Tactic:
((nhds_basis_ball.comap _).le_basis_iff hB.nhds_hasBasis).2 ?_

Premises used: Iff.mpr, Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap, Metric.nhds_basis_ball, TopologicalSpace.IsTopologicalBasis.nhds_hasBasis
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
refine_2 : ∀ (i' : Set X), i' ∈ B ∧ x ∈ i' → ∃ (i : ℝ), 0 < i ∧ F ⁻¹' ball (F x) i ⊆ i'
⊢ comap F (𝓝 (F x)) ≤ 𝓝 x

Tactic:
refine ((nhds_basis_ball.comap _).le_basis_iff hB.nhds_hasBasis).2 ?_

Premises used: Iff.mpr, Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap, Metric.nhds_basis_ball, TopologicalSpace.IsTopologicalBasis.nhds_hasBasis
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
refine_2 :
  ∀ (U : Set X) (hUB : U ∈ B) (hxU : x ∈ U) (hUV : closure[inst] U ⊆ V), ∃ (i : ℝ), 0 < i ∧ F ⁻¹' ball (F x) i ⊆ V
⊢ ∃ (i : ℝ), 0 < i ∧ F ⁻¹' ball (F x) i ⊆ V

Tactic:
rcases hB.exists_closure_subset (hB.mem_nhds hVB hxV) with ⟨U, hUB, hxU, hUV⟩

Premises used: TopologicalSpace.IsTopologicalBasis.mem_nhds, TopologicalSpace.IsTopologicalBasis.exists_closure_subset
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst] U ⊆ V
UV : (↑s : Type u_1) := Subtype.mk (p := fun (x : Set X × Set X) ↦ x ∈ s) (U, V) ⋯
⊢ ∃ (i : ℝ), 0 < i ∧ F ⁻¹' ball (F x) i ⊆ V

Tactic:
⟨ε UV, (ε01 UV).1, fun y (hy : dist (F y) (F x) < ε UV) => ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst] U ⊆ V
UV : (↑s : Type u_1) := Subtype.mk (p := fun (x : Set X × Set X) ↦ x ∈ s) (U, V) ⋯
refine_2 : ∀ (y : X) (hy : dist (F y) (F x) < ε UV), y ∈ V
⊢ ∃ (i : ℝ), 0 < i ∧ F ⁻¹' ball (F x) i ⊆ V

Tactic:
refine ⟨ε UV, (ε01 UV).1, fun y (hy : dist (F y) (F x) < ε UV) => ?_⟩
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst] U ⊆ V
UV : (↑s : Type u_1) := Subtype.mk (p := fun (x : Set X × Set X) ↦ x ∈ s) (U, V) ⋯
y : X
hy : dist (F y) (F x) < ε UV
⊢ dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) < ε UV

Tactic:
replace hy : dist (F y UV) (F x UV) < ε UV :=
      (BoundedContinuousFunction.dist_coe_le_dist _).trans_lt hy
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst] U ⊆ V
UV : (↑s : Type u_1) := Subtype.mk (p := fun (x : Set X × Set X) ↦ x ∈ s) (U, V) ⋯
y : X
hy : dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) < ε UV
refine_2 :
  ∀ (hy : ¬y ∈ V),
    ε UV ≤ dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ)
⊢ y ∈ V

Tactic:
contrapose! hy
-- Module: Mathlib.Topology.Metrizable.Urysohn
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV : Set X × Set X | UV ∈ B ×ˢ B ∧ closure[inst] UV.1 ⊆ UV.2}
this_1 : Encodable (↑s : Type u_1)
this_2 : TopologicalSpace (↑s : Type u_1) := ⊥
this : DiscreteTopology.{u_1} (↑s : Type u_1)
hd : ∀ (UV : (↑s : Type u_1)), Disjoint (closure[inst] (↑UV : Set X × Set X).1) (↑UV : Set X × Set X).2ᶜ
ε : (↑s : Type u_1) → ℝ
ε01 : ∀ (UV : (↑s : Type u_1)), Membership.mem (γ := Set ℝ) (Ioc 0 1) (ε UV)
hε : Tendsto ε cofinite (𝓝 0)
f : (UV : (↑s : Type u_1)) → C(X, ℝ)
hf0 : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1
hfε : ∀ (UV : (↑s : Type u_1)), EqOn (β := ℝ) (⇑(f UV) : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ
hf0ε : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f UV : (a : X) → ℝ) x : ℝ)
hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
F : X → (↑s : Type u_1) →ᵇ ℝ :=
  fun (x : X) ↦
    { toFun := fun (UV : (↑s : Type u_1)) ↦ (f UV : (a : X) → ℝ) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF :
  ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst] U ⊆ V
UV : (↑s : Type u_1) := Subtype.mk (p := fun (x : Set X × Set X) ↦ x ∈ s) (U, V) ⋯
y : X
hy : ¬y ∈ V
refine_2 : ε UV ≤ norm (E := ℝ) ((fun (x : X) ↦ ε UV) y)
⊢ ε UV ≤ dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ)

Tactic:
rw [hF, hF, hfε UV hy, hf0 UV hxU, Pi.zero_apply, dist_zero_right]

Premises used: Pi.zero_apply, dist_zero_right