-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)
hf :
  f ∈
    (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
          NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
      Set C((↑s : Type u_1), 𝕜))
mem :
  ∀ (f : C((↑s : Type u_1), 𝕜))
    (hf : Membership.mem (γ := Set C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} f),
    f ∈
      (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
            (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
        Set C((↑s : Type u_1), 𝕜))
add :
  ∀ (f g : 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), 𝕜))
        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), 𝕜))
          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), 𝕜))
zero :
  0 ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
mul :
  ∀ (f g : 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), 𝕜))
        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), 𝕜))
          g →
        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), 𝕜))
smul :
  ∀ (r : 𝕜) (f : 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), 𝕜))
        f →
      ∀
        (hf :
          f ∈
            (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
                  (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
              Set C((↑s : Type u_1), 𝕜))),
        r • f ∈
          (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
                (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
            Set C((↑s : Type u_1), 𝕜))
star :
  ∀ (f : 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), 𝕜))
        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.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), 𝕜))
⊢ 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:
induction hf using adjoin_induction with
  | mem f hf =>
    obtain rfl := Set.mem_singleton_iff.mp hf
    rfl
  | add f g _ _ hf hg => exact add_mem hf hg
  | zero => exact zero_mem _
  | mul f g _ _ _ hg => exact Ideal.mul_mem_left _ f hg
  | smul r f _ hf =>
    rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢
    rw [map_smul, hf, smul_zero]
  | star f _ hf =>
    rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢
    rw [map_star, hf, star_zero]

Premises used: RingHom.mem_ker, smul_zero, StarHomClass.map_star, Submodule.mul, Submodule.smul, Set.mem_singleton_iff, star_zero, SetLike.mem_coe, Iff.mp, Submodule.zero, ZeroMemClass.zero_mem, Submodule.add, rfl, map_smul, Star.star