awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
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)
UV : (↑s : Type u_1)
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1 ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ ∧
        ∀ (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f : (a : X) → ℝ) x : ℝ)
have rcases : ∀ (f : C(X, ℝ)) (hf₀ : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 (closure[inst] (↑UV : Set X × Set X).1))
  (hf₁ : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 (↑UV : Set X × Set X).2ᶜ)
  (hf01 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)),
  ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1 ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ ∧
        ∀ (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f : (a : X) → ℝ) x : ℝ)
Tactic: rcases exists_continuous_zero_one_of_isClosed isClosed_closure
        (hB.isOpen UV.2.1.2).isClosed_compl (hd UV) with
      ⟨f, hf₀, hf₁, hf01⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (hypothesis)
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 : X → (↑s : Type u_1) →ᵇ ℝ), IsInducing f
have this₁ : ∀ (UV : (↑s : Type u_1)),
  ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1 ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ ∧
        ∀ (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f : (a : X) → ℝ) x : ℝ)
Tactic: have : ∀ UV : s, ∃ f : C(X, ℝ),
      EqOn f 0 UV.1.1 ∧ EqOn f (fun _ => ε UV) UV.1.2ᶜ ∧ ∀ x, f x ∈ Icc 0 (ε UV) := by
    intro UV
    rcases exists_continuous_zero_one_of_isClosed isClosed_closure
        (hB.isOpen UV.2.1.2).isClosed_compl (hd UV) with
      ⟨f, hf₀, hf₁, hf01⟩
    exact ⟨ε UV • f, fun x hx => by simp [hf₀ (subset_closure hx)], fun x hx => by simp [hf₁ hx],
      fun x => ⟨mul_nonneg (ε01 _).1.le (hf01 _).1, mul_le_of_le_one_right (ε01 _).1.le (hf01 _).2⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
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)
this :
  ∀ (UV : (↑s : Type u_1)),
    ∃ (f : C(X, ℝ)),
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 (↑UV : Set X × Set X).1 ∧
        EqOn (β := ℝ) (⇑f : (a : X) → ℝ) (fun (x : X) ↦ ε UV) (↑UV : Set X × Set X).2ᶜ ∧
          ∀ (x : X), Membership.mem (α := ℝ) (Icc 0 (ε UV)) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (f : X → (↑s : Type u_1) →ᵇ ℝ), IsInducing f
have choose : ∀ (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 : ℝ)),
  ∃ (f : X → (↑s : Type u_1) →ᵇ ℝ), IsInducing f
Tactic: choose f hf0 hfε hf0ε using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (hypothesis)
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 : ℝ)
⊢ ∃ (f : X → (↑s : Type u_1) →ᵇ ℝ), IsInducing f
have hf01 : ∀ (UV : (↑s : Type u_1)) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f UV : (a : X) → ℝ) x : ℝ)
Tactic: have hf01 : ∀ UV x, f UV x ∈ Icc (0 : ℝ) 1 :=
    fun UV x => Icc_subset_Icc_right (ε01 _).2 (hf0ε _ _)
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (hypothesis)
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' := ⋯ }
⊢ ∃ (f : X → (↑s : Type u_1) →ᵇ ℝ), IsInducing f
have hF : ∀ (x : X) (UV : (↑s : Type u_1)), Eq (α := ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((f UV : (a : X) → ℝ) x : ℝ)
Tactic: have hF : ∀ x UV, F x UV = f UV x := fun _ _ => rfl
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
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 : ℝ)
⊢ ∃ (f : X → (↑s : Type u_1) →ᵇ ℝ), IsInducing f
have refine_1 : ∀ (x : X), 𝓝 x ≤ comap F (𝓝 (F x))
Tactic: refine ⟨F, isInducing_iff_nhds.2 fun x => le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
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 : ℝ)
refine_1 : ∀ (x : X), 𝓝 x ≤ comap F (𝓝 (F x))
⊢ ∃ (f : X → (↑s : Type u_1) →ᵇ ℝ), IsInducing f
have refine_2 : ∀ (x : X), comap F (𝓝 (F x)) ≤ 𝓝 x
Tactic: refine ⟨F, isInducing_iff_nhds.2 fun x => le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
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
⊢ 𝓝 x ≤ comap F (𝓝 (F x))
have refine_1 : ∀ (δ : ℝ) (δ0 : 0 < δ), F ⁻¹' closedBall (F x) δ ∈ 𝓝 x
Tactic: refine (nhds_basis_closedBall.comap _).ge_iff.2 fun δ δ0 => ?_
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (hypothesis)
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
δ : ℝ
δ0 : 0 < δ
⊢ F ⁻¹' closedBall (F x) δ ∈ 𝓝 x
have h_fin : Set.Finite.{u_1} (α := (↑s : Type u_1)) {UV : (↑s : Type u_1) | δ ≤ ε UV}
Tactic: have h_fin : { UV : s | δ ≤ ε UV }.Finite := by simpa only [← not_lt] using hε (gt_mem_nhds δ0)
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
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
δ : ℝ
δ0 : 0 < δ
h_fin : Set.Finite.{u_1} (α := (↑s : Type u_1)) {UV : (↑s : Type u_1) | δ ≤ ε UV}
⊢ ∀ᶠ (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 : ℝ) ≤ δ
have refine : ∀ (UV : (↑s : Type u_1)),
  Membership.mem (γ := Set (↑s : Type u_1)) {UV : (↑s : Type u_1) | δ ≤ ε UV} UV →
    ∀ᶠ (x_2 : X) in 𝓝 x,
      dist (α := ℝ) ((F x_2 : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
Tactic: refine (eventually_all_finite h_fin).2 fun UV _ => ?_
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (hypothesis)
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
δ : ℝ
δ0 : 0 < δ
h_fin : Set.Finite.{u_1} (α := (↑s : Type u_1)) {UV : (↑s : Type u_1) | δ ≤ ε UV}
⊢ F ⁻¹' closedBall (F x) δ ∈ 𝓝 x
have 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 : ℝ) ≤ δ
Tactic: have : ∀ᶠ y in 𝓝 x, ∀ UV, δ ≤ ε UV → dist (F y UV) (F x UV) ≤ δ := by
      refine (eventually_all_finite h_fin).2 fun UV _ => ?_
      exact (f UV).continuous.tendsto x (closedBall_mem_nhds _ δ0)
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
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 : ℝ) ≤ δ
⊢ F ⁻¹' closedBall (F x) δ ∈ 𝓝 x
have refine_1 : ∀ (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)),
  dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
Tactic: refine this.mono fun y hy => (BoundedContinuousFunction.dist_le δ0.le).2 fun UV => ?_
-- Lean 4 proof step from Mathlib.Topology.Metrizable.Urysohn (goal)
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)
⊢ dist (α := ℝ) ((F y : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ((F x : (a : (↑s : Type u_1)) → ℝ) UV : ℝ) ≤ δ
have refine_1 : ∀ (hle : δ ≤ ε 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