awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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
⊢ p f
have 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
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
Cleared hypotheses: hf
-- 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_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
⊢ p f
have 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)
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
Cleared hypotheses: hf
-- 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_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)
⊢ p f
have 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)
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
Cleared hypotheses: hf
-- 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_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)
⊢ p f
have 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)
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
Cleared hypotheses: hf
-- 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)
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
have 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
Tactic: refine f.induction_on zero id star_id add mul smul 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 : 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), 𝕜)₀
⊢ ∃ᶠ (g : C((↑s : Type u_1), 𝕜)₀) in 𝓝 f, p g
have 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), 𝕜)₀)
Tactic: have := (ContinuousMapZero.adjoin_id_dense s).closure_eq ▸ Set.mem_univ (x := f)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : A) a = 0
have smul : HSMul.hSMul (β := A) r ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) * a = 0
Tactic: rw [map_smul, smul_mul_assoc, h, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : A) a = 0
have smul₁ : r • HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0
Tactic: rw [map_smul, smul_mul_assoc, h, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : A) a = 0
have smul₂ : HSMul.hSMul (β := A) r 0 = 0
Tactic: rw [map_smul, smul_mul_assoc, h, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : A) a = 0
have smul₃ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [map_smul, smul_mul_assoc, h, smul_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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), 𝕜)₀
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0
have zero : HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) 0 : 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
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0
have 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
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
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0
have 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
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
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0
have 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
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
Cleared hypotheses: f