-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
    (A : StarSubalgebra 𝕜 C(X, 𝕜)) (hA : A.SeparatesPoints) : A.topologicalClosure = ⊤

Proof state:
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
⊢ ∀ (x : C(X, 𝕜)), x ∈ A.topologicalClosure

Tactic:
have key : LinearMap.range I ≤ (A.toSubmodule.restrictScalars ℝ).topologicalClosure := by
  let A₀ : Submodule ℝ C(X, ℝ) := (A.toSubmodule.restrictScalars ℝ).comap I
  have SW : A₀.topologicalClosure = ⊤ :=
    haveI := subalgebra_topologicalClosure_eq_top_of_separatesPoints _ hA.rclike_to_real
    congr_arg Subalgebra.toSubmodule this
  rw [← Submodule.map_top, ← SW]
  have h₁ := A₀.topologicalClosure_map ((@ofRealCLM 𝕜 _).compLeftContinuousCompact X)
  have h₂ := (A.toSubmodule.restrictScalars ℝ).map_comap_le I
  exact h₁.trans (Submodule.topologicalClosure_mono h₂)

Result:
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
⊢ ∀ (x : C(X, 𝕜)), x ∈ A.topologicalClosure

Proof state:
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra))
SW : A₀.topologicalClosure = ⊤
h₁ :
  Submodule.map (↑(ContinuousLinearMap.compLeftContinuousCompact X ofRealCLM)) A₀.topologicalClosure ≤
    (Submodule.map (↑(ContinuousLinearMap.compLeftContinuousCompact X ofRealCLM)) A₀).topologicalClosure
⊢ Submodule.map I A₀.topologicalClosure ≤
    (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure

Tactic:
have h₂ := (A.toSubmodule.restrictScalars ℝ).map_comap_le I

Result:
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra))
SW : A₀.topologicalClosure = ⊤
h₁ :
  Submodule.map (↑(ContinuousLinearMap.compLeftContinuousCompact X ofRealCLM)) A₀.topologicalClosure ≤
    (Submodule.map (↑(ContinuousLinearMap.compLeftContinuousCompact X ofRealCLM)) A₀).topologicalClosure
h₂ :
  Submodule.map I (Submodule.comap I (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra))) ≤
    Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)
⊢ Submodule.map I A₀.topologicalClosure ≤
    (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure

Proof state:
case h.e'_5.h.h
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f
f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f
h_f_re : I f_re ∈ A.topologicalClosure
h_f_im : I f_im ∈ A.topologicalClosure
this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure
a✝ : X
⊢ (I f_re + RCLike.I • I f_im) a✝ = f a✝

Tactic:
simp [I, f_re, f_im, mul_comm RCLike.I _]

Result:
no goals

Proof state:
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f
f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f
h_f_re : I f_re ∈ A.topologicalClosure
h_f_im : I f_im ∈ A.topologicalClosure
this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure
⊢ f ∈ A.topologicalClosure

Tactic:
convert this

Result:
case h.e'_5
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f
f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f
h_f_re : I f_re ∈ A.topologicalClosure
h_f_im : I f_im ∈ A.topologicalClosure
this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure
⊢ f = I f_re + RCLike.I • I f_im

Proof state:
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
⊢ LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure

Tactic:
let A₀ : Submodule ℝ C(X, ℝ) := (A.toSubmodule.restrictScalars ℝ).comap I

Result:
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
A₀ : Submodule ℝ C(X, ℝ) := Submodule.comap I (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra))
⊢ LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure

Proof state:
case h.e'_5.h
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f
f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f
h_f_re : I f_re ∈ A.topologicalClosure
h_f_im : I f_im ∈ A.topologicalClosure
this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure
a✝ : X
⊢ f a✝ = (I f_re + RCLike.I • I f_im) a✝

Tactic:
apply Eq.symm

Result:
case h.e'_5.h.h
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f
f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f
h_f_re : I f_re ∈ A.topologicalClosure
h_f_im : I f_im ∈ A.topologicalClosure
this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure
a✝ : X
⊢ (I f_re + RCLike.I • I f_im) a✝ = f a✝