awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
p s : C(α, R)₀
s_mem : Membership.mem (γ := Set C(α, R)₀) (Set.range fun (s : C(α, R)₀) ↦ star s * s) s
f : C(α, R)₀
mpr : ∀ (s : C(α, R)₀), f ≤ f + (fun (s : C(α, R)₀) ↦ star s * s) s
⊢ f ≤ f + s

Tactic:
obtain ⟨s, rfl⟩ := s_mem

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
p f s : C(α, R)₀
⊢ f ≤ f + (fun (s : C(α, R)₀) ↦ star s * s) s

Tactic:
fun x ↦ le_add_of_nonneg_right (star_mul_self_nonneg (s x))

Premises used: star_mul_self_nonneg, le_add_of_nonneg_right, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
p f s : C(α, R)₀
⊢ f ≤ f + (fun (s : C(α, R)₀) ↦ star s * s) s

Tactic:
exact fun x ↦ le_add_of_nonneg_right (star_mul_self_nonneg (s x))

Premises used: star_mul_self_nonneg, le_add_of_nonneg_right, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
p f : C(α, R)₀
⊢ f ≤ f + 0

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
p g₁ g₂ : C(α, R)₀
hx : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) g₁
hy : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) g₂
h₁ : ∀ (f : C(α, R)₀), f ≤ f + g₁
h₂ : ∀ (f : C(α, R)₀), f ≤ f + g₂
f : C(α, R)₀
⊢ f ≤ f + g₁

Tactic:
h₁ f
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
p g₁ g₂ : C(α, R)₀
hx : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) g₁
hy : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) g₂
h₁ : ∀ (f : C(α, R)₀), f ≤ f + g₁
h₂ : ∀ (f : C(α, R)₀), f ≤ f + g₂
f : C(α, R)₀
⊢ f + g₁ ≤ f + g₁ + g₂

Tactic:
h₂ (f + g₁)

Premises used: HAdd.hAdd
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
p g₁ g₂ : C(α, R)₀
hx : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) g₁
hy : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) g₂
h₁ : ∀ (f : C(α, R)₀), f ≤ f + g₁
h₂ : ∀ (f : C(α, R)₀), f ≤ f + g₂
f : C(α, R)₀
⊢ f + g₁ + g₂ = f + (g₁ + g₂)

Tactic:
add_assoc _ _ _

Premises used: add_assoc
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
p g₁ g₂ : C(α, R)₀
hx : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) g₁
hy : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) g₂
h₁ : ∀ (f : C(α, R)₀), f ≤ f + g₁
h₂ : ∀ (f : C(α, R)₀), f ≤ f + g₂
f : C(α, R)₀
⊢ f ≤ f + (g₁ + g₂)

Tactic:
calc
          f ≤ f + g₁ := h₁ f
          _ ≤ (f + g₁) + g₂ := h₂ (f + g₁)
          _ = f + (g₁ + g₂) := add_assoc _ _ _

Premises used: add_assoc, HAdd.hAdd
-- Module: Mathlib.Topology.ContinuousMap.StarOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Zero α
R : Type u_2
inst_2 : TopologicalSpace R
inst_3 : CommSemiring R
inst_4 : PartialOrder R
inst_5 : NoZeroDivisors R
inst_6 : StarRing R
inst_7 : StarOrderedRing R
inst_8 : IsTopologicalSemiring R
inst_9 : ContinuousStar R
inst_10 : StarOrderedRing C(α, R)
f p : C(α, R)₀
hp : Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) p
mpr :
  ∀ (s : C(α, R)₀) (s_mem : Membership.mem (γ := Set C(α, R)₀) (Set.range fun (s : C(α, R)₀) ↦ star s * s) s)
    (f : C(α, R)₀), f ≤ f + s
mpr₁ : ∀ (f : C(α, R)₀), f ≤ f + 0
mpr₂ :
  ∀ (g₁ g₂ : C(α, R)₀),
    Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s)) g₁ →
      Membership.mem (γ := AddSubmonoid C(α, R)₀) (AddSubmonoid.closure (Set.range fun (s : C(α, R)₀) ↦ star s * s))
          g₂ →
        ∀ (h₁ : ∀ (f : C(α, R)₀), f ≤ f + g₁) (h₂ : ∀ (f : C(α, R)₀), f ≤ f + g₂) (f : C(α, R)₀), f ≤ f + (g₁ + g₂)
⊢ f ≤ f + p

Tactic:
induction hp using AddSubmonoid.closure_induction generalizing f with
      | mem s s_mem =>
        obtain ⟨s, rfl⟩ := s_mem
        exact fun x ↦ le_add_of_nonneg_right (star_mul_self_nonneg (s x))
      | zero => simp
      | add g₁ g₂ _ _ h₁ h₂ => calc
          f ≤ f + g₁ := h₁ f
          _ ≤ (f + g₁) + g₂ := h₂ (f + g₁)
          _ = f + (g₁ + g₂) := add_assoc _ _ _

Premises used: add_assoc, rfl
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
f : C(X, ℝ)
x : X
⊢ Eq (α := ℝ)
    ((↑(((f.attachBound : C(X, (↑(Set.Icc (-‖f‖) ‖f‖) : Type))) : (a : X) → (↑(Set.Icc (-‖f‖) ‖f‖) : Type)) x) : ℝ) : ℝ)
    ((f : (a : X) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
h :
  ∀ (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 : ℝ)
⊢ comp (β := (↑(Set.Icc (-‖f‖) ‖f‖) : Type)) (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)) (↑f : C(X, ℝ)).attachBound =
    (↑((Polynomial.aeval f : (a : ℝ[X]) → ↥A) g) : C(X, ℝ))

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
a : X
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 : ℝ)
⊢ 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 : ℝ)

Tactic:
simp only [Polynomial.aeval_subalgebra_coe, Polynomial.aeval_continuousMap_apply]

Premises used: Polynomial.aeval_subalgebra_coe, Polynomial.aeval_continuousMap_apply
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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.eval (((↑f : C(X, ℝ)) : (a : X) → ℝ) a) g : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
rw : (↑((Polynomial.aeval f : (a : ℝ[X]) → ↥A) g) : C(X, ℝ)) ∈ A
⊢ comp (β := (↑(Set.Icc (-‖f‖) ‖f‖) : Type)) (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)) (↑f : C(X, ℝ)).attachBound ∈ A

Tactic:
rw [polynomial_comp_attachBound]

Premises used: ContinuousMap.polynomial_comp_attachBound
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
⊢ (↑((Polynomial.aeval f : (a : ℝ[X]) → ↥A) g) : C(X, ℝ)) ∈ A

Tactic:
apply SetLike.coe_mem

Premises used: SetLike.coe_mem
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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), ℝ)
⊢ 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
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
⊢ ∃ᶠ (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
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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), ℝ))
apply : ∃ᶠ (x : C(X, ℝ)) in nhds (p.comp (↑f : C(X, ℝ)).attachBound), x ∈ (↑A.toSubsemiring : Set C(X, ℝ))
⊢ p.comp (↑f : C(X, ℝ)).attachBound ∈ A.topologicalClosure

Tactic:
apply mem_closure_iff_frequently.mpr

Premises used: Iff.mpr, mem_closure_iff_frequently
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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, ℝ))

Tactic:
((compRightContinuousMap ℝ (attachBound (f : C(X, ℝ)))).continuousAt
            p).tendsto.frequently_map
      _ ?_ frequently_mem_polynomials

Premises used: Real, Filter.Tendsto.frequently_map, ContinuousMap.comp, ContinuousAt.tendsto, ContinuousMap.attachBound, ContinuousMap.compRightContinuousMap, Subtype.val, ContinuousMap.continuousAt
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 ∈
      (↑(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, ℝ))
⊢ ∃ᶠ (x : C(X, ℝ)) in nhds (p.comp (↑f : C(X, ℝ)).attachBound), x ∈ (↑A.toSubsemiring : Set C(X, ℝ))

Tactic:
refine
    ((compRightContinuousMap ℝ (attachBound (f : C(X, ℝ)))).continuousAt
            p).tendsto.frequently_map
      _ ?_ frequently_mem_polynomials

Premises used: Real, Filter.Tendsto.frequently_map, ContinuousAt.tendsto, ContinuousMap.attachBound, ContinuousMap.compRightContinuousMap, Subtype.val, ContinuousMap.continuousAt
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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]
simp :
  comp (β := (↑(Set.Icc (-‖(↑f : C(X, ℝ))‖) ‖(↑f : C(X, ℝ))‖) : Type)) (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖))
      (↑f : C(X, ℝ)).attachBound ∈
    A.toSubsemiring
⊢ 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, ℝ))

Tactic:
simp only [SetLike.mem_coe, AlgHom.coe_toRingHom, compRightContinuousMap_apply,
    Polynomial.toContinuousMapOnAlgHom_apply]

Premises used: AlgHom.coe_toRingHom, SetLike.mem_coe, ContinuousMap.compRightContinuousMap_apply, Polynomial.toContinuousMapOnAlgHom_apply
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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]
⊢ comp (β := (↑(Set.Icc (-‖(↑f : C(X, ℝ))‖) ‖(↑f : C(X, ℝ))‖) : Type)) (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖))
      (↑f : C(X, ℝ)).attachBound ∈
    A.toSubsemiring

Tactic:
apply polynomial_comp_attachBound_mem

Premises used: ContinuousMap.polynomial_comp_attachBound_mem
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 := ⋯ }
change : abs.comp f' ∈ A.topologicalClosure
⊢ |(↑f : C(X, ℝ))| ∈ A.topologicalClosure

Tactic:
change abs.comp f' ∈ A.topologicalClosure

Premises used: ContinuousMap.comp, Subalgebra.topologicalClosure
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 := ⋯ }
⊢ abs.comp f' ∈ A.topologicalClosure

Tactic:
apply comp_attachBound_mem_closure

Premises used: ContinuousMap.comp_attachBound_mem_closure
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
rw :
  HSMul.hSMul (α := ℝ) 2⁻¹ ((↑f : C(X, ℝ)) + (↑g : C(X, ℝ)) - |(↑g : C(X, ℝ)) - (↑f : C(X, ℝ))|) ∈ A.topologicalClosure
⊢ (↑f : C(X, ℝ)) ⊓ (↑g : C(X, ℝ)) ∈ A.topologicalClosure

Tactic:
rw [inf_eq_half_smul_add_sub_abs_sub' ℝ]

Premises used: Real, inf_eq_half_smul_add_sub_abs_sub'
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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

Tactic:
A.topologicalClosure.smul_mem
      (A.topologicalClosure.sub_mem
        (A.topologicalClosure.add_mem (A.le_topologicalClosure f.property)
          (A.le_topologicalClosure g.property))
        ?_)
      _

Premises used: Set.Mem, Subalgebra.add_mem, Subalgebra.sub_mem, Subalgebra.topologicalClosure, Subalgebra.smul_mem, Subalgebra.le_topologicalClosure, Subtype.property
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
_ : |(↑g : C(X, ℝ)) - (↑f : C(X, ℝ))| ∈ A.topologicalClosure
⊢ HSMul.hSMul (α := ℝ) 2⁻¹ ((↑f : C(X, ℝ)) + (↑g : C(X, ℝ)) - |(↑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))
        ?_)
      _

Premises used: Subalgebra.add_mem, Subalgebra.sub_mem, Subalgebra.topologicalClosure, Subalgebra.smul_mem, Subalgebra.le_topologicalClosure, Subtype.property
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ |(↑g : C(X, ℝ)) - (↑f : C(X, ℝ))| ∈ A.topologicalClosure

Tactic:
mod_cast abs_mem_subalgebra_closure A _

Premises used: ContinuousMap.abs_mem_subalgebra_closure, abs, HSub.hSub, cast, Membership.mem, Subalgebra.topologicalClosure, Eq.refl, Subtype.val
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ |(↑g : C(X, ℝ)) - (↑f : C(X, ℝ))| ∈ A.topologicalClosure

Tactic:
exact mod_cast abs_mem_subalgebra_closure A _

Premises used: ContinuousMap.abs_mem_subalgebra_closure
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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.topologicalClosure

Tactic:
inf_mem_subalgebra_closure A f g

Premises used: ContinuousMap.inf_mem_subalgebra_closure
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
h₁ : A = A.topologicalClosure
⊢ (↑f : C(X, ℝ)) ⊓ (↑g : C(X, ℝ)) ∈ A

Tactic:
convert! inf_mem_subalgebra_closure A f g

Premises used: ContinuousMap.inf_mem_subalgebra_closure
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
h₁ : (↑A : Set C(X, ℝ)) = (↑A.topologicalClosure : Set C(X, ℝ))
⊢ A = A.topologicalClosure

Tactic:
apply SetLike.ext'

Premises used: SetLike.ext'
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
h₁ : (↑A.topologicalClosure : Set C(X, ℝ)) = (↑A : Set C(X, ℝ))
⊢ (↑A : Set C(X, ℝ)) = (↑A.topologicalClosure : Set C(X, ℝ))

Tactic:
symm
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
h₁ : IsClosed (↑A : Set C(X, ℝ))
⊢ (↑A.topologicalClosure : Set C(X, ℝ)) = (↑A : Set C(X, ℝ))

Tactic:
rw [Subalgebra.topologicalClosure_coe, closure_eq_iff_isClosed]

Premises used: Subalgebra.topologicalClosure_coe, closure_eq_iff_isClosed
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
⊢ IsClosed (↑A : Set C(X, ℝ))

Tactic:
h
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
⊢ IsClosed (↑A : Set C(X, ℝ))

Tactic:
exact h
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
rw :
  HSMul.hSMul (α := ℝ) 2⁻¹ ((↑f : C(X, ℝ)) + (↑g : C(X, ℝ)) + |(↑g : C(X, ℝ)) - (↑f : C(X, ℝ))|) ∈ A.topologicalClosure
⊢ (↑f : C(X, ℝ)) ⊔ (↑g : C(X, ℝ)) ∈ A.topologicalClosure

Tactic:
rw [sup_eq_half_smul_add_add_abs_sub' ℝ]

Premises used: Real, sup_eq_half_smul_add_add_abs_sub'
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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

Tactic:
A.topologicalClosure.smul_mem
      (A.topologicalClosure.add_mem
        (A.topologicalClosure.add_mem (A.le_topologicalClosure f.property)
          (A.le_topologicalClosure g.property))
        ?_)
      _

Premises used: Set.Mem, Subalgebra.add_mem, Subalgebra.topologicalClosure, Subalgebra.smul_mem, Subalgebra.le_topologicalClosure, Subtype.property