awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
⊢ closure[inst_5] ((↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A)) =
    closure[inst_5] (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A)
have refine_1 : closure[inst_5] ((↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A)) ⊆ closure[inst_5] (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A)
Tactic: refine subset_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
refine_1 :
  closure[inst_5] ((↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A)) ⊆
    closure[inst_5] (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A)
⊢ closure[inst_5] ((↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A)) =
    closure[inst_5] (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A)
have refine_2 : closure[inst_5] (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A) ⊆ closure[inst_5] ((↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A))
Tactic: refine subset_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
x : A
⊢ x ∈ closure[inst_5] (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A) →
    x ∈ closure[inst_5] ((↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A))
have refine_2 : ∀ (hxs : x ∈ closure[inst_5] (↑s : Set A)) (hxφ : Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)),
  x ∈ closure[inst_5] ((↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A))
Tactic: ⟨hxs, (hxφ : φ x = 0)⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
x : A
hxs : x ∈ closure[inst_5] (↑s : Set A)
hxφ : Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)
⊢ x ∈ closure[inst_5] ((↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A))
have hxs₁ : (𝓝 x ⊓ 𝓟 (↑s : Set A)).NeBot
Tactic: rw [mem_closure_iff_clusterPt, ClusterPt] at hxs
Cleared hypotheses: hxs, hxφ
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 (↑s : Set A)).NeBot
hxφ : Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)
| Tendsto (fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1)
    (𝓝 x ⊓ 𝓟 (↑s : Set A)) (𝓝 x)
have f : fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 (↑s : Set A)).NeBot
hxφ : Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)
f : fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1
| Tendsto (fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1)
    (𝓝 x ⊓ 𝓟 (↑s : Set A)) (𝓝 x)
have l₁ : 𝓝 x ⊓ 𝓟 (↑s : Set A)
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 (↑s : Set A)).NeBot
hxφ : Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)
f : fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1
l₁ : 𝓝 x ⊓ 𝓟 (↑s : Set A)
| Tendsto (fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1)
    (𝓝 x ⊓ 𝓟 (↑s : Set A)) (𝓝 x)
have l₂ : 𝓝 x
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 (↑s : Set A)).NeBot
hxφ : Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)
| 𝓝 x
have l₂ : 𝓝 (x - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) x : K) 1)
Tactic: rw [← sub_zero x, ← zero_smul K 1, ← hxφ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 (↑s : Set A)).NeBot
hxφ : Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)
| Tendsto (fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1)
    (𝓝 x ⊓ 𝓟 (↑s : Set A)) (𝓝 x)
have l₂ : 𝓝 (x - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) x : K) 1)
Tactic: congr; rfl; rfl; rw [← sub_zero x, ← zero_smul K 1, ← hxφ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 (↑s : Set A)).NeBot
hxφ : Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)
⊢ Tendsto (fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1)
    (𝓝 x ⊓ 𝓟 (↑s : Set A)) (𝓝 x)
have conv : Tendsto (fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1)
  (𝓝 x ⊓ 𝓟 (↑s : Set A)) (𝓝 (x - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) x : K) 1))
Tactic: conv => congr; rfl; rfl; rw [← sub_zero x, ← zero_smul K 1, ← hxφ]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 (↑s : Set A)).NeBot
hxφ : Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)
⊢ x ∈ closure[inst_5] ((↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A))
have this : Tendsto (fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1)
  (𝓝 x ⊓ 𝓟 (↑s : Set A)) (𝓝 x)
Tactic: have : Tendsto (fun y ↦ y - φ y • 1) (𝓝 x ⊓ 𝓟 s) (𝓝 x) := by
      conv => congr; rfl; rfl; rw [← sub_zero x, ← zero_smul K 1, ← hxφ]
      exact Filter.tendsto_inf_left (Continuous.tendsto (by fun_prop) x)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 (↑s : Set A)).NeBot
hxφ : Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)
this :
  Tendsto (fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1)
    (𝓝 x ⊓ 𝓟 (↑s : Set A)) (𝓝 x)
⊢ x ∈ closure[inst_5] ((↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A))
have refine_2 : ∀ᶠ (x : A) in 𝓝 x,
  x ∈ (↑s : Set A) →
    x - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) x : K) 1 ∈
      (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A)
Tactic: refine mem_closure_of_tendsto this <| eventually_inf_principal.mpr ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 (↑s : Set A)).NeBot
hxφ : Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)
this :
  Tendsto (fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1)
    (𝓝 x ⊓ 𝓟 (↑s : Set A)) (𝓝 x)
⊢ ∀ᶠ (x : A) in 𝓝 x,
    x ∈ (↑s : Set A) →
      x - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) x : K) 1 ∈
        (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A)
have refine_2 : ∀ (a : A),
  Membership.mem (γ := Set A)
    {x : A |
      (fun (x : A) ↦
          x ∈ (↑s : Set A) →
            x - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) x : K) 1 ∈
              (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A))
        x}
    a
Tactic: filter_upwards [] with g hg using
      ⟨sub_mem hg (SMulMemClass.smul_mem _ <| one_mem _), by simp [RingHom.mem_ker]⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst : CommRing K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : TopologicalSpace K
inst_4 : T1Space K
inst_5 : TopologicalSpace A
inst_6 : ContinuousSub A
inst_7 : ContinuousSMul K A
inst_8 : FunLike F A K
inst_9 : AlgHomClass F K A K
inst_10 : SetLike S A
inst_11 : OneMemClass S A
inst_12 : AddSubgroupClass S A
inst_13 : SMulMemClass S K A
φ : F
hφ : Continuous[inst_5, inst_3] (⇑φ : (a : A) → K)
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 (↑s : Set A)).NeBot
hxφ : Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)
this :
  Tendsto (fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1)
    (𝓝 x ⊓ 𝓟 (↑s : Set A)) (𝓝 x)
refine_2 :
  ∀ (a : A),
    Membership.mem (γ := Set A)
      {x : A |
        (fun (x : A) ↦
            x ∈ (↑s : Set A) →
              x - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) x : K) 1 ∈
                (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A))
          x}
      a
⊢ ∀ᶠ (x : A) in 𝓝 x,
    x ∈ (↑s : Set A) →
      x - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) x : K) 1 ∈
        (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A)
have refine_2₁ : ∀ a ∈ (↑s : Set A),
  a - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) a : K) 1 ∈
    (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A)
Tactic: filter_upwards [] with g hg using
      ⟨sub_mem hg (SMulMemClass.smul_mem _ <| one_mem _), by simp [RingHom.mem_ker]⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
⊢ (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜)) =
    closure
      (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) :
        Set C((↑s : Type u_1), 𝕜))
have rw : (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
        (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
    Set C((↑s : Type u_1), 𝕜)) =
  closure (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) ∩
    (↑(RingHom.ker (F := C((↑s : Type u_1), 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜))
Tactic: rw [← ker_evalStarAlgHom_inter_adjoin_id s h0,
    AlgHom.closure_ker_inter (φ := evalStarAlgHom 𝕜 𝕜 (X := s) ⟨0, h0⟩) (continuous_eval_const _) _]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
⊢ (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
      Set C((↑s : Type u_1), 𝕜)) =
    closure (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) ∩
      (↑(RingHom.ker (F := C((↑s : Type u_1), 𝕜) →⋆ₐ[𝕜] 𝕜)
            (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0))) :
        Set C((↑s : Type u_1), 𝕜))
have h : closure (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) = Set.univ
Tactic: convert! (Set.univ_inter _).symm
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst_1 : CompactSpace.{u_1} (↑s : Type u_1)
⊢ closure (↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) : Set C((↑s : Type u_1), 𝕜)) = Set.univ
have h : closure (↑(Subalgebra.starClosure (polynomialFunctions s)) : Set C((↑s : Type u_1), 𝕜)) = Set.univ
Tactic: rw [← Polynomial.toContinuousMapOn_X_eq_restrict_id, ← Polynomial.toContinuousMapOnAlgHom_apply,
    ← polynomialFunctions.starClosure_eq_adjoin_X s]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
⊢ Dense
    (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
          NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀) :
      Set C((↑s : Type u_1), 𝕜)₀)
have h0' : 0 ∈ s
Tactic: have h0' : 0 ∈ s := Fact.out
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
h0' : 0 ∈ s
⊢ Dense
    (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
          NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀) :
      Set C((↑s : Type u_1), 𝕜)₀)
have rw : Eq (α := Set C((↑s : Type u_1), 𝕜)₀)
  ((⇑toContinuousMapHom : (a : C((↑s : Type u_1), 𝕜)₀) → C((↑s : Type u_1), 𝕜)) ⁻¹'
    (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (ContinuousMap.evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0'))) :
      Set C((↑s : Type u_1), 𝕜)))
  Set.univ
Tactic: rw [dense_iff_closure_eq,
    ← isClosedEmbedding_toContinuousMap.injective.preimage_image (closure _),
    ← isClosedEmbedding_toContinuousMap.closure_image_eq, ← coe_toContinuousMapHom,
    ← NonUnitalStarSubalgebra.coe_map, NonUnitalStarAlgHom.map_adjoin_singleton,
    toContinuousMapHom_apply, toContinuousMap_id,
    ← ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id s h0']
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
h0' : 0 ∈ s
⊢ Eq (α := Set C((↑s : Type u_1), 𝕜)₀)
    ((⇑toContinuousMapHom : (a : C((↑s : Type u_1), 𝕜)₀) → C((↑s : Type u_1), 𝕜)) ⁻¹'
      (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
            (ContinuousMap.evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0'))) :
        Set C((↑s : Type u_1), 𝕜)))
    Set.univ
have apply : ∀ (f : C((↑s : Type u_1), 𝕜)₀),
  Membership.mem (γ := Set C((↑s : Type u_1), 𝕜)₀)
    ((⇑toContinuousMapHom : (a : C((↑s : Type u_1), 𝕜)₀) → C((↑s : Type u_1), 𝕜)) ⁻¹'
      (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
            (ContinuousMap.evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0'))) :
        Set C((↑s : Type u_1), 𝕜)))
    f
Tactic: apply Set.eq_univ_of_forall fun f ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
h0' : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)₀
⊢ Membership.mem (γ := Set C((↑s : Type u_1), 𝕜)₀)
    ((⇑toContinuousMapHom : (a : C((↑s : Type u_1), 𝕜)₀) → C((↑s : Type u_1), 𝕜)) ⁻¹'
      (↑(RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
            (ContinuousMap.evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0'))) :
        Set C((↑s : Type u_1), 𝕜)))
    f
have simp : Eq (α := 𝕜) ((f : (a : { x : 𝕜 // x ∈ s }) → 𝕜) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0') : 𝕜) (0 : 𝕜)
Tactic: simp only [Set.mem_preimage, toContinuousMapHom_apply, SetLike.mem_coe, RingHom.mem_ker,
    ContinuousMap.evalStarAlgHom_apply, ContinuousMap.coe_coe]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          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 (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
      (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
        NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
      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 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          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), 𝕜)₀) ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s}) f
⊢ p f
have hf₁ : f = ContinuousMapZero.id s ∨ star f = ContinuousMapZero.id s
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 𝕜
inst_1 : Fact (0 ∈ s)
p : C((↑s : Type u_1), 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id s)
star_id : p (star (ContinuousMapZero.id s))
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)
smul : ∀ (r : 𝕜) (f : C((↑s : Type u_1), 𝕜)₀), p f → p (r • f)
closure :
  (∀ (f : C((↑s : Type u_1), 𝕜)₀),
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          f →
        p f) →
    ∀ (f : C((↑s : Type u_1), 𝕜)₀), p f
f_1 f_2 f : C((↑s : Type u_1), 𝕜)₀
hf : f = ContinuousMapZero.id s ∨ star f = ContinuousMapZero.id s
⊢ p f
have hf₁ : f = ContinuousMapZero.id s ∨ star (ContinuousMapZero.id s) = f
Tactic: rw [star_eq_iff_star_eq] at hf
Cleared hypotheses: hf