awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ Eq (α := 𝕜)
    ((evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : (a : C((↑s : Type u_1), 𝕜)) → 𝕜) (Star.star f) :
      𝕜)
    (0 : 𝕜)
have star₂ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [map_star, hf, star_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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), 𝕜))
⊢ f ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
have 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), 𝕜))
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]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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), 𝕜))
⊢ f ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
have 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), 𝕜))
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]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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), 𝕜))
⊢ f ∈
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
have 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), 𝕜))
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]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
⊢ (↑(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), 𝕜))
have 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), 𝕜))
Tactic: ext f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
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), 𝕜))
have 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), 𝕜))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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), 𝕜))
⊢ 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), 𝕜))
have 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), 𝕜))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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), 𝕜))
⊢ f ∈
    (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
          NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
      Set C((↑s : Type u_1), 𝕜))
have 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
Tactic: rw [SetLike.mem_coe] at hf₂ ⊢
Cleared hypotheses: hf₂
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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
⊢ 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
have 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
Tactic: simp_rw [adjoin_id_eq_span_one_add, Set.mem_add, SetLike.mem_coe, mem_span_singleton] at hf₁
Cleared hypotheses: hf₁
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ 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
have 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)
Tactic: obtain ⟨-, ⟨r, rfl⟩, f, hf, rfl⟩ := hf₁
Cleared hypotheses: f, hf₂, hf₁
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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)
⊢ 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)
have 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), 𝕜))
Tactic: have := nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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), 𝕜))
⊢ 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)
have 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 : 𝕜)
Tactic: simp only [SetLike.mem_coe, RingHom.mem_ker, evalStarAlgHom_apply] at hf₂ this
Cleared hypotheses: hf₂, this
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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 : 𝕜)
⊢ 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)
have this₁ : 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
Cleared hypotheses: hf₂, this
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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 : 𝕜)
⊢ 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)
have hf₃ : r = 0
Tactic: rw [add_apply, this, add_zero, smul_apply, one_apply, smul_eq_mul, mul_one] at hf₂
Cleared hypotheses: hf₂, this
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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₂ : r = 0
this : Eq (α := 𝕜) ((f : (a : { x : 𝕜 // x ∈ s }) → 𝕜) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : 𝕜) (0 : 𝕜)
⊢ 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)
have h : 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), 𝕜)) 0 1 + f)
Tactic: rwa [hf₂, zero_smul, zero_add]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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₂ : r = 0
this : Eq (α := 𝕜) ((f : (a : { x : 𝕜 // x ∈ s }) → 𝕜) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : 𝕜) (0 : 𝕜)
h :
  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), 𝕜)) 0 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)
have h₁ : 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), 𝕜))
  (0 + f)
Tactic: rwa [hf₂, zero_smul, zero_add]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
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 →
    Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
        (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) f ∧
      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
have h : ∀
  (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),
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
    f
Tactic: refine fun hf ↦ ⟨?_, nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf⟩