awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε
have right : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε
Tactic: use g, hgA
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ)
    ((gK : (a : (↑K : Type u_2)) → ℝ) (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) : ℝ)
have rw : Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ)
  (((((↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g :
          C((↑K : Type u_2), ℝ)) :
        (a : (↑K : Type u_2)) → ℝ)
      (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) :
    ℝ)
Tactic: rw [← hgKAK]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε
have eqg : Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ)
  ((gK : (a : (↑K : Type u_2)) → ℝ) (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) : ℝ)
Tactic: have eqg : g x = gK ⟨x, hxK⟩ := by
    rw [← hgKAK]; rfl
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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 (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε
have right : ‖HSub.hSub (α := ℝ) (β := ℝ) ((gK : (a : (↑K : Type u_2)) → ℝ) (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) : ℝ)
      ((f : (a : X) → ℝ) x : ℝ)‖ <
  ε
Tactic: rw [eqg]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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 : 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₂
have 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 sorry) (restrictScalars ℝ A.toSubalgebra)) : Set C(X, ℝ)))
        f ∧
      f x₁ ≠ f x₂
Tactic: obtain ⟨_, ⟨f, hfA, rfl⟩, hf⟩ := hA hx
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
have refine : HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) ((f : (a : X) → 𝕜) x₂ : 𝕜) 1 = const X ((f : (a : X) → 𝕜) x₂)
Tactic: refine A.sub_mem hfA (@Eq.subst _ (· ∈ A) _ _ ?_ <| A.smul_mem A.one_mem <| f x₂)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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, 𝕜))
⊢ HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) ((f : (a : X) → 𝕜) x₂ : 𝕜) 1 = const X ((f : (a : X) → 𝕜) x₂)
have 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 : 𝕜)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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 : 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₂
have hFA : 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]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ ∃ (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₂
have refine_1 : { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2, continuous_toFun := sorry } ∈
  (↑(comap (AlgHom.compLeftContinuous ℝ ofRealAm sorry) (restrictScalars ℝ A.toSubalgebra)) : Set C(X, ℝ))
Tactic: refine ⟨_, ⟨⟨(‖F ·‖ ^ 2), by fun_prop⟩, ?_, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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, ℝ))
⊢ ∃ (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₂
have 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 := sorry }
    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 := sorry }
    x₂)
Tactic: refine ⟨_, ⟨⟨(‖F ·‖ ^ 2), by fun_prop⟩, ?_, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ { 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, ℝ))
have refine_1 : Membership.mem (α := C(X, 𝕜)) (γ := Subalgebra ℝ C(X, 𝕜)) (restrictScalars ℝ A.toSubalgebra)
  ((AlgHom.compLeftContinuous ℝ ofRealAm sorry : (a : C(X, ℝ)) → C(X, 𝕜))
      { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
        continuous_toFun := sorry } :
    C(X, 𝕜))
Tactic: rw [SetLike.mem_coe, Subalgebra.mem_comap]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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 (α := 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, 𝕜))
have h : (AlgHom.compLeftContinuous ℝ ofRealAm sorry : (a : C(X, ℝ)) → C(X, 𝕜))
    { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
      continuous_toFun := sorry } =
  F * star F
Tactic: convert! (A.restrictScalars ℝ).mul_mem hFA (star_mem hFA : star F ∈ A)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ (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
have h : ∀ (a : X),
  Eq.{u_1 + 1} (α := 𝕜)
    ((((AlgHom.compLeftContinuous ℝ ofRealAm sorry : (a : C(X, ℝ)) → C(X, 𝕜))
              { toFun := fun (x : X) ↦ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((F : (a : X) → 𝕜) x : 𝕜)) 2,
                continuous_toFun := sorry } :
            C(X, 𝕜)) :
          (a : X) → 𝕜)
        a :
      𝕜)
    ((F * star F : (a : X) → 𝕜) a : 𝕜)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ A.topologicalClosure = ⊤
have rw : ∀ (x : C(X, 𝕜)), x ∈ A.topologicalClosure
Tactic: rw [StarSubalgebra.eq_top_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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))
⊢ (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
have SW : A₀.topologicalClosure = ⊤
Tactic: have SW : A₀.topologicalClosure = ⊤ :=
      haveI := subalgebra_topologicalClosure_eq_top_of_separatesPoints _ hA.rclike_to_real
      congr_arg Subalgebra.toSubmodule this
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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 = ⊤
⊢ (↑I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜)).range ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
have 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))
Tactic: rw [← Submodule.map_top, ← SW]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
have h₁ : 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
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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, 𝕜)) A₀.topologicalClosure ≤
    Submodule.topologicalClosure
      (Submodule.restrictScalars ℝ (R := 𝕜)
        ((Subalgebra.toSubmodule : (a : Subalgebra 𝕜 C(X, 𝕜)) → Submodule 𝕜 C(X, 𝕜)) A.toSubalgebra))
have 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)
Tactic: have h₂ := (A.toSubmodule.restrictScalars ℝ).map_comap_le I.toLinearMap
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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
⊢ ∀ (x : C(X, 𝕜)), x ∈ A.topologicalClosure
have key : (↑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₂)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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
⊢ f ∈ A.topologicalClosure
have h_f_re : 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⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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
h_f_re : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
⊢ f ∈ A.topologicalClosure
have h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
Tactic: have h_f_im : I f_im ∈ A.topologicalClosure := key ⟨f_im, rfl⟩