-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
/-- If `s : Set 𝕜` with `RCLike 𝕜` is compact and contains `0`, then the non-unital star subalgebra
generated by the identity function in `C(s, 𝕜)₀` is dense. This can be seen as a version of the
Weierstrass approximation theorem. -/
lemma ContinuousMapZero.adjoin_id_dense {s : Set 𝕜} [Zero s] (h0 : ((0 : s) : 𝕜) = 0)
    [CompactSpace s] : Dense (adjoin 𝕜 {(.id h0 : C(s, 𝕜)₀)} : Set C(s, 𝕜)₀)

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
f : C(↑s, 𝕜)₀
⊢ f ⟨0, h0'⟩ = 0

Tactic:
rw [show ⟨0, h0'⟩ = (0 : s) by ext; exact h0.symm, _root_.map_zero f]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
⊢ Dense ↑(adjoin 𝕜 {ContinuousMapZero.id h0})

Tactic:
have h0' : 0 ∈ s := h0 ▸ (0 : s).property

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
⊢ Dense ↑(adjoin 𝕜 {ContinuousMapZero.id h0})

Proof state:
case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
f : C(↑s, 𝕜)₀
⊢ ↑⟨0, h0'⟩ = ↑0

Tactic:
exact h0.symm

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
f : C(↑s, 𝕜)₀
⊢ f ∈ ⇑toContinuousMapHom ⁻¹' ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0'⟩))

Tactic:
simp only [Set.mem_preimage, toContinuousMapHom_apply, SetLike.mem_coe, RingHom.mem_ker,
  ContinuousMap.evalStarAlgHom_apply, ContinuousMap.coe_coe]

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
f : C(↑s, 𝕜)₀
⊢ f ⟨0, h0'⟩ = 0

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
f : C(↑s, 𝕜)₀
⊢ ⟨0, h0'⟩ = 0

Tactic:
ext

Result:
case a
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
f : C(↑s, 𝕜)₀
⊢ ↑⟨0, h0'⟩ = ↑0

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
⊢ Dense ↑(adjoin 𝕜 {ContinuousMapZero.id h0})

Tactic:
rw [dense_iff_closure_eq,
  ← isClosedEmbedding_toContinuousMap.injective.preimage_image (closure _),
  ← isClosedEmbedding_toContinuousMap.closure_image_eq, ← coe_toContinuousMapHom,
  ← NonUnitalStarSubalgebra.coe_map, NonUnitalStarAlgHom.map_adjoin_singleton,
  toContinuousMapHom_apply, toContinuousMap_id h0,
  ← ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id s h0']

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
⊢ ⇑toContinuousMapHom ⁻¹' ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0'⟩)) = Set.univ

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
⊢ ⇑toContinuousMapHom ⁻¹' ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0'⟩)) = Set.univ

Tactic:
apply Set.eq_univ_of_forall fun f ↦ ?_

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
h0' : 0 ∈ s
f : C(↑s, 𝕜)₀
⊢ f ∈ ⇑toContinuousMapHom ⁻¹' ↑(RingHom.ker (ContinuousMap.evalStarAlgHom 𝕜 𝕜 ⟨0, h0'⟩))