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

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

Tactic:
rw [SetLike.mem_coe] at hf₂ ⊢

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

Proof state:
case h.mp.intro
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf₂ : f ∈ RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)
hf₁ : ∃ x, (∃ a, a • 1 = x) ∧ ∃ y ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}, x + y = f
⊢ f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

Tactic:
obtain ⟨-, ⟨r, rfl⟩, f, hf, rfl⟩ := hf₁

Result:
case h.mp.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C(↑s, 𝕜)
hf : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf₂ : r • 1 + f ∈ RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)
⊢ r • 1 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

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

Tactic:
simp only [SetLike.mem_coe, RingHom.mem_ker, evalStarAlgHom_apply] at hf₂ this

Result:
case h.mp.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C(↑s, 𝕜)
hf : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf₂ : (r • 1 + f) ⟨0, h0⟩ = 0
this : f ⟨0, h0⟩ = 0
⊢ r • 1 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

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

Tactic:
refine fun hf ↦ ⟨?_, nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf⟩

Result:
case h.mpr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
⊢ f ∈ StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

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

Tactic:
have := nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf

Result:
case h.mp.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C(↑s, 𝕜)
hf : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf₂ : r • 1 + f ∈ RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)
this : f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
⊢ r • 1 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

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

Tactic:
constructor

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

case h.mpr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
⊢ f ∈ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) →
    f ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ∩ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Proof state:
case h.mp.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C(↑s, 𝕜)
hf : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf₂ : (r • 1 + f) ⟨0, h0⟩ = 0
this : f ⟨0, h0⟩ = 0
⊢ r • 1 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

Tactic:
rw [add_apply, this, add_zero, smul_apply, one_apply, smul_eq_mul, mul_one] at hf₂

Result:
case h.mp.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C(↑s, 𝕜)
hf : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf₂ : r = 0
this : f ⟨0, h0⟩ = 0
⊢ r • 1 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

Proof state:
case h.mp.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C(↑s, 𝕜)
hf : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
hf₂ : r = 0
this : f ⟨0, h0⟩ = 0
⊢ r • 1 + f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

Tactic:
rwa [hf₂, zero_smul, zero_add]

Result:
no goals

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

Tactic:
simp only [Set.mem_inter_iff, SetLike.mem_coe]

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

Proof state:
case h.mpr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf : f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}
⊢ f ∈ StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}

Tactic:
exact adjoin_le_starAlgebra_adjoin _ _ hf

Result:
no goals

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

Tactic:
rintro ⟨hf₁, hf₂⟩

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

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

Tactic:
ext f

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

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

Tactic:
simp_rw [adjoin_id_eq_span_one_add, Set.mem_add, SetLike.mem_coe, mem_span_singleton] at hf₁

Result:
case h.mp.intro
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C(↑s, 𝕜)
hf₂ : f ∈ RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)
hf₁ : ∃ x, (∃ a, a • 1 = x) ∧ ∃ y ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}, x + y = f
⊢ f ∈ adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}