awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_2
inst : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C((↑K : Type u_2), ℝ) :=
  compStarAlgHom' ℝ ℝ { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := ⋯ }
AK : Subalgebra ℝ C((↑K : Type u_2), ℝ) := Subalgebra.map (↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) A
hsep : AK.SeparatesPoints
gK : C((↑K : Type u_2), ℝ)
hgKAK_1 : gK ∈ AK
hgapprox :
  ∀ (x : (↑K : Type u_2)),
    ‖HSub.hSub (α := ℝ) (β := ℝ)
          (((↑(Subtype.mk (p := fun (x : C((↑K : Type u_2), ℝ)) ↦ x ∈ AK) gK hgKAK_1) : C((↑K : Type u_2), ℝ)) :
                (a : (↑K : Type u_2)) → ℝ)
              x :
            ℝ)
          (K.restrict (π := fun (a : X) ↦ ℝ) (⇑f : (a : X) → ℝ) x : ℝ)‖ <
      ε
g : C(X, ℝ)
hgA : g ∈ A
hgKAK : ((↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g = gK
x : X
hxK : x ∈ K
eqg :
  Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ)
    ((gK : (a : (↑K : Type u_2)) → ℝ) (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) : ℝ)
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((gK : (a : (↑K : Type u_2)) → ℝ) (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) : ℝ)
        ((f : (a : X) → ℝ) x : ℝ)‖ <
    ε

Tactic:
exact hgapprox ⟨x, hxK⟩

Premises used: Subtype.mk
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
obtain :
  ∀ (f : C(X, 𝕜)) (hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜)))
    (hf :
      Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
        ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)),
    ∃ (f : X → ℝ),
      Membership.mem (γ := Set (X → ℝ))
          ((fun (f : C(X, ℝ)) ↦ (⇑f : (a : X) → ℝ)) ''
            (↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)) : Set C(X, ℝ)))
          f ∧
        f x₁ ≠ f x₂
⊢ ∃ (f : X → ℝ),
    Membership.mem (γ := Set (X → ℝ))
        ((fun (f : C(X, ℝ)) ↦ (⇑f : (a : X) → ℝ)) ''
          (↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)) : Set C(X, ℝ)))
        f ∧
      f x₁ ≠ f x₂

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

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
⊢ F ∈ A

Tactic:
A.sub_mem hfA (@Eq.subst _ (· ∈ A) _ _ ?_ <| A.smul_mem A.one_mem <| f x₂)

Premises used: StarSubalgebra.toSubalgebra, Set.Mem, Eq.subst, Subalgebra.sub_mem, StarSubalgebra.smul_mem, Subalgebra.one_mem, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
refine : HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) ((f : (a : X) → 𝕜) x₂ : 𝕜) 1 = const X ((f : (a : X) → 𝕜) x₂)
⊢ F ∈ A

Tactic:
refine A.sub_mem hfA (@Eq.subst _ (· ∈ A) _ _ ?_ <| A.smul_mem A.one_mem <| f x₂)

Premises used: StarSubalgebra.toSubalgebra, Eq.subst, Subalgebra.sub_mem, StarSubalgebra.smul_mem, Subalgebra.one_mem, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
h :
  ∀ (a : X),
    Eq.{u_1 + 1} (α := 𝕜) ((HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) ((f : (a : X) → 𝕜) x₂ : 𝕜) 1 : (a : X) → 𝕜) a : 𝕜)
      (((const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜)) : (a : X) → 𝕜) a : 𝕜)
⊢ HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) ((f : (a : X) → 𝕜) x₂ : 𝕜) 1 = const X ((f : (a : X) → 𝕜) x₂)

Tactic:
ext1
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
a : X
⊢ Eq.{u_1 + 1} (α := 𝕜) ((HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) ((f : (a : X) → 𝕜) x₂ : 𝕜) 1 : (a : X) → 𝕜) a : 𝕜)
    (((const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜)) : (a : X) → 𝕜) a : 𝕜)

Tactic:
simp only [smul_apply, one_apply, smul_eq_mul, mul_one,
      const_apply]

Premises used: ContinuousMap.smul_apply, ContinuousMap.one_apply, ContinuousMap.const_apply, smul_eq_mul, mul_one
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
⊢ F ∈ A

Tactic:
have hFA : F ∈ A := by
    refine A.sub_mem hfA (@Eq.subst _ (· ∈ A) _ _ ?_ <| A.smul_mem A.one_mem <| f x₂)
    ext1
    simp only [smul_apply, one_apply, smul_eq_mul, mul_one,
      const_apply]
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
hFA : F ∈ A
⊢ Continuous (Y := ℝ) fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2

Tactic:
fun_prop
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
hFA : F ∈ A
refine_1 :
  { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
      continuous_toFun := ⋯ } ∈
    (↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)) : Set C(X, ℝ))
refine_2 :
  Ne (α := ℝ)
    ((fun (f : C(X, ℝ)) ↦ ((⇑f : (a : X) → ℝ) : (a : X) → ℝ))
      { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
        continuous_toFun := ⋯ }
      x₁)
    ((fun (f : C(X, ℝ)) ↦ ((⇑f : (a : X) → ℝ) : (a : X) → ℝ))
      { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
        continuous_toFun := ⋯ }
      x₂)
⊢ ∃ (f : X → ℝ),
    Membership.mem (γ := Set (X → ℝ))
        ((fun (f : C(X, ℝ)) ↦ (⇑f : (a : X) → ℝ)) ''
          (↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)) : Set C(X, ℝ)))
        f ∧
      f x₁ ≠ f x₂

Tactic:
refine ⟨_, ⟨⟨(‖F ·‖ ^ 2), by fun_prop⟩, ?_, rfl⟩, ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
hFA : F ∈ A
refine_1 :
  Membership.mem (α := C(X, 𝕜)) (γ := Subalgebra ℝ C(X, 𝕜)) (restrictScalars ℝ A.toSubalgebra)
    ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(X, ℝ)) → C(X, 𝕜))
        { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
          continuous_toFun := ⋯ } :
      C(X, 𝕜))
⊢ { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
      continuous_toFun := ⋯ } ∈
    (↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm ⋯) (restrictScalars ℝ A.toSubalgebra)) : Set C(X, ℝ))

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

Premises used: Subalgebra.mem_comap, SetLike.mem_coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
hFA : F ∈ A
⊢ Membership.mem (γ := Subalgebra ℝ C(X, 𝕜)) (restrictScalars ℝ A.toSubalgebra) (F * star F)

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

Premises used: Subalgebra.mul_mem, Real, StarSubalgebra.toSubalgebra, StarMemClass.star_mem, Subalgebra.restrictScalars
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
hFA : F ∈ A
h :
  (AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(X, ℝ)) → C(X, 𝕜))
      { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
        continuous_toFun := ⋯ } =
    F * star F
⊢ Membership.mem (α := C(X, 𝕜)) (γ := Subalgebra ℝ C(X, 𝕜)) (restrictScalars ℝ A.toSubalgebra)
    ((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(X, ℝ)) → C(X, 𝕜))
        { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
          continuous_toFun := ⋯ } :
      C(X, 𝕜))

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

Premises used: Subalgebra.mul_mem, Real, StarSubalgebra.toSubalgebra, StarMemClass.star_mem, Subalgebra.restrictScalars
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
hFA : F ∈ A
h :
  ∀ (a : X),
    Eq.{u_1 + 1} (α := 𝕜)
      ((((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(X, ℝ)) → C(X, 𝕜))
                { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
                  continuous_toFun := ⋯ } :
              C(X, 𝕜)) :
            (a : X) → 𝕜)
          a :
        𝕜)
      ((F * star F : (a : X) → 𝕜) a : 𝕜)
⊢ (AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(X, ℝ)) → C(X, 𝕜))
      { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
        continuous_toFun := ⋯ } =
    F * star F

Tactic:
ext1
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
hFA : F ∈ A
a : X
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((AlgHom.compLeftContinuous ℝ ofRealAm ⋯ : (a : C(X, ℝ)) → C(X, 𝕜))
              { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
                continuous_toFun := ⋯ } :
            C(X, 𝕜)) :
          (a : X) → 𝕜)
        a :
      𝕜)
    ((F * star F : (a : X) → 𝕜) a : 𝕜)

Tactic:
simp [← RCLike.mul_conj]

Premises used: RCLike.mul_conj
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
x₁ x₂ : X
hx : x₁ ≠ x₂
f : C(X, 𝕜)
hfA : f ∈ (↑A.toSubalgebra : Set C(X, 𝕜))
hf :
  Ne.{u_1 + 1} (α := 𝕜) ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₁)
    ((fun (f : C(X, 𝕜)) ↦ ((⇑f : (a : X) → 𝕜) : (a : X) → 𝕜)) f x₂)
F : C(X, 𝕜) := HSub.hSub (β := C(X, 𝕜)) f (const X ((f : (a : X) → 𝕜) x₂) : C(X, 𝕜))
hFA : F ∈ A
⊢ Ne (α := ℝ)
    ((fun (f : C(X, ℝ)) ↦ ((⇑f : (a : X) → ℝ) : (a : X) → ℝ))
      { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
        continuous_toFun := ⋯ }
      x₁)
    ((fun (f : C(X, ℝ)) ↦ ((⇑f : (a : X) → ℝ) : (a : X) → ℝ))
      { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
        continuous_toFun := ⋯ }
      x₂)

Tactic:
simpa [F] using sub_ne_zero.mpr hf

Premises used: Iff.mpr, sub_ne_zero
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
rw : ∀ (x : C(X, 𝕜)), x ∈ A.topologicalClosure
⊢ A.topologicalClosure = ⊤

Tactic:
rw [StarSubalgebra.eq_top_iff]

Premises used: StarSubalgebra.eq_top_iff
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
A₀ : Submodule ℝ C(X, ℝ) :=
  Submodule.comap (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜))
    (Submodule.restrictScalars ℝ (R := 𝕜)
      ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
⊢ A₀.topologicalClosure = ⊤

Tactic:
have SW : A₀.topologicalClosure = ⊤ :=
      haveI := subalgebra_topologicalClosure_eq_top_of_separatesPoints _ hA.rclike_to_real
      congr_arg Subalgebra.toSubmodule this
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
A₀ : Submodule ℝ C(X, ℝ) :=
  Submodule.comap (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜))
    (Submodule.restrictScalars ℝ (R := 𝕜)
      ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
SW : A₀.topologicalClosure = ⊤
rw :
  Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)) A₀.topologicalClosure ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
⊢ (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))

Tactic:
rw [← Submodule.map_top, ← SW]

Premises used: Submodule.map_top
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
A₀ : Submodule ℝ C(X, ℝ) :=
  Submodule.comap (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜))
    (Submodule.restrictScalars ℝ (R := 𝕜)
      ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
SW : A₀.topologicalClosure = ⊤
⊢ Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)) A₀.topologicalClosure ≤
    (Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)) A₀).topologicalClosure

Tactic:
have h₁ := A₀.topologicalClosure_map I
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
A₀ : Submodule ℝ C(X, ℝ) :=
  Submodule.comap (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜))
    (Submodule.restrictScalars ℝ (R := 𝕜)
      ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
SW : A₀.topologicalClosure = ⊤
h₁ :
  Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)) A₀.topologicalClosure ≤
    (Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)) A₀).topologicalClosure
⊢ Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜))
      (Submodule.comap (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜))
        (Submodule.restrictScalars ℝ (R := 𝕜)
          ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))) ≤
    Submodule.restrictScalars ℝ (R := 𝕜)
      ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra)

Tactic:
have h₂ := (A.toSubmodule.restrictScalars ℝ).map_comap_le I.toLinearMap
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
A₀ : Submodule ℝ C(X, ℝ) :=
  Submodule.comap (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜))
    (Submodule.restrictScalars ℝ (R := 𝕜)
      ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
SW : A₀.topologicalClosure = ⊤
h₁ :
  Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)) A₀.topologicalClosure ≤
    (Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)) A₀).topologicalClosure
h₂ :
  Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜))
      (Submodule.comap (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜))
        (Submodule.restrictScalars ℝ (R := 𝕜)
          ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))) ≤
    Submodule.restrictScalars ℝ (R := 𝕜)
      ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra)
⊢ Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)) A₀.topologicalClosure ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))

Tactic:
h₁.trans (Submodule.topologicalClosure_mono h₂)

Premises used: Set.Mem, Submodule.topologicalClosure_mono, LE.le.trans
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
A₀ : Submodule ℝ C(X, ℝ) :=
  Submodule.comap (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜))
    (Submodule.restrictScalars ℝ (R := 𝕜)
      ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
SW : A₀.topologicalClosure = ⊤
h₁ :
  Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)) A₀.topologicalClosure ≤
    (Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)) A₀).topologicalClosure
h₂ :
  Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜))
      (Submodule.comap (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜))
        (Submodule.restrictScalars ℝ (R := 𝕜)
          ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))) ≤
    Submodule.restrictScalars ℝ (R := 𝕜)
      ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra)
⊢ Submodule.map (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)) A₀.topologicalClosure ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))

Tactic:
exact h₁.trans (Submodule.topologicalClosure_mono h₂)

Premises used: Submodule.topologicalClosure_mono, LE.le.trans
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
⊢ (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))

Tactic:
have key : I.range ≤ (A.toSubmodule.restrictScalars ℝ).topologicalClosure := by
    -- Let `A₀` be the subalgebra of `C(X, ℝ)` consisting of `A`'s purely real elements; it is the
    -- preimage of `A` under `I`.  In this argument we only need its submodule structure.
    let A₀ : Submodule ℝ C(X, ℝ) := (A.toSubmodule.restrictScalars ℝ).comap I.toLinearMap
    -- By `Subalgebra.SeparatesPoints.rclike_to_real`, this subalgebra also separates points, so
    -- we may apply the real Stone-Weierstrass result to it.
    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]
    -- So it suffices to prove that the image under `I` of the closure of `A₀` is contained in the
    -- closure of `A`, which follows by abstract nonsense
    have h₁ := A₀.topologicalClosure_map I
    have h₂ := (A.toSubmodule.restrictScalars ℝ).map_comap_le I.toLinearMap
    exact h₁.trans (Submodule.topologicalClosure_mono h₂)
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
X : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace X
inst_2 : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key :
  (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
f : C(X, 𝕜)
f_re : C(X, ℝ) := comp { toFun := (⇑re : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
f_im : C(X, ℝ) := comp { toFun := (⇑im : (a : 𝕜) → ℝ), continuous_toFun := ⋯ } f
⊢ Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))

Tactic:
have h_f_re : I f_re ∈ A.topologicalClosure := key ⟨f_re, rfl⟩