awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
rw :
  (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜)) =
    closure (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) ∩
      (↑(RingHom.ker (F := C((↑s : Type u_1), 𝕜) →⋆ₐ[𝕜] 𝕜)
            (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
        Set C((↑s : Type u_1), 𝕜))
⊢ (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜)) =
    closure
      (↑(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 [← ker_evalStarAlgHom_inter_adjoin_id s h0,
    AlgHom.closure_ker_inter (φ := evalStarAlgHom 𝕜 𝕜 (X := s) ⟨0, h0⟩) (continuous_eval_const _) _]

Premises used: ContinuousMap.AlgHom.closure_ker_inter, Subtype.mk, ContinuousMap.evalStarAlgHom, ContinuousEvalConst.continuous_eval_const, ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
⊢ (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜)) =
    Set.univ ∩
      (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
            (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
        Set C((↑s : Type u_1), 𝕜))

Tactic:
(Set.univ_inter _).symm

Premises used: Set.univ_inter, Eq.symm
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
h : closure (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) = Set.univ
⊢ (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜)) =
    closure (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) ∩
      (↑(RingHom.ker (F := C((↑s : Type u_1), 𝕜) →⋆ₐ[𝕜] 𝕜)
            (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
        Set C((↑s : Type u_1), 𝕜))

Tactic:
convert! (Set.univ_inter _).symm

Premises used: Set.univ_inter, Eq.symm
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
h : closure (↑(Subalgebra.starClosure (polynomialFunctions s)) : Set C((↑s : Type u_1), 𝕜)) = Set.univ
⊢ closure (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) = Set.univ

Tactic:
rw [← Polynomial.toContinuousMapOn_X_eq_restrict_id, ← Polynomial.toContinuousMapOnAlgHom_apply,
    ← polynomialFunctions.starClosure_eq_adjoin_X s]

Premises used: Polynomial.toContinuousMapOn_X_eq_restrict_id, polynomialFunctions.starClosure_eq_adjoin_X, Polynomial.toContinuousMapOnAlgHom_apply
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
⊢ closure (↑(Subalgebra.starClosure (polynomialFunctions s)) : Set C((↑s : Type u_1), 𝕜)) = Set.univ

Tactic:
congrm (($(polynomialFunctions.starClosure_topologicalClosure s) : Set C(s, 𝕜)))
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
⊢ 0 ∈ s

Tactic:
have h0' : 0 ∈ s := Fact.out
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
h0' : 0 ∈ s
rw :
  Eq (α := Set C((↑s : Type u_1), 𝕜)₀)
    ((⇑toContinuousMapHom : (a : C((↑s : Type u_1), 𝕜)₀) → C((↑s : Type u_1), 𝕜)) ⁻¹'
      (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
            (ContinuousMap.evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0'))) :
        Set C((↑s : Type u_1), 𝕜)))
    Set.univ
⊢ Dense
    (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
          NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀) :
      Set C((↑s : Type u_1), 𝕜)₀)

Tactic:
rw [dense_iff_closure_eq,
    ← isClosedEmbedding_toContinuousMap.injective.preimage_image (closure _),
    ← isClosedEmbedding_toContinuousMap.closure_image_eq, ← coe_toContinuousMapHom,
    ← NonUnitalStarSubalgebra.coe_map, NonUnitalStarAlgHom.map_adjoin_singleton,
    toContinuousMapHom_apply, toContinuousMap_id,
    ← ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id s h0']

Premises used: ContinuousMapZero.toContinuousMap_id, dense_iff_closure_eq, Topology.IsClosedEmbedding.toIsEmbedding, NonUnitalStarSubalgebra.coe_map, NonUnitalStarAlgHom.map_adjoin_singleton, closure, Function.Injective.preimage_image, ContinuousMapZero.toContinuousMapHom_apply, Topology.IsEmbedding.injective, Topology.IsClosedEmbedding.closure_image_eq, ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id, ContinuousMapZero.coe_toContinuousMapHom, ContinuousMapZero.isClosedEmbedding_toContinuousMap
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
h0' : 0 ∈ s
apply :
  ∀ (f : C((↑s : Type u_1), 𝕜)₀),
    Membership.mem (γ := Set C((↑s : Type u_1), 𝕜)₀)
      ((⇑toContinuousMapHom : (a : C((↑s : Type u_1), 𝕜)₀) → C((↑s : Type u_1), 𝕜)) ⁻¹'
        (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
              (ContinuousMap.evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0'))) :
          Set C((↑s : Type u_1), 𝕜)))
      f
⊢ Eq (α := Set C((↑s : Type u_1), 𝕜)₀)
    ((⇑toContinuousMapHom : (a : C((↑s : Type u_1), 𝕜)₀) → C((↑s : Type u_1), 𝕜)) ⁻¹'
      (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
            (ContinuousMap.evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0'))) :
        Set C((↑s : Type u_1), 𝕜)))
    Set.univ

Tactic:
apply Set.eq_univ_of_forall fun f ↦ ?_

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
h0' : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)₀
simp : Eq (α := 𝕜) ((f : (a : { x : 𝕜 // x ∈ s }) → 𝕜) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0') : 𝕜) (0 : 𝕜)
⊢ Membership.mem (γ := Set C((↑s : Type u_1), 𝕜)₀)
    ((⇑toContinuousMapHom : (a : C((↑s : Type u_1), 𝕜)₀) → C((↑s : Type u_1), 𝕜)) ⁻¹'
      (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
            (ContinuousMap.evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0'))) :
        Set C((↑s : Type u_1), 𝕜)))
    f

Tactic:
simp only [Set.mem_preimage, toContinuousMapHom_apply, SetLike.mem_coe, RingHom.mem_ker,
    ContinuousMap.evalStarAlgHom_apply, ContinuousMap.coe_coe]

Premises used: RingHom.mem_ker, ContinuousMap.evalStarAlgHom_apply, SetLike.mem_coe, ContinuousMapZero.toContinuousMapHom_apply, ContinuousMap.coe_coe, Set.mem_preimage
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
h0' : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)₀
⊢ Eq (α := 𝕜) ((f : (a : { x : 𝕜 // x ∈ s }) → 𝕜) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0') : 𝕜) (0 : 𝕜)

Tactic:
map_zero f

Premises used: map_zero
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
h0' : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)₀
⊢ Eq (α := 𝕜) ((f : (a : { x : 𝕜 // x ∈ s }) → 𝕜) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0') : 𝕜) (0 : 𝕜)

Tactic:
exact map_zero f

Premises used: map_zero
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_2} (↑s : Type u_2)
⊢ Eq (α := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_2), 𝕜)₀)
    (elemental 𝕜 (A := C((↑s : Type u_2), 𝕜)₀) (ContinuousMapZero.id s) :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_2), 𝕜)₀)
    (⊤ : NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_2), 𝕜)₀)

Tactic:
SetLike.ext'_iff.mpr (adjoin_id_dense s).closure_eq

Premises used: Iff.mpr, Dense.closure_eq, SetLike.ext'_iff, ContinuousMapZero.adjoin_id_dense
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          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 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          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 (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
        (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
          NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
        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 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          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), 𝕜)₀) ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s}) f
⊢ f = ContinuousMapZero.id s ∨ star f = ContinuousMapZero.id s

Tactic:
push _ ∈ _ at hf
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f_2 f : C((↑s : Type u_1), 𝕜)₀
hf : f = ContinuousMapZero.id s ∨ star f = ContinuousMapZero.id s
⊢ f = ContinuousMapZero.id s ∨ star (ContinuousMapZero.id s) = f

Tactic:
rw [star_eq_iff_star_eq] at hf

Premises used: star_eq_iff_star_eq
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f_2 f : C((↑s : Type u_1), 𝕜)₀
hf : f = ContinuousMapZero.id s ∨ star (ContinuousMapZero.id s) = f
mem : p (ContinuousMapZero.id s)
mem₁ : p (star (ContinuousMapZero.id s))
⊢ p f

Tactic:
obtain (rfl | rfl) := hf

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f : C((↑s : Type u_1), 𝕜)₀
⊢ p (ContinuousMapZero.id s)

Tactic:
assumption
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f : C((↑s : Type u_1), 𝕜)₀
⊢ p (star (ContinuousMapZero.id s))

Tactic:
assumption
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f : C((↑s : Type u_1), 𝕜)₀
⊢ p 0

Tactic:
zero
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f : C((↑s : Type u_1), 𝕜)₀
⊢ p 0

Tactic:
exact zero
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f x y : C((↑s : Type u_1), 𝕜)₀
hx :
  Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
    (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) x
hy :
  Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
    (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) 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 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f x y : C((↑s : Type u_1), 𝕜)₀
hx :
  Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
    (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) x
hy :
  Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
    (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) 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 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f x y : C((↑s : Type u_1), 𝕜)₀
hx :
  Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
    (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) x
hy :
  Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
    (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) 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 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f x y : C((↑s : Type u_1), 𝕜)₀
hx :
  Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
    (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) x
hy :
  Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
    (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) 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 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f : C((↑s : Type u_1), 𝕜)₀
r : 𝕜
x : C((↑s : Type u_1), 𝕜)₀
hx :
  Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
    (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) x
hf : p x
⊢ p (r • x)

Tactic:
smul _ _ hf
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f : C((↑s : Type u_1), 𝕜)₀
r : 𝕜
x : C((↑s : Type u_1), 𝕜)₀
hx :
  Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
    (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) x
hf : p x
⊢ p (r • x)

Tactic:
exact smul _ _ hf