awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C((↑s : Type u_1), 𝕜)
hf :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    f
hf₂ :
  Eq (α := 𝕜)
    ((HSMul.hSMul (β := C((↑s : Type u_1), 𝕜)) r 1 + f : (a : { x : 𝕜 // x ∈ s }) → 𝕜)
        (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) :
      𝕜)
    (0 : 𝕜)
this : Eq (α := 𝕜) ((f : (a : { x : 𝕜 // x ∈ s }) → 𝕜) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : 𝕜) (0 : 𝕜)
hf₃ : r = 0
⊢ Eq (α := 𝕜) ((f : (a : { x : 𝕜 // x ∈ s }) → 𝕜) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : 𝕜) (0 : 𝕜)

Tactic:
rw [add_apply, this, add_zero, smul_apply, one_apply, smul_eq_mul, mul_one] at hf₂

Premises used: ContinuousMap.smul_apply, ContinuousMap.one_apply, ContinuousMap.add_apply, smul_eq_mul, mul_one, add_zero
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
r : 𝕜
f : C((↑s : Type u_1), 𝕜)
hf :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    f
hf₂ : r = 0
this : Eq (α := 𝕜) ((f : (a : { x : 𝕜 // x ∈ s }) → 𝕜) (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0) : 𝕜) (0 : 𝕜)
h :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (HSMul.hSMul (α := 𝕜) (β := C((↑s : Type u_1), 𝕜)) 0 1 + f)
h₁ :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (0 + f)
h₂ h₃ h₄ h₅ :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    f
⊢ Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (HSMul.hSMul (β := C((↑s : Type u_1), 𝕜)) r 1 + f)

Tactic:
rwa [hf₂, zero_smul, zero_add]

Premises used: zero_add, zero_smul
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)
⊢ Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
      (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
        NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
      f →
    Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
        (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) f ∧
      Membership.mem (γ := Ideal C({ x : 𝕜 // x ∈ s }, 𝕜))
        (RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0)))
        f

Tactic:
fun hf ↦ ⟨?_, nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf⟩

Premises used: ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom, And.intro
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)
h :
  ∀
    (hf :
      Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
        (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
          NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
        f),
    Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
      (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) f
⊢ Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
      (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
        NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
      f →
    Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
        (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) f ∧
      Membership.mem (γ := Ideal C({ x : 𝕜 // x ∈ s }, 𝕜))
        (RingHom.ker (F := C({ x : 𝕜 // x ∈ s }, 𝕜) →⋆ₐ[𝕜] 𝕜)
          (evalStarAlgHom 𝕜 𝕜 (Subtype.mk (p := fun (x : 𝕜) ↦ x ∈ s) 0 h0)))
        f

Tactic:
refine fun hf ↦ ⟨?_, nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf⟩
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)
hf :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    f
⊢ Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
    f

Tactic:
adjoin_le_starAlgebra_adjoin _ _ hf

Premises used: iInf, Set.Mem, Set.iInter, NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
f : C((↑s : Type u_1), 𝕜)
hf :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    (adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)) {restrict s (ContinuousMap.id 𝕜)} :
      NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜))
    f
⊢ Membership.mem (γ := StarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)) (StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
    f

Tactic:
exact adjoin_le_starAlgebra_adjoin _ _ hf

Premises used: NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)

Tactic:
subset_antisymm ?_ ?_

Premises used: subset_antisymm
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
refine_2 :
  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)

Tactic:
refine subset_antisymm ?_ ?_

Premises used: subset_antisymm
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)

Tactic:
simpa only [ker_eq, (isClosed_singleton.preimage hφ).closure_eq]
      using closure_inter_subset_inter_closure s (ker φ : Set A)

Premises used: IsClosed.closure_eq, closure_inter_subset_inter_closure, SetLike.coe, IsClosed.preimage, RingHom.ker_eq, isClosed_singleton, RingHom.ker
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
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))
⊢ x ∈ closure[inst_5] (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A) →
    x ∈ closure[inst_5] ((↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A))

Tactic:
⟨hxs, (hxφ : φ x = 0)⟩
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 ⊓ 𝓟 (↑s : Set A)).NeBot

Tactic:
rw [mem_closure_iff_clusterPt, ClusterPt] at hxs

Premises used: mem_closure_iff_clusterPt, ClusterPt
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
hxs₁ : (𝓝 x ⊓ 𝓟 (↑s : Set A)).NeBot
⊢ Eq.{u_4 + 1} (α := K) ((φ : (a : A) → K) x : K) (0 : K)

Tactic:
rw [mem_closure_iff_clusterPt, ClusterPt] at hxs

Premises used: mem_closure_iff_clusterPt, ClusterPt
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
l₂ : 𝓝 x
| 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:
congr
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
| fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 ⊓ 𝓟 (↑s : Set A)

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
l₂ : 𝓝 (x - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) x : K) 1)
| 𝓝 x

Tactic:
rw [← sub_zero x, ← zero_smul K 1, ← hxφ]

Premises used: sub_zero, zero_smul, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
l₂ : 𝓝 (x - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) x : 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)

Tactic:
congr; rfl; rfl; rw [← sub_zero x, ← zero_smul K 1, ← hxφ]

Premises used: sub_zero, zero_smul, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
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))
⊢ 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:
conv => congr; rfl; rfl; rw [← sub_zero x, ← zero_smul K 1, ← hxφ]

Premises used: sub_zero, zero_smul, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
⊢ Continuous[inst_5, inst_5] fun (y : A) ↦ y - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) y : K) 1

Tactic:
fun_prop
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) x : K) 1))

Tactic:
exact Filter.tendsto_inf_left (Continuous.tendsto (by fun_prop) x)

Premises used: Filter.tendsto_inf_left, Continuous.tendsto
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)

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)
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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))

Tactic:
mem_closure_of_tendsto this <| eventually_inf_principal.mpr ?_

Premises used: Filter.eventually_inf_principal, Iff.mpr, mem_closure_of_tendsto
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 :
  ∀ᶠ (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)
⊢ x ∈ closure[inst_5] ((↑s : Set A) ∩ (↑(RingHom.ker φ) : Set A))

Tactic:
refine mem_closure_of_tendsto this <| eventually_inf_principal.mpr ?_

Premises used: Filter.eventually_inf_principal, Iff.mpr, mem_closure_of_tendsto
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
g : A
hg : g ∈ (↑s : Set A)
⊢ g - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) g : K) 1 ∈ (↑(RingHom.ker φ) : Set A)

Tactic:
simp [RingHom.mem_ker]

Premises used: RingHom.mem_ker
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
refine_2₁ refine_2₂ :
  ∀ (g : A) (hg : g ∈ (↑s : Set A)),
    g - HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := A) ((φ : (a : A) → K) g : K) 1 ∈
      (↑s : Set A) ∩ (↑(RingHom.ker φ) : Set 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)

Tactic:
filter_upwards [] with g hg using
      ⟨sub_mem hg (SMulMemClass.smul_mem _ <| one_mem _), by simp [RingHom.mem_ker]⟩