-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
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)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)),
      Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)), p f
f_1 f : C((↑s : Type u_1), 𝕜)
hf :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (StarAlgebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
        ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜))))
    f
mem :
  ∀ (f : C((↑s : Type u_1), 𝕜))
    (hf :
      Membership.mem (γ := Set C((↑s : Type u_1), 𝕜))
        (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
          star
            (singleton (α := C((↑s : Type u_1), 𝕜))
              ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜))))
        f),
    p f
algebraMap : ∀ (r : 𝕜), p ((Algebra.algebraMap 𝕜 C((↑s : Type u_1), 𝕜) : (a : 𝕜) → C((↑s : Type u_1), 𝕜)) r)
add₁ :
  ∀ (x y : C((↑s : Type u_1), 𝕜)),
    Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
        (Algebra.adjoin 𝕜
          (singleton (α := C((↑s : Type u_1), 𝕜))
              ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
            star
              (singleton (α := C((↑s : Type u_1), 𝕜))
                ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
        x →
      Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
          (Algebra.adjoin 𝕜
            (singleton (α := C((↑s : Type u_1), 𝕜))
                ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
              star
                (singleton (α := C((↑s : Type u_1), 𝕜))
                  ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
          y →
        ∀ (hf : p x) (hg : p y), p (x + y)
⊢ p f
have mul₁ : ∀ (x y : C((↑s : Type u_1), 𝕜)),
  Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
      (Algebra.adjoin 𝕜
        (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
          star
            (singleton (α := C((↑s : Type u_1), 𝕜))
              ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
      x →
    Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
        (Algebra.adjoin 𝕜
          (singleton (α := C((↑s : Type u_1), 𝕜))
              ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
            star
              (singleton (α := C((↑s : Type u_1), 𝕜))
                ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
        y →
      ∀ (hf : p x) (hg : p y), p (x * y)
Tactic: induction hf using Algebra.adjoin_induction with
  | mem f hf =>
    push _ ∈ _ at hf
    rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf
    obtain (rfl | rfl) := hf
    all_goals simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]
  | algebraMap r => exact const r
  | add _ _ _ _ hf hg => exact add _ _ hf hg
  | mul _ _ _ _ hf hg => exact mul _ _ hf hg
Cleared hypotheses: hf