-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem Subalgebra.SeparatesPoints.rclike_to_real {A : StarSubalgebra 𝕜 C(X, 𝕜)}
    (hA : A.SeparatesPoints) :
      ((A.restrictScalars ℝ).comap
        (ofRealAm.compLeftContinuous ℝ continuous_ofReal)).SeparatesPoints

Proof state:
case h.e'_5.h
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
a✝ : X
⊢ ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯) { toFun := fun x => ‖F x‖ ^ 2, continuous_toFun := ⋯ }) a✝ = (F * star F) a✝

Tactic:
simp [← RCLike.mul_conj]

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
⊢ (fun f => ⇑f) { toFun := fun x => ‖F x‖ ^ 2, continuous_toFun := ⋯ } x₁ ≠
    (fun f => ⇑f) { toFun := fun x => ‖F x‖ ^ 2, continuous_toFun := ⋯ } x₂

Tactic:
simpa [F] using sub_ne_zero.mpr hf

Result:
no goals

Proof state:
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
⊢ f x₂ • 1 = const X (f x₂)

Tactic:
ext1

Result:
case h
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
a✝ : X
⊢ (f x₂ • 1) a✝ = (const X (f x₂)) a✝

Proof state:
case intro.intro.intro.intro.refine_1
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
⊢ (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) { toFun := fun x => ‖F x‖ ^ 2, continuous_toFun := ⋯ } ∈
    restrictScalars ℝ A.toSubalgebra

Tactic:
convert (A.restrictScalars ℝ).mul_mem hFA (star_mem hFA : star F ∈ A)

Result:
case h.e'_5
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
⊢ (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) { toFun := fun x => ‖F x‖ ^ 2, continuous_toFun := ⋯ } = F * star F

Proof state:
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
⊢ (comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)).SeparatesPoints

Tactic:
intro x₁ x₂ hx

Result:
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)),
    f x₁ ≠ f x₂

Proof state:
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
⊢ Continuous fun x => ‖F x‖ ^ 2

Tactic:
continuity

Result:
no goals

Proof state:
case h.e'_5
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
⊢ (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) { toFun := fun x => ‖F x‖ ^ 2, continuous_toFun := ⋯ } = F * star F

Tactic:
ext1

Result:
case h.e'_5.h
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
a✝ : X
⊢ ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯) { toFun := fun x => ‖F x‖ ^ 2, continuous_toFun := ⋯ }) a✝ = (F * star F) a✝

Proof state:
case intro.intro.intro.intro.refine_1
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
⊢ { toFun := fun x => ‖F x‖ ^ 2, continuous_toFun := ⋯ } ∈
    ↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra))

Tactic:
rw [SetLike.mem_coe, Subalgebra.mem_comap]

Result:
case intro.intro.intro.intro.refine_1
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
hFA : F ∈ A
⊢ (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) { toFun := fun x => ‖F x‖ ^ 2, continuous_toFun := ⋯ } ∈
    restrictScalars ℝ A.toSubalgebra

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)),
    f x₁ ≠ f x₂

Tactic:
let F : C(X, 𝕜) := f - const _ (f x₂)

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)),
    f x₁ ≠ f x₂

Proof state:
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)),
    f x₁ ≠ f x₂

Tactic:
obtain ⟨_, ⟨f, hfA, rfl⟩, hf⟩ := hA hx

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)),
    f x₁ ≠ f x₂

Proof state:
case h
𝕜 : Type u_1
X : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ ↑A.toSubalgebra
hf : (fun f => ⇑f) f x₁ ≠ (fun f => ⇑f) f x₂
F : C(X, 𝕜) := f - const X (f x₂)
a✝ : X
⊢ (f x₂ • 1) a✝ = (const X (f x₂)) a✝

Tactic:
simp only [coe_smul, coe_one, smul_apply, one_apply, Algebra.id.smul_eq_mul, mul_one,
  const_apply]

Result:
no goals