awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ HMul.hMul (α := A) ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) a = 0
have 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
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 : 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)
r : 𝕜
f : C((↑s : Type u_2), 𝕜)₀
h : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : A) = 0
have smul : a * HSMul.hSMul (β := A) r ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
Tactic: rw [map_smul, mul_smul_comm, 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 : 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)
r : 𝕜
f : C((↑s : Type u_2), 𝕜)₀
h : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
smul : a * HSMul.hSMul (β := A) r ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : A) = 0
have smul₁ : r • HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
Tactic: rw [map_smul, mul_smul_comm, 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 : 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)
r : 𝕜
f : C((↑s : Type u_2), 𝕜)₀
h : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
smul : a * HSMul.hSMul (β := A) r ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
smul₁ : r • HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : A) = 0
have smul₂ : HSMul.hSMul (β := A) r 0 = 0
Tactic: rw [map_smul, mul_smul_comm, 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 : 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)
r : 𝕜
f : C((↑s : Type u_2), 𝕜)₀
h : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
smul : a * HSMul.hSMul (β := A) r ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
smul₁ : r • HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
smul₂ : HSMul.hSMul (β := A) r 0 = 0
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : A) = 0
have smul₃ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [map_smul, mul_smul_comm, 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 : 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)
f : C((↑s : Type u_2), 𝕜)₀
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
have zero : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) 0 : 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, mul_add, h₁, h₂, zero_add]
  | mul _ _ h _ => simp only [map_mul, ← mul_assoc, h, zero_mul]
  | smul _ _ h => rw [map_smul, mul_smul_comm, 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 : 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)
f : C((↑s : Type u_2), 𝕜)₀
zero : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) 0 : A) = 0
id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) = 0
star_id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) = 0
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
have add : ∀ (f g : C((↑s : Type u_2), 𝕜)₀) (h₁ : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0)
  (h₂ : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) = 0),
  HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (f + g) : 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, mul_add, h₁, h₂, zero_add]
  | mul _ _ h _ => simp only [map_mul, ← mul_assoc, h, zero_mul]
  | smul _ _ h => rw [map_smul, mul_smul_comm, 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 : 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)
f : C((↑s : Type u_2), 𝕜)₀
zero : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) 0 : A) = 0
id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) = 0
star_id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) = 0
add :
  ∀ (f g : C((↑s : Type u_2), 𝕜)₀) (h₁ : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0)
    (h₂ : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) = 0),
    HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (f + g) : A) = 0
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
have mul : ∀ (f g : C((↑s : Type u_2), 𝕜)₀) (h : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0),
  HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) = 0 →
    HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (f * g) : 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, mul_add, h₁, h₂, zero_add]
  | mul _ _ h _ => simp only [map_mul, ← mul_assoc, h, zero_mul]
  | smul _ _ h => rw [map_smul, mul_smul_comm, 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 : 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)
f : C((↑s : Type u_2), 𝕜)₀
zero : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) 0 : A) = 0
id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) = 0
star_id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) = 0
add :
  ∀ (f g : C((↑s : Type u_2), 𝕜)₀) (h₁ : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0)
    (h₂ : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) = 0),
    HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (f + g) : A) = 0
mul :
  ∀ (f g : C((↑s : Type u_2), 𝕜)₀) (h : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0),
    HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) = 0 →
      HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (f * g) : A) = 0
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
have smul : ∀ (r : 𝕜) (f : C((↑s : Type u_2), 𝕜)₀) (h : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0),
  HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : 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, mul_add, h₁, h₂, zero_add]
  | mul _ _ h _ => simp only [map_mul, ← mul_assoc, h, zero_mul]
  | smul _ _ h => rw [map_smul, mul_smul_comm, 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 : 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)
f : C((↑s : Type u_2), 𝕜)₀
zero : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) 0 : A) = 0
id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (ContinuousMapZero.id s) : A) = 0
star_id : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (star (ContinuousMapZero.id s)) : A) = 0
add :
  ∀ (f g : C((↑s : Type u_2), 𝕜)₀) (h₁ : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0)
    (h₂ : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) = 0),
    HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (f + g) : A) = 0
mul :
  ∀ (f g : C((↑s : Type u_2), 𝕜)₀) (h : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0),
    HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) = 0 →
      HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (f * g) : A) = 0
smul :
  ∀ (r : 𝕜) (f : C((↑s : Type u_2), 𝕜)₀) (h : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0),
    HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : A) = 0
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
have frequently : ∀ (f : C((↑s : Type u_2), 𝕜)₀)
  (h :
    ∃ᶠ (g : C((↑s : Type u_2), 𝕜)₀) in nhds f, HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : A) = 0),
  HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : 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, mul_add, h₁, h₂, zero_add]
  | mul _ _ h _ => simp only [map_mul, ← mul_assoc, h, zero_mul]
  | smul _ _ h => rw [map_smul, mul_smul_comm, 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.T0Sierpinski (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsInducing (X := X) (Y := Opens X → Prop) (⇑(productOfMemOpens X) : (a : X) → Opens X → Prop)
have h : inst = ⨅ (i : Opens X), induced (Y := Prop) (fun (x : X) ↦ x ∈ i) inferInstance
Tactic: convert! inducing_iInf_to_pi fun (u : Opens X) (x : X) => x ∈ u
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.T0Sierpinski (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
x1 x2 : X
h :
  Eq (α := Opens X → Prop) ((productOfMemOpens X : (a : X) → Opens X → Prop) x1 : Opens X → Prop)
    ((productOfMemOpens X : (a : X) → Opens X → Prop) x2 : Opens X → Prop)
⊢ x1 = x2
have h₁ : Inseparable x1 x2
Tactic: apply Inseparable.eq
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.T0Sierpinski (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
x1 x2 : X
h :
  Eq (α := Opens X → Prop) ((productOfMemOpens X : (a : X) → Opens X → Prop) x1 : Opens X → Prop)
    ((productOfMemOpens X : (a : X) → Opens X → Prop) x2 : Opens X → Prop)
⊢ Inseparable x1 x2
have h₁ : Inseparable (X := Opens X → Prop) ((productOfMemOpens X : (a : X) → Opens X → Prop) x1 : Opens X → Prop)
  ((productOfMemOpens X : (a : X) → Opens X → Prop) x2 : Opens X → Prop)
Tactic: rw [← IsInducing.inseparable_iff (productOfMemOpens_isInducing X), h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.T0Sierpinski (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
x1 x2 : X
h :
  Eq (α := Opens X → Prop) ((productOfMemOpens X : (a : X) → Opens X → Prop) x1 : Opens X → Prop)
    ((productOfMemOpens X : (a : X) → Opens X → Prop) x2 : Opens X → Prop)
h₁ :
  Inseparable (X := Opens X → Prop) ((productOfMemOpens X : (a : X) → Opens X → Prop) x1 : Opens X → Prop)
    ((productOfMemOpens X : (a : X) → Opens X → Prop) x2 : Opens X → Prop)
⊢ Inseparable x1 x2
have h₂ : Inseparable (X := Opens X → Prop) ((productOfMemOpens X : (a : X) → Opens X → Prop) x2 : Opens X → Prop)
  ((productOfMemOpens X : (a : X) → Opens X → Prop) x2 : Opens X → Prop)
Tactic: rw [← IsInducing.inseparable_iff (productOfMemOpens_isInducing X), h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Units (goal)
Goal:
X : Type u_1
R : Type u_3
inst : TopologicalSpace X
inst_1 : NormedRing R
inst_2 : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit.{u_3} (M := R) ((f : (a : X) → R) x : R)
⊢ Continuous.{u_1, u_3} (Y := Rˣ) fun (x : X) ↦ ⋯.unit
have fun : ∀ (x : X), ContinuousAt.{u_1, u_3} (Y := R) (fun (x : X) ↦ (↑((fun (x : X) ↦ sorry.unit) x)⁻¹ : R)) x
Tactic: refine
    continuous_induced_rng.2
      (Continuous.prodMk f.continuous
        (MulOpposite.continuous_op.comp (continuous_iff_continuousAt.mpr fun x => ?_)))
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Units (hypothesis)
Goal:
X : Type u_1
R : Type u_3
inst : TopologicalSpace X
inst_1 : NormedRing R
inst_2 : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit.{u_3} (M := R) ((f : (a : X) → R) x : R)
x : X
⊢ ContinuousAt.{u_1, u_3} (Y := R) (fun (x : X) ↦ (↑((fun (x : X) ↦ ⋯.unit) x)⁻¹ : R)) x
have this : ContinuousAt Ring.inverse (↑sorry.unit : R)
Tactic: have := NormedRing.inverse_continuousAt (h x).unit
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Units (goal)
Goal:
X : Type u_1
R : Type u_3
inst : TopologicalSpace X
inst_1 : NormedRing R
inst_2 : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit.{u_3} (M := R) ((f : (a : X) → R) x : R)
x : X
this : ContinuousAt Ring.inverse (↑⋯.unit : R)
⊢ ContinuousAt.{u_1, u_3} (Y := R) (fun (x : X) ↦ (↑⋯.unit⁻¹ : R)) x
have simp : ContinuousAt.{u_1, u_3} (Y := R) (fun (x : X) ↦ Ring.inverse ((f : (a : X) → R) x)) x
Tactic: simp only [← Ring.inverse_unit, IsUnit.unit_spec] at this ⊢
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Units (goal)
Goal:
X : Type u_1
M : Type u_2
R : Type u_3
𝕜 : Type u_4
inst : TopologicalSpace X
inst_1 : NormedRing R
inst_2 : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit.{u_3} (M := R) ((f : (a : X) → R) x : R)
⊢ { toFun := fun (x : X) ↦ (↑((unitsOfForallIsUnit h : (a : X) → Rˣ) x) : R), continuous_toFun := ⋯ : C(X, R) } = f
have h₁ : ∀ (a : X),
  Eq.{u_3 + 1} (α := R)
    (({ toFun := fun (x : X) ↦ (↑((unitsOfForallIsUnit h : (a : X) → Rˣ) x) : R), continuous_toFun := sorry : C(X, R) } :
          (a : X) → R)
        a :
      R)
    ((f : (a : X) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Units (goal)
Goal:
X : Type u_1
R : Type u_3
inst : TopologicalSpace X
inst_1 : NormedRing R
inst_2 : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit.{u_3} (M := R) ((f : (a : X) → R) x : R)
⊢ (↑((unitsLift : (a : C(X, Rˣ)) → C(X, R)ˣ) (unitsOfForallIsUnit h)) : C(X, R)) = f
have h₁ : ∀ (a : X),
  Eq.{u_3 + 1} (α := R)
    (((↑((unitsLift : (a : C(X, Rˣ)) → C(X, R)ˣ) (unitsOfForallIsUnit h)) : C(X, R)) : (a : X) → R) a : R)
    ((f : (a : X) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Units (goal)
Goal:
X : Type u_1
R : Type u_3
inst : TopologicalSpace X
inst_1 : NormedDivisionRing R
inst_2 : CompleteSpace R
f : C(X, R)
⊢ IsUnit f ↔ ∀ (x : X), Ne.{u_3 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
have simp_rw : (∀ (x : X), IsUnit.{u_3} (M := R) ((f : (a : X) → R) x : R)) ↔
  ∀ (x : X), Ne.{u_3 + 1} (α := R) ((f : (a : X) → R) x : R) (0 : R)
Tactic: simp_rw [f.isUnit_iff_forall_isUnit, isUnit_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Units (goal)
Goal:
X : Type u_1
R : Type u_3
𝕜 : Type u_4
inst : TopologicalSpace X
inst_1 : NormedField 𝕜
inst_2 : NormedDivisionRing R
inst_3 : Algebra 𝕜 R
inst_4 : CompleteSpace R
f : C(X, R)
⊢ spectrum 𝕜 f =
    Set.preimage.{u_4, u_3} (β := R) (⇑(algebraMap 𝕜 R) : (a : 𝕜) → R)
      (Set.range.{u_3, u_1 + 1} (ι := X) (⇑f : (a : X) → R))
have h : ∀ (x : 𝕜),
  x ∈ spectrum 𝕜 f ↔
    Membership.mem (γ := Set 𝕜)
      (Set.preimage.{u_4, u_3} (β := R) (⇑(algebraMap 𝕜 R) : (a : 𝕜) → R)
        (Set.range.{u_3, u_1 + 1} (ι := X) (⇑f : (a : X) → R)))
      x
Tactic: ext x