-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
x : C((↑s : Type u_1), 𝕜)
h :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
      x ↔
    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), 𝕜))
h₁ :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
      x ↔
    Membership.mem (γ := Submodule 𝕜 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), 𝕜))))
      x
h₂ :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
      (StarAlgebra.adjoin 𝕜
        (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
              NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
          Set C((↑s : Type u_1), 𝕜)))
      x ↔
    Membership.mem (γ := Submodule 𝕜 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), 𝕜))))
      x
h₃ :
  Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
      (StarSubalgebra.toSubalgebra
        (StarAlgebra.adjoin 𝕜
          (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
            Set C((↑s : Type u_1), 𝕜))))
      x ↔
    Membership.mem (γ := Submodule 𝕜 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), 𝕜))))
      x
h₄ :
  Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C((↑s : Type u_1), 𝕜)) → Submodule 𝕜 C((↑s : Type u_1), 𝕜))
          (StarSubalgebra.toSubalgebra
            (StarAlgebra.adjoin 𝕜
              (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                    NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
                Set C((↑s : Type u_1), 𝕜)))) :
        Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      x ↔
    Membership.mem (γ := Submodule 𝕜 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), 𝕜))))
      x
h₅ :
  Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      (𝕜 ∙ 1 ⊔
          NonUnitalSubalgebra.toSubmodule
            (NonUnitalStarSubalgebra.toNonUnitalSubalgebra
              (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)})) :
        Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      x ↔
    Membership.mem (γ := Submodule 𝕜 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), 𝕜))))
      x
h₆ :
  Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      (𝕜 ∙ 1 ⊔
          NonUnitalSubalgebra.toSubmodule
            (NonUnitalStarSubalgebra.toNonUnitalSubalgebra
              (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)})) :
        Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      x ↔
    Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      (𝕜 ∙ 1 ⊔
        span 𝕜
          (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
                NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
            Set C((↑s : Type u_1), 𝕜)))
      x
h₇ h₈ :
  Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      (𝕜 ∙ 1 ⊔
          NonUnitalSubalgebra.toSubmodule
            (NonUnitalStarSubalgebra.toNonUnitalSubalgebra
              (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)})) :
        Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      x ↔
    Membership.mem (γ := Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      (𝕜 ∙ 1 ⊔
          NonUnitalSubalgebra.toSubmodule (A := C((↑s : Type u_1), 𝕜))
            (NonUnitalStarSubalgebra.toNonUnitalSubalgebra
              (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)})) :
        Submodule 𝕜 C((↑s : Type u_1), 𝕜))
      x
⊢ 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), 𝕜))

Tactic:
rw [SetLike.mem_coe, SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
    ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
    StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_union, span_eq_toSubmodule]

Premises used: StarSubalgebra.mem_toSubalgebra, StarAlgebra.adjoin_nonUnitalStarSubalgebra, Subalgebra.mem_toSubmodule, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, Submodule.span_union, SetLike.mem_coe, NonUnitalStarAlgebra.span_eq_toSubmodule