awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key :
  (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp { toFun := (⇑re : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
f_im : C(X, ℝ) := comp { toFun := (⇑im : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
h_f_re : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
⊢ Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))

Tactic:
have h_f_im : I f_im ∈ A.topologicalClosure := key ⟨f_im, rfl⟩
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key :
  (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp { toFun := (⇑re : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
f_im : C(X, ℝ) := comp { toFun := (⇑im : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
h_f_re : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
⊢ HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure.toSubalgebra

Tactic:
have := A.topologicalClosure.add_mem h_f_re (A.topologicalClosure.smul_mem h_f_im RCLike.I)
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key :
  (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp { toFun := (⇑re : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
f_im : C(X, ℝ) := comp { toFun := (⇑im : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
h_f_re : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
this :
  HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure.toSubalgebra
⊢ HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure

Tactic:
rw [StarSubalgebra.mem_toSubalgebra] at this

Premises used: StarSubalgebra.mem_toSubalgebra
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key :
  (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp { toFun := (⇑re : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
f_im : C(X, ℝ) := comp { toFun := (⇑im : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
h_f_re : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
this :
  HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure
⊢ HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure

Tactic:
this
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key :
  (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp { toFun := (⇑re : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
f_im : C(X, ℝ) := comp { toFun := (⇑im : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
h_f_re : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
this :
  HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure
h :
  f =
    HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜)))
⊢ f ∈ A.topologicalClosure

Tactic:
convert! this
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key :
  (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp { toFun := (⇑re : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
f_im : C(X, ℝ) := comp { toFun := (⇑im : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
h_f_re : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
this :
  HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure
h :
  ∀ (a : X),
    Eq.{u_1 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) a : 𝕜)
      ((HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
              (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) :
            (a : X) → 𝕜)
          a :
        𝕜)
⊢ f =
    HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜)))

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key :
  (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp { toFun := (⇑re : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
f_im : C(X, ℝ) := comp { toFun := (⇑im : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
h_f_re : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
this :
  HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure
a : X
h :
  Eq.{u_1 + 1} (α := 𝕜)
    ((HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
            (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) :
          (a : X) → 𝕜)
        a :
      𝕜)
    ((f : (a : X) → 𝕜) a : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) a : 𝕜)
    ((HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
            (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) :
          (a : X) → 𝕜)
        a :
      𝕜)

Tactic:
apply Eq.symm

Premises used: Eq.symm
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key :
  (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp { toFun := (⇑re : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
f_im : C(X, ℝ) := comp { toFun := (⇑im : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
h_f_re : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
this :
  HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure
a : X
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
            (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) :
          (a : X) → 𝕜)
        a :
      𝕜)
    ((f : (a : X) → 𝕜) a : 𝕜)

Tactic:
simp [I, f_re, f_im, mul_comm RCLike.I _]

Premises used: RCLike.I, mul_comm
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
s : Set ℝ
inst : CompactSpace (↑s : Type)
⊢ Eq (α := Subalgebra ℝ C((↑s : Type), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions s)) ⊤

Tactic:
ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints _
    (polynomialFunctions_separatesPoints s)

Premises used: polynomialFunctions_separatesPoints, ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
⊢ Eq (α := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (StarSubalgebra.topologicalClosure (Subalgebra.starClosure (polynomialFunctions s))) ⊤

Tactic:
ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints _
    (Subalgebra.separatesPoints_monotone le_sup_left (polynomialFunctions_separatesPoints s))

Premises used: polynomialFunctions_separatesPoints, le_sup_left, Subalgebra.separatesPoints_monotone, ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
rw :
  Eq (α := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (topologicalClosure (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}))
    (topologicalClosure
      (adjoin 𝕜
        (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
⊢ Eq (α := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (elemental 𝕜 (restrict s (ContinuousMap.id 𝕜))) ⊤

Tactic:
rw [StarAlgebra.elemental, ← polynomialFunctions.starClosure_topologicalClosure,
    polynomialFunctions.starClosure_eq_adjoin_X]

Premises used: polynomialFunctions.starClosure_topologicalClosure, polynomialFunctions.starClosure_eq_adjoin_X, StarAlgebra.elemental
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
e_s : Eq (α := C(𝕜, 𝕜)) (ContinuousMap.id 𝕜) (Polynomial.toContinuousMap X)
⊢ Eq (α := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (topologicalClosure (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}))
    (topologicalClosure
      (adjoin 𝕜
        (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))

Tactic:
congr
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
⊢ Eq (α := C(𝕜, 𝕜)) (ContinuousMap.id 𝕜) (Polynomial.toContinuousMap X)

Tactic:
Polynomial.toContinuousMap_X_eq_id.symm

Premises used: Polynomial.toContinuousMap_X_eq_id, Eq.symm
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
⊢ Eq (α := C(𝕜, 𝕜)) (ContinuousMap.id 𝕜) (Polynomial.toContinuousMap X)

Tactic:
exact Polynomial.toContinuousMap_X_eq_id.symm

Premises used: Polynomial.toContinuousMap_X_eq_id, Eq.symm
-- 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 : C((↑s : Type u_1), 𝕜)
⊢ p f

Tactic:
closure (fun f hf => ?_) f
-- 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 : C((↑s : Type u_1), 𝕜)
refine :
  ∀ (f : C((↑s : Type u_1), 𝕜))
    (hf :
      Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f),
    p f
⊢ p f

Tactic:
refine closure (fun f hf => ?_) f
-- 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 : C((↑s : Type u_1), 𝕜)
hf : Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f
⊢ Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (StarAlgebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
        ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜))))
    f

Tactic:
rw [polynomialFunctions.starClosure_eq_adjoin_X] at hf

Premises used: polynomialFunctions.starClosure_eq_adjoin_X
-- 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_2 f : C((↑s : Type u_1), 𝕜)
hf :
  Membership.mem (γ := Set C((↑s : Type u_1), 𝕜))
    (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), 𝕜))))
    f
⊢ f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X ∨
    star f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X

Tactic:
push _ ∈ _ at hf
-- 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_2 f : C((↑s : Type u_1), 𝕜)
hf :
  f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X ∨
    star f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X
⊢ f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X ∨
    f = star ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X)

Tactic:
rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf

Premises used: eq_comm, star_eq_iff_star_eq
-- 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_2 f : C((↑s : Type u_1), 𝕜)
hf :
  f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X ∨
    f = star ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X)
mem : p ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X)
mem₁ : p (star ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X))
⊢ p f

Tactic:
obtain (rfl | rfl) := hf

Premises used: rfl
-- 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 : C((↑s : Type u_1), 𝕜)
⊢ p ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X)

Tactic:
simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]

Premises used: Polynomial.toContinuousMapOn_X_eq_restrict_id, Polynomial.toContinuousMapOnAlgHom_apply
-- 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 : C((↑s : Type u_1), 𝕜)
⊢ p (star ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X))

Tactic:
simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]

Premises used: Polynomial.toContinuousMapOn_X_eq_restrict_id, Polynomial.toContinuousMapOnAlgHom_apply
-- 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 : C((↑s : Type u_1), 𝕜)
r : 𝕜
⊢ p ((algebraMap 𝕜 C((↑s : Type u_1), 𝕜) : (a : 𝕜) → C((↑s : Type u_1), 𝕜)) r)

Tactic:
const r

Premises used: ContinuousMap.const
-- 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 : C((↑s : Type u_1), 𝕜)
r : 𝕜
⊢ p ((algebraMap 𝕜 C((↑s : Type u_1), 𝕜) : (a : 𝕜) → C((↑s : Type u_1), 𝕜)) r)

Tactic:
exact const r