awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
x : C((↑s : Type u_1), 𝕜)
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), 𝕜))
⊢ 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:
rw [SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
    ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
    StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, mem_sup]

Premises used: StarSubalgebra.mem_toSubalgebra, StarAlgebra.adjoin_nonUnitalStarSubalgebra, Subalgebra.mem_toSubmodule, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, SetLike.mem_coe, Submodule.mem_sup
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
x : C((↑s : Type u_1), 𝕜)
⊢ (∃ (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:
simp [Set.mem_add]

Premises used: Set.mem_add
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
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), 𝕜))
⊢ f ∈
    (↑(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

Premises used: Set.mem_singleton_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)
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:
rfl
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f_1 f g : 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
hy :
  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), 𝕜))
    g
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), 𝕜))
hg :
  g ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
⊢ f + g ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))

Tactic:
add_mem hf hg

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f_1 f g : 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
hy :
  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), 𝕜))
    g
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), 𝕜))
hg :
  g ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
⊢ f + g ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))

Tactic:
exact add_mem hf hg

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)
⊢ 0 ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)
⊢ 0 ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f_1 f g : 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
hy :
  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), 𝕜))
    g
h :
  f ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
hg :
  g ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
⊢ f * g ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))

Tactic:
Ideal.mul_mem_left _ f hg

Premises used: Set.Mem, Ideal.mul_mem_left
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f_1 f g : 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
hy :
  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), 𝕜))
    g
h :
  f ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
hg :
  g ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
⊢ f * g ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))

Tactic:
exact Ideal.mul_mem_left _ f hg

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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), 𝕜))
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 : 𝕜)
⊢ 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), 𝕜))

Tactic:
rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢

Premises used: RingHom.mem_ker, SetLike.mem_coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
smul₂ smul₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) (r • f) : 𝕜)
    (0 : 𝕜)

Tactic:
rw [map_smul, hf, smul_zero]

Premises used: smul_zero, map_smul
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 :
  ∀
    (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.star f) :
        𝕜)
      (0 : 𝕜)
⊢ Star.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), 𝕜))

Tactic:
rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢

Premises used: RingHom.mem_ker, SetLike.mem_coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 : 𝕜)
star₁ : Eq.{u_1 + 1} (α := 𝕜) (Star.star 0) 0
star₂ star₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) (Star.star f) :
      𝕜)
    (0 : 𝕜)

Tactic:
rw [map_star, hf, star_zero]

Premises used: StarHomClass.map_star, star_zero
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
h :
  ∀ (f : C((↑s : Type u_1), 𝕜)),
    f ∈
        (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : 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), 𝕜)) ↔
      f ∈
        (↑(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), 𝕜)) ∩
      (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
            (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
        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 f
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)
h :
  f ∈
      (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : 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), 𝕜)) →
    f ∈
      (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
        Set C((↑s : Type u_1), 𝕜))
h₁ :
  f ∈
      (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
        Set C((↑s : Type u_1), 𝕜)) →
    f ∈
      (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : 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), 𝕜))
⊢ f ∈
      (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : 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), 𝕜)) ↔
    f ∈
      (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
        Set C((↑s : Type u_1), 𝕜))

Tactic:
constructor
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)
hf₁ : f ∈ (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜))
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), 𝕜))
⊢ Membership.mem (γ := Ideal C({ x : 𝕜 // x ∈ s }, 𝕜))
    (RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
      (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0)))
    f

Tactic:
rw [SetLike.mem_coe] at hf₂ ⊢

Premises used: SetLike.mem_coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)
hf₁ : f ∈ (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜))
hf₂ :
  Membership.mem (γ := Ideal C({ x : 𝕜 // x ∈ s }, 𝕜))
    (RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
      (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0)))
    f
⊢ ∃ (x : C((↑s : Type u_1), 𝕜)),
    (∃ (a : 𝕜), HSMul.hSMul (β := C((↑s : Type u_1), 𝕜)) a 1 = x) ∧
      ∃ (y : C((↑s : Type u_1), 𝕜)),
        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), 𝕜))
            y ∧
          x + y = f

Tactic:
simp_rw [adjoin_id_eq_span_one_add, Set.mem_add, SetLike.mem_coe, mem_span_singleton] at hf₁

Premises used: Submodule.mem_span_singleton, SetLike.mem_coe, ContinuousMap.adjoin_id_eq_span_one_add, Set.mem_add
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)
hf₂ :
  Membership.mem (γ := Ideal C({ x : 𝕜 // x ∈ s }, 𝕜))
    (RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
      (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0)))
    f
hf₁ :
  ∃ (x : C((↑s : Type u_1), 𝕜)),
    (∃ (a : 𝕜), HSMul.hSMul (β := C((↑s : Type u_1), 𝕜)) a 1 = x) ∧
      ∃ (y : C((↑s : Type u_1), 𝕜)),
        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), 𝕜))
            y ∧
          x + y = f
h :
  ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜))
    (hf :
      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₂ :
      Membership.mem (γ := Ideal C({ x : 𝕜 // x ∈ s }, 𝕜))
        (RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0)))
        (HSMul.hSMul (β := C((↑s : Type u_1), 𝕜)) r 1 + f)),
    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), 𝕜))
      (HSMul.hSMul (β := C((↑s : Type u_1), 𝕜)) r 1 + f)
⊢ 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

Tactic:
obtain ⟨-, ⟨r, rfl⟩, f, hf, rfl⟩ := hf₁

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C((↑s : Type u_1), 𝕜)
hf :
  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₂ :
  Membership.mem (γ := Ideal C({ x : 𝕜 // x ∈ s }, 𝕜))
    (RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
      (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0)))
    (HSMul.hSMul (β := C((↑s : Type u_1), 𝕜)) r 1 + 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), 𝕜))

Tactic:
have := nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C((↑s : Type u_1), 𝕜)
hf :
  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₂ :
  Membership.mem (γ := Ideal C({ x : 𝕜 // x ∈ s }, 𝕜))
    (RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
      (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0)))
    (HSMul.hSMul (β := C((↑s : Type u_1), 𝕜)) r 1 + f)
this :
  f ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
⊢ Eq (α := 𝕜)
    ((HSMul.hSMul (β := C((↑s : Type u_1), 𝕜)) r 1 + f : (a : { x : 𝕜 // x ∈ s }) → 𝕜)
        (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) :
      𝕜)
    (0 : 𝕜)

Tactic:
simp only [SetLike.mem_coe, RingHom.mem_ker, evalStarAlgHom_apply] at hf₂ this

Premises used: RingHom.mem_ker, ContinuousMap.evalStarAlgHom_apply, SetLike.mem_coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C((↑s : Type u_1), 𝕜)
hf :
  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₂ :
  Membership.mem (γ := Ideal C({ x : 𝕜 // x ∈ s }, 𝕜))
    (RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
      (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0)))
    (HSMul.hSMul (β := C((↑s : Type u_1), 𝕜)) r 1 + f)
this :
  f ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
hf₃ :
  Eq (α := 𝕜)
    ((HSMul.hSMul (β := C((↑s : Type u_1), 𝕜)) r 1 + f : (a : { x : 𝕜 // x ∈ s }) → 𝕜)
        (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) :
      𝕜)
    (0 : 𝕜)
⊢ Eq (α := 𝕜) ((f : (a : { x : 𝕜 // x ∈ s }) → 𝕜) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : 𝕜) (0 : 𝕜)

Tactic:
simp only [SetLike.mem_coe, RingHom.mem_ker, evalStarAlgHom_apply] at hf₂ this

Premises used: RingHom.mem_ker, ContinuousMap.evalStarAlgHom_apply, SetLike.mem_coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C((↑s : Type u_1), 𝕜)
hf :
  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 (α := 𝕜)
    ((HSMul.hSMul (β := C((↑s : Type u_1), 𝕜)) r 1 + f : (a : { x : 𝕜 // x ∈ s }) → 𝕜)
        (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) :
      𝕜)
    (0 : 𝕜)
this : Eq (α := 𝕜) ((f : (a : { x : 𝕜 // x ∈ s }) → 𝕜) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : 𝕜) (0 : 𝕜)
⊢ r = 0

Tactic:
rw [add_apply, this, add_zero, smul_apply, one_apply, smul_eq_mul, mul_one] at hf₂

Premises used: ContinuousMap.smul_apply, ContinuousMap.one_apply, ContinuousMap.add_apply, smul_eq_mul, mul_one, add_zero