-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
lemma nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom {s : Set 𝕜} (h0 : 0 ∈ s) :
    (adjoin 𝕜 {restrict s (.id 𝕜)} : Set C(s, 𝕜)) ⊆
      RingHom.ker (evalStarAlgHom 𝕜 𝕜 (⟨0, h0⟩ : s))

Proof state:
case zero
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
⊢ 0 ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
exact zero_mem _

Result:
no goals

Proof state:
case add
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ f g : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hy✝ : g ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
hg : g ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
⊢ f + g ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
exact add_mem hf hg

Result:
no goals

Proof state:
case mem
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf : restrict s (ContinuousMap.id 𝕜) ∈ {restrict s (ContinuousMap.id 𝕜)}
⊢ restrict s (ContinuousMap.id 𝕜) ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf : f ∈ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
⊢ f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

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]

Result:
no goals

Proof state:
case mem
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ f : C(↑s, 𝕜)
hf : f ∈ {restrict s (ContinuousMap.id 𝕜)}
⊢ f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
obtain rfl := Set.mem_singleton_iff.mp hf

Result:
case mem
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf : restrict s (ContinuousMap.id 𝕜) ∈ {restrict s (ContinuousMap.id 𝕜)}
⊢ restrict s (ContinuousMap.id 𝕜) ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Proof state:
case star
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) (star f) = 0

Tactic:
rw [map_star, hf, star_zero]

Result:
no goals

Proof state:
case smul
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ : C(↑s, 𝕜)
r : 𝕜
f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
⊢ r • f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢

Result:
case smul
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ : C(↑s, 𝕜)
r : 𝕜
f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) (r • f) = 0

Proof state:
case star
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
⊢ star f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢

Result:
case star
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) (star f) = 0

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
⊢ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ⊆ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
intro f hf

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf : f ∈ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
⊢ f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Proof state:
case mul
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ f g : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hy✝ : g ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
a✝ : f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
hg : g ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
⊢ f * g ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
exact Ideal.mul_mem_left _ f hg

Result:
no goals

Proof state:
case smul
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f✝ : C(↑s, 𝕜)
r : 𝕜
f : C(↑s, 𝕜)
hx✝ : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf : (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) f = 0
⊢ (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩) (r • f) = 0

Tactic:
rw [map_smul, hf, smul_zero]

Result:
no goals