-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ 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), 𝕜))
have 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
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]