awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
a : X
⊢ Eq (α := ℝ)
    ((comp (β := (↑(Set.Icc (-‖f‖) ‖f‖) : Type)) (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)) (↑f : C(X, ℝ)).attachBound :
          (a : X) → ℝ)
        a :
      ℝ)
    (((↑((Polynomial.aeval f : (a : ℝ[X]) → ↥A) g) : C(X, ℝ)) : (a : X) → ℝ) a : ℝ)
have h : Eq (α := ℝ)
  ((comp (β := (↑(Set.Icc (-‖f‖) ‖f‖) : Type)) (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)) (↑f : C(X, ℝ)).attachBound :
        (a : X) → ℝ)
      a :
    ℝ)
  (Polynomial.eval (((↑f : C(X, ℝ)) : (a : X) → ℝ) a) g : ℝ)
Tactic: simp only [Polynomial.aeval_subalgebra_coe, Polynomial.aeval_continuousMap_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
⊢ comp (β := (↑(Set.Icc (-‖f‖) ‖f‖) : Type)) (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)) (↑f : C(X, ℝ)).attachBound ∈ A
have rw : (↑((Polynomial.aeval f : (a : ℝ[X]) → ↥A) g) : C(X, ℝ)) ∈ A
Tactic: rw [polynomial_comp_attachBound]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
p : C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ)
⊢ p.comp (↑f : C(X, ℝ)).attachBound ∈ A.topologicalClosure
have mem_closure : Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ))
  (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))) p
Tactic: have mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure :=
    continuousMap_mem_polynomialFunctions_closure _ _ p
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
p : C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ)
mem_closure :
  Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))) p
⊢ p.comp (↑f : C(X, ℝ)).attachBound ∈ A.topologicalClosure
have frequently_mem_polynomials : ∃ᶠ (x : C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ)) in nhds p,
  x ∈
    (↑(Subalgebra.toSubsemiring (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))) : Set C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ))
Tactic: have frequently_mem_polynomials := mem_closure_iff_frequently.mp mem_closure
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
p : C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ)
mem_closure :
  Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))) p
frequently_mem_polynomials :
  ∃ᶠ (x : C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ)) in nhds p,
    x ∈
      (↑(Subalgebra.toSubsemiring (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))) :
        Set C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ))
⊢ p.comp (↑f : C(X, ℝ)).attachBound ∈ A.topologicalClosure
have apply : ∃ᶠ (x : C(X, ℝ)) in nhds (p.comp (↑f : C(X, ℝ)).attachBound), x ∈ (↑A.toSubsemiring : Set C(X, ℝ))
Tactic: apply mem_closure_iff_frequently.mpr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
p : C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ)
mem_closure :
  Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))) p
frequently_mem_polynomials :
  ∃ᶠ (x : C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ)) in nhds p,
    x ∈
      (↑(Subalgebra.toSubsemiring (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))) :
        Set C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ))
⊢ ∃ᶠ (x : C(X, ℝ)) in nhds (p.comp (↑f : C(X, ℝ)).attachBound), x ∈ (↑A.toSubsemiring : Set C(X, ℝ))
have ℝ : ∀
  x ∈
    (↑(Subalgebra.toSubsemiring (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))) : Set C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ)),
  Membership.mem (α := C(X, ℝ)) (↑A.toSubsemiring : Set C(X, ℝ))
    ((compRightContinuousMap ℝ (↑f : C(X, ℝ)).attachBound :
          (a : C((↑(Set.Icc (-‖(↑f : C(X, ℝ))‖) ‖(↑f : C(X, ℝ))‖) : Type), ℝ)) → C(X, ℝ))
        x :
      C(X, ℝ))
Tactic: refine
    ((compRightContinuousMap ℝ (attachBound (f : C(X, ℝ)))).continuousAt
            p).tendsto.frequently_map
      _ ?_ frequently_mem_polynomials
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
p : C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ)
mem_closure :
  Membership.mem (γ := Subalgebra ℝ C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ))
    (Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))) p
frequently_mem_polynomials :
  ∃ᶠ (x : C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ)) in nhds p,
    x ∈
      (↑(Subalgebra.toSubsemiring (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))) :
        Set C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ))
g : ℝ[X]
⊢ Membership.mem (α := C(X, ℝ)) (↑A.toSubsemiring : Set C(X, ℝ))
    ((compRightContinuousMap ℝ (↑f : C(X, ℝ)).attachBound :
          (a : C((↑(Set.Icc (-‖(↑f : C(X, ℝ))‖) ‖(↑f : C(X, ℝ))‖) : Type), ℝ)) → C(X, ℝ))
        (((↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc (-‖f‖) ‖f‖)) : ℝ[X] →+* C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ)) :
            (a : ℝ[X]) → C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ))
          g) :
      C(X, ℝ))
have simp : comp (β := (↑(Set.Icc (-‖(↑f : C(X, ℝ))‖) ‖(↑f : C(X, ℝ))‖) : Type)) (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖))
    (↑f : C(X, ℝ)).attachBound ∈
  A.toSubsemiring
Tactic: simp only [SetLike.mem_coe, AlgHom.coe_toRingHom, compRightContinuousMap_apply,
    Polynomial.toContinuousMapOnAlgHom_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
f' : C(X, (↑(Set.Icc (-‖(↑f : C(X, ℝ))‖) ‖(↑f : C(X, ℝ))‖) : Type)) := (↑f : C(X, ℝ)).attachBound
abs : C((↑(Set.Icc (-‖f‖) ‖f‖) : Type), ℝ) :=
  { toFun := fun (x : (↑(Set.Icc (-‖f‖) ‖f‖) : Type)) ↦ |(↑x : ℝ)|, continuous_toFun := ⋯ }
⊢ |(↑f : C(X, ℝ))| ∈ A.topologicalClosure
have change : abs.comp f' ∈ A.topologicalClosure
Tactic: change abs.comp f' ∈ A.topologicalClosure
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ (↑f : C(X, ℝ)) ⊓ (↑g : C(X, ℝ)) ∈ A.topologicalClosure
have rw : HSMul.hSMul (α := ℝ) 2⁻¹ ((↑f : C(X, ℝ)) + (↑g : C(X, ℝ)) - |(↑g : C(X, ℝ)) - (↑f : C(X, ℝ))|) ∈ A.topologicalClosure
Tactic: rw [inf_eq_half_smul_add_sub_abs_sub' ℝ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ HSMul.hSMul (α := ℝ) 2⁻¹ ((↑f : C(X, ℝ)) + (↑g : C(X, ℝ)) - |(↑g : C(X, ℝ)) - (↑f : C(X, ℝ))|) ∈ A.topologicalClosure
have _ : |(↑g : C(X, ℝ)) - (↑f : C(X, ℝ))| ∈ A.topologicalClosure
Tactic: refine
    A.topologicalClosure.smul_mem
      (A.topologicalClosure.sub_mem
        (A.topologicalClosure.add_mem (A.le_topologicalClosure f.property)
          (A.le_topologicalClosure g.property))
        ?_)
      _
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed (↑A : Set C(X, ℝ))
f g : ↥A
⊢ (↑f : C(X, ℝ)) ⊓ (↑g : C(X, ℝ)) ∈ A
have h₁ : A = A.topologicalClosure
Tactic: convert! inf_mem_subalgebra_closure A f g
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed (↑A : Set C(X, ℝ))
f g : ↥A
⊢ A = A.topologicalClosure
have h₁ : (↑A : Set C(X, ℝ)) = (↑A.topologicalClosure : Set C(X, ℝ))
Tactic: apply SetLike.ext'
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed (↑A : Set C(X, ℝ))
f g : ↥A
⊢ (↑A : Set C(X, ℝ)) = (↑A.topologicalClosure : Set C(X, ℝ))
have h₁ : (↑A.topologicalClosure : Set C(X, ℝ)) = (↑A : Set C(X, ℝ))
Tactic: symm
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ (↑f : C(X, ℝ)) ⊔ (↑g : C(X, ℝ)) ∈ A.topologicalClosure
have rw : HSMul.hSMul (α := ℝ) 2⁻¹ ((↑f : C(X, ℝ)) + (↑g : C(X, ℝ)) + |(↑g : C(X, ℝ)) - (↑f : C(X, ℝ))|) ∈ A.topologicalClosure
Tactic: rw [sup_eq_half_smul_add_add_abs_sub' ℝ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ HSMul.hSMul (α := ℝ) 2⁻¹ ((↑f : C(X, ℝ)) + (↑g : C(X, ℝ)) + |(↑g : C(X, ℝ)) - (↑f : C(X, ℝ))|) ∈ A.topologicalClosure
have _ : |(↑g : C(X, ℝ)) - (↑f : C(X, ℝ))| ∈ A.topologicalClosure
Tactic: refine
    A.topologicalClosure.smul_mem
      (A.topologicalClosure.add_mem
        (A.topologicalClosure.add_mem (A.le_topologicalClosure f.property)
          (A.le_topologicalClosure g.property))
        ?_)
      _
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed (↑A : Set C(X, ℝ))
f g : ↥A
⊢ (↑f : C(X, ℝ)) ⊔ (↑g : C(X, ℝ)) ∈ A
have h₁ : A = A.topologicalClosure
Tactic: convert! sup_mem_subalgebra_closure A f g
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : L.SeparatesPointsStrongly
⊢ closure L = ⊤
have rw : ⊤ ≤ closure L
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : L.SeparatesPointsStrongly
f : C(X, ℝ)
⊢ f ∈ closure L
have fun : ∀ (ε : ℝ) (pos : 0 < ε), ∃ x ∈ Metric.ball f ε, x ∈ L
Tactic: refine
    Filter.Frequently.mem_closure
      ((Filter.HasBasis.frequently_iff Metric.nhds_basis_ball).mpr fun ε pos => ?_)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : L.SeparatesPointsStrongly
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
have pos₁ : ∀ (nX : Nonempty X), ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
Tactic: by_cases nX : Nonempty X
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : L.SeparatesPointsStrongly
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
pos₁ : ∀ (nX : Nonempty X), ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
⊢ ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
have neg : ∀ (nX : ¬Nonempty X), ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
Tactic: by_cases nX : Nonempty X
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
⊢ ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
have pos₁ : ∀ (g : (x y : X) → C(X, ℝ)) (hg : ∀ (x y : X), g x y ∈ L)
  (w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ))
  (w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)),
  ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
Tactic: choose g hg w₁ w₂ using sep f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
x y : X
⊢ U x y ∈ 𝓝 y
have refine_1 : IsOpen[inst] (U x y)
Tactic: refine IsOpen.mem_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
x y : X
refine_1 : IsOpen[inst] (U x y)
⊢ U x y ∈ 𝓝 y
have refine_2 : y ∈ U x y
Tactic: refine IsOpen.mem_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
x y : X
⊢ IsOpen[inst] (U x y)
have refine_1 : Continuous[inst, _] fun (b : X) ↦ HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) b : ℝ) ε
Tactic: apply isOpen_lt
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
x y : X
refine_1 : Continuous[inst, _] fun (b : X) ↦ HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) b : ℝ) ε
⊢ IsOpen[inst] (U x y)
have refine_1₁ : Continuous[inst, _] (⇑(g x y) : (a : X) → ℝ)
Tactic: apply isOpen_lt
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
x y : X
⊢ y ∈ U x y
have refine_2 : HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) y : ℝ) ε < (f : (a : X) → ℝ) y
Tactic: rw [Set.mem_setOf_eq, w₂]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
⊢ ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
have U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
Tactic: have U_nhds_y : ∀ x y, U x y ∈ 𝓝 y := by
    intro x y
    refine IsOpen.mem_nhds ?_ ?_
    · apply isOpen_lt <;> fun_prop
    · rw [Set.mem_setOf_eq, w₂]
      exact sub_lt_self _ pos
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
⊢ ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
have ys_nonempty : ∀ (x : X), (ys x).Nonempty
Tactic: have ys_nonempty : ∀ x, (ys x).Nonempty := fun x =>
    Set.nonempty_of_union_eq_top_of_nonempty _ _ nX (ys_w x)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
x z : X
⊢ HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
have obtain : ∀ (y : X) (ym : y ∈ (↑(ys x) : Set X)) (zm : z ∈ U x y),
  HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
Tactic: obtain ⟨y, ym, zm⟩ := Set.exists_set_mem_of_union_eq_top _ _ (ys_w x) z
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
x z y : X
ym : y ∈ (↑(ys x) : Set X)
zm : z ∈ U x y
⊢ HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
have dsimp : HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((ys x).sup' sorry fun (y : X) ↦ g x y : (a : X) → ℝ) z
Tactic: dsimp [h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
x z y : X
ym : y ∈ (↑(ys x) : Set X)
zm : z ∈ U x y
⊢ HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((ys x).sup' ⋯ fun (y : X) ↦ g x y : (a : X) → ℝ) z
have simp : ∃ b ∈ ys x, HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x b : (a : X) → ℝ) z
Tactic: simp only [coe_sup', Finset.sup'_apply, Finset.lt_sup'_iff]