awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f * g)
frequently : ∀ (f : C((↑s : Type u_1), 𝕜)), (∃ᶠ (g : C((↑s : Type u_1), 𝕜)) in 𝓝 f, p g) → p f
f_1 : C((↑s : Type u_1), 𝕜)
h :
  ∀ (f : C((↑s : Type u_1), 𝕜)),
    Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
      p f
f : C((↑s : Type u_1), 𝕜)
this :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (topologicalClosure (Subalgebra.starClosure (polynomialFunctions s))) f
⊢ ∃ᶠ (g : C((↑s : Type u_1), 𝕜)) in 𝓝 f, p g
have this₁ : ∃ᶠ (x : C((↑s : Type u_1), 𝕜)) in 𝓝 f,
  x ∈ (↑(Subalgebra.starClosure (polynomialFunctions s)) : Set C((↑s : Type u_1), 𝕜))
Tactic: rw [← SetLike.mem_coe, topologicalClosure_coe, mem_closure_iff_frequently] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
A : Type u_1
inst : Semiring A
inst_1 : Algebra ℝ A
inst_2 : TopologicalSpace A
inst_3 : T2Space A
s : Set ℝ
inst_4 : CompactSpace (↑s : Type)
φ ψ : C((↑s : Type), ℝ) →ₐ[ℝ] A
hφ : Continuous (X := C((↑s : Type), ℝ)) (Y := A) (⇑φ : (a : C((↑s : Type), ℝ)) → A)
hψ : Continuous (X := C((↑s : Type), ℝ)) (Y := A) (⇑ψ : (a : C((↑s : Type), ℝ)) → A)
h :
  Eq (α := A)
    ((φ : (a : C((↑s : Type), ℝ)) → A)
        ((toContinuousMapOnAlgHom s : (a : ℝ[X]) → C((↑s : Type), ℝ)) X : C((↑s : Type), ℝ)) :
      A)
    ((ψ : (a : C((↑s : Type), ℝ)) → A)
        ((toContinuousMapOnAlgHom s : (a : ℝ[X]) → C((↑s : Type), ℝ)) X : C((↑s : Type), ℝ)) :
      A)
⊢ φ = ψ
have suffices : LE.le (α := Subalgebra ℝ C((↑s : Type), ℝ)) ⊤ (AlgHom.equalizer φ ψ)
Tactic: suffices (⊤ : Subalgebra ℝ C(s, ℝ)) ≤ AlgHom.equalizer φ ψ from
    AlgHom.ext fun x => this (by trivial)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
A : Type u_1
inst : Semiring A
inst_1 : Algebra ℝ A
inst_2 : TopologicalSpace A
inst_3 : T2Space A
s : Set ℝ
inst_4 : CompactSpace (↑s : Type)
φ ψ : C((↑s : Type), ℝ) →ₐ[ℝ] A
hφ : Continuous (X := C((↑s : Type), ℝ)) (Y := A) (⇑φ : (a : C((↑s : Type), ℝ)) → A)
hψ : Continuous (X := C((↑s : Type), ℝ)) (Y := A) (⇑ψ : (a : C((↑s : Type), ℝ)) → A)
h :
  Eq (α := A)
    ((φ : (a : C((↑s : Type), ℝ)) → A)
        ((toContinuousMapOnAlgHom s : (a : ℝ[X]) → C((↑s : Type), ℝ)) X : C((↑s : Type), ℝ)) :
      A)
    ((ψ : (a : C((↑s : Type), ℝ)) → A)
        ((toContinuousMapOnAlgHom s : (a : ℝ[X]) → C((↑s : Type), ℝ)) X : C((↑s : Type), ℝ)) :
      A)
⊢ LE.le (α := Subalgebra ℝ C((↑s : Type), ℝ)) ⊤ (AlgHom.equalizer φ ψ)
have rw : LE.le (α := Subalgebra ℝ C((↑s : Type), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions s))
  (AlgHom.equalizer φ ψ)
Tactic: rw [← polynomialFunctions.topologicalClosure s]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : T2Space A
s : Set 𝕜
inst_6 : CompactSpace.{u_1} (↑s : Type u_1)
φ ψ : C((↑s : Type u_1), 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous.{u_1, u_2} (X := C((↑s : Type u_1), 𝕜)) (Y := A) (⇑φ : (a : C((↑s : Type u_1), 𝕜)) → A)
hψ : Continuous.{u_1, u_2} (X := C((↑s : Type u_1), 𝕜)) (Y := A) (⇑ψ : (a : C((↑s : Type u_1), 𝕜)) → A)
h :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑s : Type u_1), 𝕜)) → A)
        ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) :
      A)
    ((ψ : (a : C((↑s : Type u_1), 𝕜)) → A)
        ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) :
      A)
⊢ φ = ψ
have suffices : LE.le (α := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) ⊤ (StarAlgHom.equalizer φ ψ)
Tactic: suffices (⊤ : StarSubalgebra 𝕜 C(s, 𝕜)) ≤ StarAlgHom.equalizer φ ψ from
    StarAlgHom.ext fun x => this mem_top
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra 𝕜 A
inst_4 : TopologicalSpace A
inst_5 : T2Space A
s : Set 𝕜
inst_6 : CompactSpace.{u_1} (↑s : Type u_1)
φ ψ : C((↑s : Type u_1), 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous.{u_1, u_2} (X := C((↑s : Type u_1), 𝕜)) (Y := A) (⇑φ : (a : C((↑s : Type u_1), 𝕜)) → A)
hψ : Continuous.{u_1, u_2} (X := C((↑s : Type u_1), 𝕜)) (Y := A) (⇑ψ : (a : C((↑s : Type u_1), 𝕜)) → A)
h :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑s : Type u_1), 𝕜)) → A)
        ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) :
      A)
    ((ψ : (a : C((↑s : Type u_1), 𝕜)) → A)
        ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) :
      A)
⊢ LE.le (α := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) ⊤ (StarAlgHom.equalizer φ ψ)
have rw : LE.le (α := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
  (topologicalClosure (Subalgebra.starClosure (polynomialFunctions s))) (StarAlgHom.equalizer φ ψ)
Tactic: rw [← polynomialFunctions.starClosure_topologicalClosure s]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
⊢ (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) =
    (↑(span 𝕜
          ({1} ∪
            (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                  NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
              Set C((↑s : Type u_1), 𝕜)))) :
      Set C((↑s : Type u_1), 𝕜))
have h : ∀ (x : C((↑s : Type u_1), 𝕜)),
  x ∈ (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) ↔
    x ∈
      (↑(span 𝕜
            ({1} ∪
              (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                    NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
                Set C((↑s : Type u_1), 𝕜)))) :
        Set C((↑s : Type u_1), 𝕜))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
x : C((↑s : Type u_1), 𝕜)
⊢ x ∈ (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) ↔
    x ∈
      (↑(span 𝕜
            ({1} ∪
              (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                    NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
                Set C((↑s : Type u_1), 𝕜)))) :
        Set C((↑s : Type u_1), 𝕜))
have h : Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
    x ↔
  x ∈
    (↑(span 𝕜
          ({1} ∪
            (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                  NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
              Set C((↑s : Type u_1), 𝕜)))) :
      Set C((↑s : Type u_1), 𝕜))
Tactic: rw [SetLike.mem_coe, SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
    ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
    StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_union, span_eq_toSubmodule]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
x : C((↑s : Type u_1), 𝕜)
h :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
      x ↔
    x ∈
      (↑(span 𝕜
            ({1} ∪
              (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                    NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
                Set C((↑s : Type u_1), 𝕜)))) :
        Set C((↑s : Type u_1), 𝕜))
⊢ x ∈ (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) ↔
    x ∈
      (↑(span 𝕜
            ({1} ∪
              (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                    NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
                Set C((↑s : Type u_1), 𝕜)))) :
        Set C((↑s : Type u_1), 𝕜))
have h₁ : Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
    x ↔
  Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
    (span 𝕜
      ({1} ∪
        (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
              NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
          Set C((↑s : Type u_1), 𝕜))))
    x
Tactic: rw [SetLike.mem_coe, SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
    ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
    StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_union, span_eq_toSubmodule]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
x : C((↑s : Type u_1), 𝕜)
h :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
      x ↔
    x ∈
      (↑(span 𝕜
            ({1} ∪
              (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                    NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
                Set C((↑s : Type u_1), 𝕜)))) :
        Set C((↑s : Type u_1), 𝕜))
h₁ :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
      x ↔
    Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      (span 𝕜
        ({1} ∪
          (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
            Set C((↑s : Type u_1), 𝕜))))
      x
⊢ x ∈ (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) ↔
    x ∈
      (↑(span 𝕜
            ({1} ∪
              (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                    NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
                Set C((↑s : Type u_1), 𝕜)))) :
        Set C((↑s : Type u_1), 𝕜))
have h₂ : Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (StarAlgebra.adjoin 𝕜
      (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
        Set C((↑s : Type u_1), 𝕜)))
    x ↔
  Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
    (span 𝕜
      ({1} ∪
        (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
              NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
          Set C((↑s : Type u_1), 𝕜))))
    x
Tactic: rw [SetLike.mem_coe, SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
    ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
    StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_union, span_eq_toSubmodule]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
x : C((↑s : Type u_1), 𝕜)
h :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
      x ↔
    x ∈
      (↑(span 𝕜
            ({1} ∪
              (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                    NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
                Set C((↑s : Type u_1), 𝕜)))) :
        Set C((↑s : Type u_1), 𝕜))
h₁ :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
      x ↔
    Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      (span 𝕜
        ({1} ∪
          (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
            Set C((↑s : Type u_1), 𝕜))))
      x
h₂ :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
      (StarAlgebra.adjoin 𝕜
        (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
              NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
          Set C((↑s : Type u_1), 𝕜)))
      x ↔
    Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      (span 𝕜
        ({1} ∪
          (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
            Set C((↑s : Type u_1), 𝕜))))
      x
⊢ x ∈ (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) ↔
    x ∈
      (↑(span 𝕜
            ({1} ∪
              (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                    NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
                Set C((↑s : Type u_1), 𝕜)))) :
        Set C((↑s : Type u_1), 𝕜))
have h₃ : Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (StarSubalgebra.toSubalgebra
      (StarAlgebra.adjoin 𝕜
        (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
              NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
          Set C((↑s : Type u_1), 𝕜))))
    x ↔
  Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
    (span 𝕜
      ({1} ∪
        (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
              NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
          Set C((↑s : Type u_1), 𝕜))))
    x
Tactic: rw [SetLike.mem_coe, SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
    ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
    StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_union, span_eq_toSubmodule]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
⊢ (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) =
    (↑(𝕜 ∙ 1) : Set C((↑s : Type u_1), 𝕜)) +
      (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
        Set C((↑s : Type u_1), 𝕜))
have h : ∀ (x : C((↑s : Type u_1), 𝕜)),
  x ∈ (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) ↔
    x ∈
      (↑(𝕜 ∙ 1) : Set C((↑s : Type u_1), 𝕜)) +
        (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
              NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
          Set C((↑s : Type u_1), 𝕜))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
x : C((↑s : Type u_1), 𝕜)
⊢ x ∈ (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) ↔
    x ∈
      (↑(𝕜 ∙ 1) : Set C((↑s : Type u_1), 𝕜)) +
        (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
              NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
          Set C((↑s : Type u_1), 𝕜))
have h : (∃ (y : C((↑s : Type u_1), 𝕜)),
    Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜)) (𝕜 ∙ 1) y ∧
      ∃ (z : C((↑s : Type u_1), 𝕜)),
        Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
            (NonUnitalSubalgebra.toSubmodule
                (NonUnitalStarSubalgebra.toNonUnitalSubalgebra
                  (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)})) :
              Submodule 𝕜 C((↑s : Type u_1), 𝕜))
            z ∧
          y + z = x) ↔
  x ∈
    (↑(𝕜 ∙ 1) : Set C((↑s : Type u_1), 𝕜)) +
      (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
        Set C((↑s : Type u_1), 𝕜))
Tactic: rw [SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
    ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
    StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, mem_sup]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f_1 f : C((↑s : Type u_1), 𝕜)
hf : Membership.mem (γ := Set C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} f
⊢ f ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
have mem : ∀
  (hf :
    Membership.mem (γ := Set C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)}
      (restrict s (ContinuousMap.id 𝕜))),
  restrict s (ContinuousMap.id 𝕜) ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
Tactic: obtain rfl := Set.mem_singleton_iff.mp hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f_1 : C((↑s : Type u_1), 𝕜)
r : 𝕜
f : C((↑s : Type u_1), 𝕜)
hx :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    f
hf :
  f ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
⊢ r • f ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
have smul : ∀
  (hf :
    Eq (α := 𝕜)
      ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) f : 𝕜)
      (0 : 𝕜)),
  Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) (r • f) : 𝕜)
    (0 : 𝕜)
Tactic: rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f_1 : C((↑s : Type u_1), 𝕜)
r : 𝕜
f : C((↑s : Type u_1), 𝕜)
hx :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    f
hf :
  Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) f : 𝕜) (0 : 𝕜)
⊢ Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) (r • f) : 𝕜)
    (0 : 𝕜)
have smul : HSMul.hSMul (β := 𝕜) r
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) f : 𝕜) =
  0
Tactic: rw [map_smul, hf, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f_1 : C((↑s : Type u_1), 𝕜)
r : 𝕜
f : C((↑s : Type u_1), 𝕜)
hx :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    f
hf :
  Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) f : 𝕜) (0 : 𝕜)
smul :
  HSMul.hSMul (β := 𝕜) r
      ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) f : 𝕜) =
    0
⊢ Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) (r • f) : 𝕜)
    (0 : 𝕜)
have smul₁ : HSMul.hSMul (β := 𝕜) r 0 = 0
Tactic: rw [map_smul, hf, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f_1 : C((↑s : Type u_1), 𝕜)
r : 𝕜
f : C((↑s : Type u_1), 𝕜)
hx :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    f
hf :
  Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) f : 𝕜) (0 : 𝕜)
smul :
  HSMul.hSMul (β := 𝕜) r
      ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) f : 𝕜) =
    0
smul₁ : HSMul.hSMul (β := 𝕜) r 0 = 0
⊢ Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) (r • f) : 𝕜)
    (0 : 𝕜)
have smul₂ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [map_smul, hf, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f_1 f : C((↑s : Type u_1), 𝕜)
hx :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    f
hf :
  f ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
⊢ star f ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
have star : ∀
  (hf :
    Eq (α := 𝕜)
      ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) f : 𝕜)
      (0 : 𝕜)),
  Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) (star f) : 𝕜)
    (0 : 𝕜)
Tactic: rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f_1 f : C((↑s : Type u_1), 𝕜)
hx :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    f
hf :
  Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) f : 𝕜) (0 : 𝕜)
⊢ Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) (star f) : 𝕜)
    (0 : 𝕜)
have star : Eq (α := 𝕜)
  (star ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) f) : 𝕜)
  (0 : 𝕜)
Tactic: rw [map_star, hf, star_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f_1 f : C((↑s : Type u_1), 𝕜)
hx :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    f
hf :
  Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) f : 𝕜) (0 : 𝕜)
star :
  Eq (α := 𝕜)
    (Star.star ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) f) :
      𝕜)
    (0 : 𝕜)
⊢ Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) (Star.star f) :
      𝕜)
    (0 : 𝕜)
have star₁ : Eq.{u_1 + 1} (α := 𝕜) (Star.star 0) 0
Tactic: rw [map_star, hf, star_zero]