awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 : 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
mem :
  ∀ (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
zero₁ : p 0
add₁ :
  ∀ (x y : C((↑s : Type u_1), 𝕜)₀),
    Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
        (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) x →
      Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) y →
        ∀ (hf : p x) (hg : p y), p (x + y)
mul₁ :
  ∀ (x y : C((↑s : Type u_1), 𝕜)₀),
    Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
        (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) x →
      Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
          (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) y →
        ∀ (hf : p x) (hg : p y), p (x * y)
smul₁ :
  ∀ (r : 𝕜) (x : C((↑s : Type u_1), 𝕜)₀),
    Membership.mem (γ := NonUnitalSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀)
        (NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id s} ∪ star {ContinuousMapZero.id s})) x →
      ∀ (hf : p x), p (r • x)
⊢ p f

Tactic:
induction hf using NonUnitalAlgebra.adjoin_induction with
  | mem f hf =>
    push _ ∈ _ at hf
    rw [star_eq_iff_star_eq] at hf
    obtain (rfl | rfl) := hf
    all_goals assumption
  | zero => exact zero
  | add _ _ _ _ hf hg => exact add _ _ hf hg
  | mul _ _ _ _ hf hg => exact mul _ _ hf hg
  | smul _ _ _ hf => exact smul _ _ hf

Premises used: star_eq_iff_star_eq, rfl
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
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)
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

Tactic:
f.induction_on zero id star_id add mul smul fun h f ↦ frequently f ?_

Premises used: ContinuousMapZero.induction_on
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
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)
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), 𝕜)₀
refine :
  ∀
    (h :
      ∀ (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), 𝕜)₀), ∃ᶠ (g : C((↑s : Type u_1), 𝕜)₀) in 𝓝 f, p g
⊢ p f

Tactic:
refine f.induction_on zero id star_id add mul smul fun h f ↦ frequently f ?_
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
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)
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 (γ := 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), 𝕜)₀
⊢ f ∈
    closure
      (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀) :
        Set C((↑s : Type u_1), 𝕜)₀)

Tactic:
have := (ContinuousMapZero.adjoin_id_dense s).closure_eq ▸ Set.mem_univ (x := f)
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
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)
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 (γ := 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), 𝕜)₀
this :
  f ∈
    closure
      (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀) :
        Set C((↑s : Type u_1), 𝕜)₀)
⊢ ∃ᶠ (g : C((↑s : Type u_1), 𝕜)₀) in 𝓝 f, p g

Tactic:
mem_closure_iff_frequently.mp this |>.mp <| .of_forall h

Premises used: mem_closure_iff_frequently, Filter.Eventually.of_forall, Iff.mp, Filter.Frequently.mp
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
s : Set 𝕜
inst_1 : Fact (0 ∈ s)
inst_2 : CompactSpace.{u_1} (↑s : Type u_1)
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)
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 (γ := 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), 𝕜)₀
this :
  f ∈
    closure
      (↑(adjoin 𝕜 (A := C((↑s : Type u_1), 𝕜)₀) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 C((↑s : Type u_1), 𝕜)₀) :
        Set C((↑s : Type u_1), 𝕜)₀)
⊢ ∃ᶠ (g : C((↑s : Type u_1), 𝕜)₀) in 𝓝 f, p g

Tactic:
exact mem_closure_iff_frequently.mp this |>.mp <| .of_forall h

Premises used: mem_closure_iff_frequently, Iff.mp, Filter.Frequently.mp
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : IsScalarTower 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0
hmul_star_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) 0 : A) a = 0

Tactic:
simp [map_zero]

Premises used: map_zero
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : IsScalarTower 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0
hmul_star_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0

Tactic:
hmul_id
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : IsScalarTower 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0
hmul_star_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0

Tactic:
exact hmul_id
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : IsScalarTower 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0
hmul_star_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0

Tactic:
hmul_star_id
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : IsScalarTower 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0
hmul_star_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0

Tactic:
exact hmul_star_id
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : IsScalarTower 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0
hmul_star_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
f g : C((↑s : Type u_2), 𝕜)₀
h₁ : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0
h₂ : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) a = 0
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (f + g) : A) a = 0

Tactic:
simp only [map_add, add_mul, h₁, h₂, zero_add]

Premises used: add_mul, map_add, zero_add
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : IsScalarTower 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0
hmul_star_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
f g : C((↑s : Type u_2), 𝕜)₀
h_1 : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0
h : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) a = 0
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (f * g) : A) a = 0

Tactic:
simp only [map_mul, mul_assoc, h, mul_zero]

Premises used: mul_assoc, MulZeroClass.mul_zero, map_mul
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : IsScalarTower 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0
hmul_star_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
r : 𝕜
f : C((↑s : Type u_2), 𝕜)₀
h : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0
smul : HSMul.hSMul (β := A) r ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) * a = 0
smul₁ : r • HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0
smul₂ : HSMul.hSMul (β := A) r 0 = 0
smul₃ smul₄ : Eq.{u_3 + 1} (α := A) 0 0
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : A) a = 0

Tactic:
rw [map_smul, smul_mul_assoc, h, smul_zero]

Premises used: smul_zero, smul_mul_assoc, map_smul
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : IsScalarTower 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0
hmul_star_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
f : C((↑s : Type u_2), 𝕜)₀
h : ∃ᶠ (g : C((↑s : Type u_2), 𝕜)₀) in nhds f, HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) a = 0
⊢ Continuous.{u_2, u_3} (Y := A) fun (g : C((↑s : Type u_2), 𝕜)₀) ↦
    HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) a

Tactic:
fun_prop
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : IsScalarTower 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0
hmul_star_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
f : C((↑s : Type u_2), 𝕜)₀
h : ∃ᶠ (g : C((↑s : Type u_2), 𝕜)₀) in nhds f, HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) a = 0
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0

Tactic:
exact h.mem_of_closed <| isClosed_eq (by fun_prop) continuous_zero

Premises used: continuous_zero, isClosed_eq, Filter.Frequently.mem_of_closed
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : IsScalarTower 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0
hmul_star_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
f : C((↑s : Type u_2), 𝕜)₀
zero : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) 0 : A) a = 0
id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) a = 0
star_id : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) a = 0
add :
  ∀ (f g : C((↑s : Type u_2), 𝕜)₀) (h₁ : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0)
    (h₂ : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) a = 0),
    HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (f + g) : A) a = 0
mul :
  ∀ (f g : C((↑s : Type u_2), 𝕜)₀),
    HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0 →
      ∀ (h : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) a = 0),
        HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (f * g) : A) a = 0
smul :
  ∀ (r : 𝕜) (f : C((↑s : Type u_2), 𝕜)₀) (h : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0),
    HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : A) a = 0
frequently :
  ∀ (f : C((↑s : Type u_2), 𝕜)₀)
    (h :
      ∃ᶠ (g : C((↑s : Type u_2), 𝕜)₀) in nhds f,
        HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) a = 0),
    HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0

Tactic:
induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simp [map_zero]
  | id => exact hmul_id
  | star_id => exact hmul_star_id
  | add _ _ h₁ h₂ => simp only [map_add, add_mul, h₁, h₂, zero_add]
  | mul _ _ _ h => simp only [map_mul, mul_assoc, h, mul_zero]
  | smul _ _ h => rw [map_smul, smul_mul_assoc, h, smul_zero]
  | frequently f h => exact h.mem_of_closed <| isClosed_eq (by fun_prop) continuous_zero

Premises used: add_mul, mul_assoc, smul_zero, map_zero, map_add, id, smul_mul_assoc, zero_add, Submodule.mul, MulZeroClass.mul_zero, continuous_zero, map_mul, Submodule.smul, isClosed_eq, Submodule.zero, Submodule.add, map_smul
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : SMulCommClass 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) = 0
hmul_star_id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) 0 : A) = 0

Tactic:
simp [map_zero]

Premises used: map_zero
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : SMulCommClass 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) = 0
hmul_star_id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) = 0

Tactic:
hmul_id
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
𝕜 : Type u_2
A : Type u_3
inst : RCLike 𝕜
inst_1 : NonUnitalSemiring A
inst_2 : Star A
inst_3 : TopologicalSpace A
inst_4 : SeparatelyContinuousMul A
inst_5 : T2Space A
inst_6 : DistribMulAction 𝕜 A
inst_7 : SMulCommClass 𝕜 A A
s : Set 𝕜
inst_8 : Fact (0 ∈ s)
inst_9 : CompactSpace.{u_2} (↑s : Type u_2)
φ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) = 0
hmul_star_id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) = 0
hφ : Continuous.{u_2, u_3} (X := C((↑s : Type u_2), 𝕜)₀) (Y := A) (⇑φ : (a : C((↑s : Type u_2), 𝕜)₀) → A)
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) = 0

Tactic:
exact hmul_id