awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
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)
closure :
  (∀ (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), 𝕜)), p f
f_1 f x y : C((↑s : Type u_1), 𝕜)
hx :
  Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (Algebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
        star
          (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
    x
hy :
  Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (Algebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
        star
          (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
    y
hf : p x
hg : p y
⊢ p (x + y)

Tactic:
add _ _ hf hg
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
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)
closure :
  (∀ (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), 𝕜)), p f
f_1 f x y : C((↑s : Type u_1), 𝕜)
hx :
  Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (Algebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
        star
          (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
    x
hy :
  Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (Algebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
        star
          (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
    y
hf : p x
hg : p y
⊢ p (x + y)

Tactic:
exact add _ _ hf hg
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
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)
closure :
  (∀ (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), 𝕜)), p f
f_1 f x y : C((↑s : Type u_1), 𝕜)
hx :
  Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (Algebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
        star
          (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
    x
hy :
  Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (Algebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
        star
          (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
    y
hf : p x
hg : p y
⊢ p (x * y)

Tactic:
mul _ _ hf hg
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
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)
closure :
  (∀ (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), 𝕜)), p f
f_1 f x y : C((↑s : Type u_1), 𝕜)
hx :
  Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (Algebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
        star
          (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
    x
hy :
  Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (Algebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
        star
          (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
    y
hf : p x
hg : p y
⊢ p (x * y)

Tactic:
exact mul _ _ hf hg
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 : C((↑s : Type u_1), 𝕜)
⊢ p f

Tactic:
f.induction_on const id star_id add mul fun h f ↦ frequently f ?_

Premises used: ContinuousMap.induction_on
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 : C((↑s : Type u_1), 𝕜)
refine :
  ∀
    (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), 𝕜)), ∃ᶠ (g : C((↑s : Type u_1), 𝕜)) in 𝓝 f, p g
⊢ p f

Tactic:
refine f.induction_on const id star_id add mul fun h f ↦ frequently f ?_
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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), 𝕜)
⊢ Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (topologicalClosure (Subalgebra.starClosure (polynomialFunctions s))) f

Tactic:
have := polynomialFunctions.starClosure_topologicalClosure s ▸ mem_top (x := f)
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
⊢ ∃ᶠ (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

Premises used: mem_closure_iff_frequently, StarSubalgebra.topologicalClosure_coe, SetLike.mem_coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 :
  ∃ᶠ (x : C((↑s : Type u_1), 𝕜)) in 𝓝 f,
    x ∈ (↑(Subalgebra.starClosure (polynomialFunctions s)) : Set C((↑s : Type u_1), 𝕜))
⊢ ∃ᶠ (g : C((↑s : Type u_1), 𝕜)) in 𝓝 f, p g

Tactic:
this.mp <| .of_forall h

Premises used: Filter.Eventually.of_forall, Filter.Frequently.mp
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 :
  ∃ᶠ (x : C((↑s : Type u_1), 𝕜)) in 𝓝 f,
    x ∈ (↑(Subalgebra.starClosure (polynomialFunctions s)) : Set C((↑s : Type u_1), 𝕜))
⊢ ∃ᶠ (g : C((↑s : Type u_1), 𝕜)) in 𝓝 f, p g

Tactic:
exact this.mp <| .of_forall h

Premises used: Filter.Frequently.mp
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
this : LE.le (α := Subalgebra ℝ C((↑s : Type), ℝ)) ⊤ (AlgHom.equalizer φ ψ)
x : C((↑s : Type), ℝ)
⊢ Membership.mem (γ := Subalgebra ℝ C((↑s : Type), ℝ)) ⊤ x

Tactic:
trivial
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
suffices : LE.le (α := Subalgebra ℝ C((↑s : Type), ℝ)) ⊤ (AlgHom.equalizer φ ψ)
⊢ φ = ψ

Tactic:
suffices (⊤ : Subalgebra ℝ C(s, ℝ)) ≤ AlgHom.equalizer φ ψ from
    AlgHom.ext fun x => this (by trivial)
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
rw :
  LE.le (α := Subalgebra ℝ C((↑s : Type), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions s))
    (AlgHom.equalizer φ ψ)
⊢ LE.le (α := Subalgebra ℝ C((↑s : Type), ℝ)) ⊤ (AlgHom.equalizer φ ψ)

Tactic:
rw [← polynomialFunctions.topologicalClosure s]

Premises used: polynomialFunctions.topologicalClosure
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions s))
    (AlgHom.equalizer φ ψ)

Tactic:
Subalgebra.topologicalClosure_minimal
    (polynomialFunctions.le_equalizer s φ ψ h) (isClosed_eq hφ hψ)

Premises used: polynomialFunctions.le_equalizer, Set.Mem, Subalgebra.topologicalClosure_minimal, isClosed_eq
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions s))
    (AlgHom.equalizer φ ψ)

Tactic:
exact Subalgebra.topologicalClosure_minimal
    (polynomialFunctions.le_equalizer s φ ψ h) (isClosed_eq hφ hψ)

Premises used: polynomialFunctions.le_equalizer, Subalgebra.topologicalClosure_minimal, isClosed_eq
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
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
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
rw :
  LE.le (α := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (topologicalClosure (Subalgebra.starClosure (polynomialFunctions s))) (StarAlgHom.equalizer φ ψ)
⊢ LE.le (α := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) ⊤ (StarAlgHom.equalizer φ ψ)

Tactic:
rw [← polynomialFunctions.starClosure_topologicalClosure s]

Premises used: polynomialFunctions.starClosure_topologicalClosure
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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), 𝕜))
    (topologicalClosure (Subalgebra.starClosure (polynomialFunctions s))) (StarAlgHom.equalizer φ ψ)

Tactic:
StarSubalgebra.topologicalClosure_minimal
    (polynomialFunctions.starClosure_le_equalizer s φ ψ h) (isClosed_eq hφ hψ)

Premises used: Set.Mem, polynomialFunctions.starClosure_le_equalizer, isClosed_eq, StarSubalgebra.topologicalClosure_minimal
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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), 𝕜))
    (topologicalClosure (Subalgebra.starClosure (polynomialFunctions s))) (StarAlgHom.equalizer φ ψ)

Tactic:
exact StarSubalgebra.topologicalClosure_minimal
    (polynomialFunctions.starClosure_le_equalizer s φ ψ h) (isClosed_eq hφ hψ)

Premises used: polynomialFunctions.starClosure_le_equalizer, isClosed_eq, StarSubalgebra.topologicalClosure_minimal
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
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), 𝕜))
⊢ (↑(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), 𝕜))

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
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), 𝕜))
⊢ (↑(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), 𝕜))

Tactic:
ext x