awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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, 𝕜))
h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
⊢ f ∈ A.topologicalClosure
have this : HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
    (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
  A.topologicalClosure.toSubalgebra
Tactic: have := A.topologicalClosure.add_mem h_f_re (A.topologicalClosure.smul_mem h_f_im RCLike.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
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, 𝕜))
h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
this :
  HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure.toSubalgebra
⊢ f ∈ A.topologicalClosure
have this₁ : HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
    (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
  A.topologicalClosure
Tactic: rw [StarSubalgebra.mem_toSubalgebra] at this
Cleared hypotheses: 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
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, 𝕜))
h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
this :
  HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure
⊢ f ∈ A.topologicalClosure
have h : f =
  HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
    (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜)))
Tactic: convert! 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
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, 𝕜))
h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
this :
  HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure
⊢ f =
    HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜)))
have h : ∀ (a : X),
  Eq.{u_1 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) a : 𝕜)
    ((HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
            (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) :
          (a : X) → 𝕜)
        a :
      𝕜)
Tactic: ext
-- 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
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, 𝕜))
h_f_im : Membership.mem (α := C(X, 𝕜)) A.topologicalClosure ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))
this :
  HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
      (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) ∈
    A.topologicalClosure
a : X
⊢ Eq.{u_1 + 1} (α := 𝕜) ((f : (a : X) → 𝕜) a : 𝕜)
    ((HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
            (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) :
          (a : X) → 𝕜)
        a :
      𝕜)
have h : Eq.{u_1 + 1} (α := 𝕜)
  ((HAdd.hAdd (α := C(X, 𝕜)) ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_re : C(X, 𝕜))
          (HSMul.hSMul (α := 𝕜) (β := C(X, 𝕜)) RCLike.I ((I : (a : C(X, ℝ)) → C(X, 𝕜)) f_im : C(X, 𝕜))) :
        (a : X) → 𝕜)
      a :
    𝕜)
  ((f : (a : X) → 𝕜) a : 𝕜)
Tactic: apply Eq.symm
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
⊢ Eq (α := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (elemental 𝕜 (restrict s (ContinuousMap.id 𝕜))) ⊤
have rw : Eq (α := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (topologicalClosure (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}))
  (topologicalClosure
    (adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
        ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
Tactic: rw [StarAlgebra.elemental, ← polynomialFunctions.starClosure_topologicalClosure,
    polynomialFunctions.starClosure_eq_adjoin_X]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
⊢ Eq (α := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (topologicalClosure (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}))
    (topologicalClosure
      (adjoin 𝕜
        (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
have e_s : Eq (α := C(𝕜, 𝕜)) (ContinuousMap.id 𝕜) (Polynomial.toContinuousMap X)
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f * g)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)),
      Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)), p f
f : C((↑s : Type u_1), 𝕜)
⊢ p f
have refine : ∀ (f : C((↑s : Type u_1), 𝕜))
  (hf :
    Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f),
  p f
Tactic: refine closure (fun f hf => ?_) f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f * g)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)),
      Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)), p f
f_1 f : C((↑s : Type u_1), 𝕜)
hf : Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f
⊢ p f
have hf₁ : Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
  (StarAlgebra.adjoin 𝕜
    (singleton (α := C((↑s : Type u_1), 𝕜))
      ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜))))
  f
Tactic: rw [polynomialFunctions.starClosure_eq_adjoin_X] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f * g)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)),
      Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)), p f
f_1 f_2 f : C((↑s : Type u_1), 𝕜)
hf :
  Membership.mem (γ := Set C((↑s : Type u_1), 𝕜))
    (singleton (α := C((↑s : Type u_1), 𝕜))
        ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
      star
        (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜))))
    f
⊢ p f
have hf₁ : f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X ∨
  star f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X
Tactic: push _ ∈ _ at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f * g)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)),
      Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)), p f
f_1 f_2 f : C((↑s : Type u_1), 𝕜)
hf :
  f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X ∨
    star f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X
⊢ p f
have hf₁ : f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X ∨
  f = star ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X)
Tactic: rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f * g)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)),
      Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)), p f
f_1 f_2 f : C((↑s : Type u_1), 𝕜)
hf :
  f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X ∨
    f = star ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X)
⊢ p f
have mem : p ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X)
Tactic: obtain (rfl | rfl) := hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f * g)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)),
      Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)), p f
f_1 f_2 f : C((↑s : Type u_1), 𝕜)
hf :
  f = (toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X ∨
    f = star ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X)
mem : p ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X)
⊢ p f
have mem₁ : p (star ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X))
Tactic: obtain (rfl | rfl) := hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f * g)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)),
      Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)), p f
f_1 f : C((↑s : Type u_1), 𝕜)
hf :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (StarAlgebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
        ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜))))
    f
⊢ p f
have mem : ∀ (f : C((↑s : Type u_1), 𝕜))
  (hf :
    Membership.mem (γ := Set C((↑s : Type u_1), 𝕜))
      (singleton (α := C((↑s : Type u_1), 𝕜))
          ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
        star
          (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜))))
      f),
  p f
Tactic: induction hf using Algebra.adjoin_induction with
  | mem f hf =>
    push _ ∈ _ at hf
    rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf
    obtain (rfl | rfl) := hf
    all_goals simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]
  | algebraMap r => exact const r
  | add _ _ _ _ hf hg => exact add _ _ hf hg
  | mul _ _ _ _ hf hg => exact mul _ _ hf hg
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f * g)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)),
      Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)), p f
f_1 f : C((↑s : Type u_1), 𝕜)
hf :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (StarAlgebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
        ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜))))
    f
mem :
  ∀ (f : C((↑s : Type u_1), 𝕜))
    (hf :
      Membership.mem (γ := Set C((↑s : Type u_1), 𝕜))
        (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
          star
            (singleton (α := C((↑s : Type u_1), 𝕜))
              ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜))))
        f),
    p f
⊢ p f
have algebraMap : ∀ (r : 𝕜), p ((algebraMap 𝕜 C((↑s : Type u_1), 𝕜) : (a : 𝕜) → C((↑s : Type u_1), 𝕜)) r)
Tactic: induction hf using Algebra.adjoin_induction with
  | mem f hf =>
    push _ ∈ _ at hf
    rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf
    obtain (rfl | rfl) := hf
    all_goals simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]
  | algebraMap r => exact const r
  | add _ _ _ _ hf hg => exact add _ _ hf hg
  | mul _ _ _ _ hf hg => exact mul _ _ hf hg
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f * g)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)),
      Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)), p f
f_1 f : C((↑s : Type u_1), 𝕜)
hf :
  Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (StarAlgebra.adjoin 𝕜
      (singleton (α := C((↑s : Type u_1), 𝕜))
        ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜))))
    f
mem :
  ∀ (f : C((↑s : Type u_1), 𝕜))
    (hf :
      Membership.mem (γ := Set C((↑s : Type u_1), 𝕜))
        (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
          star
            (singleton (α := C((↑s : Type u_1), 𝕜))
              ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜))))
        f),
    p f
algebraMap : ∀ (r : 𝕜), p ((Algebra.algebraMap 𝕜 C((↑s : Type u_1), 𝕜) : (a : 𝕜) → C((↑s : Type u_1), 𝕜)) r)
⊢ p f
have add₁ : ∀ (x y : C((↑s : Type u_1), 𝕜)),
  Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
      (Algebra.adjoin 𝕜
        (singleton (α := C((↑s : Type u_1), 𝕜))
            ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
          star
            (singleton (α := C((↑s : Type u_1), 𝕜))
              ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
      x →
    Membership.mem (γ := Subalgebra 𝕜 C((↑s : Type u_1), 𝕜))
        (Algebra.adjoin 𝕜
          (singleton (α := C((↑s : Type u_1), 𝕜))
              ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)) ∪
            star
              (singleton (α := C((↑s : Type u_1), 𝕜))
                ((toContinuousMapOnAlgHom s : (a : 𝕜[X]) → C((↑s : Type u_1), 𝕜)) X : C((↑s : Type u_1), 𝕜)))))
        y →
      ∀ (hf : p x) (hg : p y), p (x + y)
Tactic: induction hf using Algebra.adjoin_induction with
  | mem f hf =>
    push _ ∈ _ at hf
    rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf
    obtain (rfl | rfl) := hf
    all_goals simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]
  | algebraMap r => exact const r
  | add _ _ _ _ hf hg => exact add _ _ hf hg
  | mul _ _ _ _ hf hg => exact mul _ _ hf hg
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f * g)
frequently : ∀ (f : C((↑s : Type u_1), 𝕜)), (∃ᶠ (g : C((↑s : Type u_1), 𝕜)) in 𝓝 f, p g) → p f
f : C((↑s : Type u_1), 𝕜)
⊢ p f
have refine : ∀
  (h :
    ∀ (f : C((↑s : Type u_1), 𝕜)),
      Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
        p f)
  (f : C((↑s : Type u_1), 𝕜)), ∃ᶠ (g : C((↑s : Type u_1), 𝕜)) in 𝓝 f, p g
Tactic: refine f.induction_on const id star_id add mul fun h f ↦ frequently f ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
p : C((↑s : Type u_1), 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s : Type u_1) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C((↑s : Type u_1), 𝕜)), p f → p g → p (f * g)
frequently : ∀ (f : C((↑s : Type u_1), 𝕜)), (∃ᶠ (g : C((↑s : Type u_1), 𝕜)) in 𝓝 f, p g) → p f
f_1 : C((↑s : Type u_1), 𝕜)
h :
  ∀ (f : C((↑s : Type u_1), 𝕜)),
    Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (Subalgebra.starClosure (polynomialFunctions s)) f →
      p f
f : C((↑s : Type u_1), 𝕜)
⊢ ∃ᶠ (g : C((↑s : Type u_1), 𝕜)) in 𝓝 f, p g
have this : Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
  (topologicalClosure (Subalgebra.starClosure (polynomialFunctions s))) f
Tactic: have := polynomialFunctions.starClosure_topologicalClosure s ▸ mem_top (x := f)