awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (star (ContinuousMapZero.id s)) : 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 : 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) (star (ContinuousMapZero.id s)) : 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 : 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 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:
simp only [map_add, mul_add, h₁, h₂, zero_add]

Premises used: map_add, zero_add, mul_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 : 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 g : C((↑s : Type u_2), 𝕜)₀
h : HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) f : A) = 0
h_1 : 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:
simp only [map_mul, ← mul_assoc, h, zero_mul]

Premises used: MulZeroClass.zero_mul, mul_assoc, 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 : 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
smul₃ smul₄ : Eq.{u_3 + 1} (α := A) 0 0
⊢ HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) (r • f) : A) = 0

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

Premises used: smul_zero, mul_smul_comm, 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)
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
⊢ Continuous.{u_2, u_3} (Y := A) fun (g : C((↑s : Type u_2), 𝕜)₀) ↦
    HMul.hMul (β := A) a ((φ : (a : C((↑s : Type u_2), 𝕜)₀) → A) g : 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 : 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), 𝕜)₀
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:
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 : 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
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
⊢ 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

Premises used: MulZeroClass.zero_mul, mul_assoc, smul_zero, map_zero, map_add, id, zero_add, Submodule.mul, continuous_zero, map_mul, Submodule.smul, isClosed_eq, mul_smul_comm, Submodule.zero, mul_add, Submodule.add, map_smul
-- Module: Mathlib.Topology.ContinuousMap.T0Sierpinski
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsInducing (Y := (i : Opens X) → Prop) fun (x : X) (i : Opens X) ↦ x ∈ i

Tactic:
inducing_iInf_to_pi fun (u : Opens X) (x : X) => x ∈ u

Premises used: Membership.mem, inducing_iInf_to_pi
-- Module: Mathlib.Topology.ContinuousMap.T0Sierpinski
Goal:
X : Type u_1
inst : TopologicalSpace X
h : inst = ⨅ (i : Opens X), induced (Y := Prop) (fun (x : X) ↦ x ∈ i) inferInstance
⊢ IsInducing (X := X) (Y := Opens X → Prop) (⇑(productOfMemOpens X) : (a : X) → Opens X → Prop)

Tactic:
convert! inducing_iInf_to_pi fun (u : Opens X) (x : X) => x ∈ u

Premises used: Membership.mem, inducing_iInf_to_pi
-- Module: Mathlib.Topology.ContinuousMap.T0Sierpinski
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ inst = ⨅ (i : Opens X), induced (Y := Prop) (fun (x : X) ↦ x ∈ i) inferInstance

Tactic:
apply eq_induced_by_maps_to_sierpinski

Premises used: TopologicalSpace.eq_induced_by_maps_to_sierpinski
-- Module: Mathlib.Topology.ContinuousMap.T0Sierpinski
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 x1 x2
⊢ x1 = x2

Tactic:
apply Inseparable.eq

Premises used: Inseparable.eq
-- Module: Mathlib.Topology.ContinuousMap.T0Sierpinski
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)
h₂ 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)
⊢ Inseparable x1 x2

Tactic:
rw [← IsInducing.inseparable_iff (productOfMemOpens_isInducing X), h]

Premises used: TopologicalSpace.productOfMemOpens_isInducing, Topology.IsInducing.inseparable_iff
-- Module: Mathlib.Topology.ContinuousMap.T0Sierpinski
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
⊢ IsEmbedding (X := X) (Y := Opens X → Prop) (⇑(productOfMemOpens X) : (a : X) → Opens X → Prop)

Tactic:
.mk (productOfMemOpens_isInducing X) (productOfMemOpens_injective X)

Premises used: TopologicalSpace.productOfMemOpens_injective, TopologicalSpace.productOfMemOpens_isInducing, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.ContinuousMap.Units
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : Monoid M
inst_2 : TopologicalSpace M
inst_3 : ContinuousMul M
f : ContinuousMap.{u_1, u_2} X Mˣ
x : X
⊢ Eq.{u_2 + 1} (α := M) (((↑((unitsLift : (a : C(X, Mˣ)) → C(X, M)ˣ) f)⁻¹ : C(X, M)) : (a : X) → M) x : M)
    ((↑((f : (a : X) → Mˣ) x)⁻¹ : M) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Units
Goal:
X : Type u_1
M : Type u_2
inst : TopologicalSpace X
inst_1 : Monoid M
inst_2 : TopologicalSpace M
inst_3 : ContinuousMul M
f : C(X, M)ˣ
x : X
⊢ Eq.{u_2 + 1} (α := M)
    ((↑((((Equiv.symm unitsLift : (a : C(X, M)ˣ) → C(X, Mˣ)) f : ContinuousMap.{u_1, u_2} X Mˣ) : (a : X) → Mˣ) x)⁻¹ :
        M) :
      M)
    (((↑f⁻¹ : C(X, M)) : (a : X) → M) x : M)

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Units
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

Tactic:
continuous_induced_rng.2
      (Continuous.prodMk f.continuous
        (MulOpposite.continuous_op.comp (continuous_iff_continuousAt.mpr fun x => ?_)))

Premises used: Iff.mpr, ContinuousMap.continuous, Continuous.comp, MulOpposite.continuous_op, continuous_iff_continuousAt, Continuous.prodMk, continuous_induced_rng
-- Module: Mathlib.Topology.ContinuousMap.Units
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)
fun : ∀ (x : X), ContinuousAt.{u_1, u_3} (Y := R) (fun (x : X) ↦ (↑((fun (x : X) ↦ ⋯.unit) x)⁻¹ : R)) x
⊢ Continuous.{u_1, u_3} (Y := Rˣ) fun (x : X) ↦ ⋯.unit

Tactic:
refine
    continuous_induced_rng.2
      (Continuous.prodMk f.continuous
        (MulOpposite.continuous_op.comp (continuous_iff_continuousAt.mpr fun x => ?_)))

Premises used: Iff.mpr, Continuous.comp, MulOpposite.continuous_op, continuous_iff_continuousAt, Continuous.prodMk, continuous_induced_rng
-- Module: Mathlib.Topology.ContinuousMap.Units
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 Ring.inverse (↑⋯.unit : R)

Tactic:
have := NormedRing.inverse_continuousAt (h x).unit
-- Module: Mathlib.Topology.ContinuousMap.Units
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)
simp : ContinuousAt.{u_1, u_3} (Y := R) (fun (x : X) ↦ (↑⋯.unit⁻¹ : R)) x
⊢ ContinuousAt.{u_1, u_3} (Y := R) (fun (x : X) ↦ (↑((fun (x : X) ↦ ⋯.unit) x)⁻¹ : R)) x

Tactic:
simp only
-- Module: Mathlib.Topology.ContinuousMap.Units
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)
simp : ContinuousAt.{u_1, u_3} (Y := R) (fun (x : X) ↦ Ring.inverse ((f : (a : X) → R) x)) x
⊢ ContinuousAt.{u_1, u_3} (Y := R) (fun (x : X) ↦ (↑⋯.unit⁻¹ : R)) x

Tactic:
simp only [← Ring.inverse_unit, IsUnit.unit_spec] at this ⊢

Premises used: Ring.inverse_unit, IsUnit.unit_spec
-- Module: Mathlib.Topology.ContinuousMap.Units
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.{u_3, u_3} (X := R) (Y := R) (Ring.inverse : R → R) ((f : (a : X) → R) x : R)
⊢ ContinuousAt.{u_1, u_3} (Y := R) (fun (x : X) ↦ Ring.inverse ((f : (a : X) → R) x)) x

Tactic:
this.comp (f.continuousAt x)

Premises used: Ring.inverse, dite, ContinuousAt.comp, ContinuousMap.continuousAt
-- Module: Mathlib.Topology.ContinuousMap.Units
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.{u_3, u_3} (X := R) (Y := R) (Ring.inverse : R → R) ((f : (a : X) → R) x : R)
⊢ ContinuousAt.{u_1, u_3} (Y := R) (fun (x : X) ↦ Ring.inverse ((f : (a : X) → R) x)) x

Tactic:
exact this.comp (f.continuousAt x)

Premises used: ContinuousAt.comp, ContinuousMap.continuousAt
-- Module: Mathlib.Topology.ContinuousMap.Units
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)
h₁ :
  ∀ (a : X),
    Eq.{u_3 + 1} (α := R)
      (({ toFun := fun (x : X) ↦ (↑((unitsOfForallIsUnit h : (a : X) → Rˣ) x) : R), continuous_toFun := ⋯ : C(X, R) } :
            (a : X) → R)
          a :
        R)
      ((f : (a : X) → R) a : R)
⊢ { toFun := fun (x : X) ↦ (↑((unitsOfForallIsUnit h : (a : X) → Rˣ) x) : R), continuous_toFun := ⋯ : C(X, R) } = f

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Units
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)
a : X
⊢ Eq.{u_3 + 1} (α := R)
    (({ toFun := fun (x : X) ↦ (↑((unitsOfForallIsUnit h : (a : X) → Rˣ) x) : R), continuous_toFun := ⋯ : C(X, R) } :
          (a : X) → R)
        a :
      R)
    ((f : (a : X) → R) a : R)

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Units
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)
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)
⊢ (↑((unitsLift : (a : C(X, Rˣ)) → C(X, R)ˣ) (unitsOfForallIsUnit h)) : C(X, R)) = f

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Units
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)
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:
rfl
-- Module: Mathlib.Topology.ContinuousMap.Units
Goal:
X : Type u_1
R : Type u_3
inst : TopologicalSpace X
inst_1 : NormedDivisionRing R
inst_2 : CompleteSpace R
f : C(X, R)
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)
⊢ IsUnit f ↔ ∀ (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]

Premises used: ContinuousMap.isUnit_iff_forall_isUnit, isUnit_iff_ne_zero
-- Module: Mathlib.Topology.ContinuousMap.Units
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)
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
⊢ 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))

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.Units
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)
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:
simp only [spectrum.mem_iff, isUnit_iff_forall_ne_zero, not_forall, sub_apply,
    Classical.not_not, Set.mem_range,
    sub_eq_zero, @eq_comm _ (x • 1 : R) _, Set.mem_preimage, Algebra.algebraMap_eq_smul_one,
    smul_apply, one_apply]

Premises used: Set.mem_range, Classical.not_not, sub_eq_zero, ContinuousMap.smul_apply, ContinuousMap.one_apply, eq_comm, Algebra.algebraMap_eq_smul_one, spectrum.mem_iff, Classical.not_forall, ContinuousMap.isUnit_iff_forall_ne_zero, ContinuousMap.sub_apply, Set.mem_preimage
-- Module: Mathlib.Topology.ContinuousMap.Units
Goal:
X : Type u_1
𝕜 : Type u_4
inst : TopologicalSpace X
inst_1 : NormedField 𝕜
inst_2 : CompleteSpace 𝕜
f : C(X, 𝕜)
rw :
  Eq (α := Set 𝕜)
    (Set.preimage (β := 𝕜) (⇑(RingHom.id 𝕜) : (a : 𝕜) → 𝕜) (Set.range.{u_4, u_1 + 1} (ι := X) (⇑f : (a : X) → 𝕜)))
    (Set.range.{u_4, u_1 + 1} (ι := X) (⇑f : (a : X) → 𝕜))
⊢ spectrum 𝕜 f = Set.range.{u_4, u_1 + 1} (ι := X) (⇑f : (a : X) → 𝕜)

Tactic:
rw [spectrum_eq_preimage_range, Algebra.algebraMap_self]

Premises used: Algebra.algebraMap_self, ContinuousMap.spectrum_eq_preimage_range
-- Module: Mathlib.Topology.ContinuousMap.Units
Goal:
X : Type u_1
𝕜 : Type u_4
inst : TopologicalSpace X
inst_1 : NormedField 𝕜
inst_2 : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ Eq (α := Set 𝕜)
    (Set.preimage (β := 𝕜) (⇑(RingHom.id 𝕜) : (a : 𝕜) → 𝕜) (Set.range.{u_4, u_1 + 1} (ι := X) (⇑f : (a : X) → 𝕜)))
    (Set.range.{u_4, u_1 + 1} (ι := X) (⇑f : (a : X) → 𝕜))

Tactic:
Set.preimage_id

Premises used: Set.preimage_id
-- Module: Mathlib.Topology.ContinuousMap.Units
Goal:
X : Type u_1
𝕜 : Type u_4
inst : TopologicalSpace X
inst_1 : NormedField 𝕜
inst_2 : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ Eq (α := Set 𝕜)
    (Set.preimage (β := 𝕜) (⇑(RingHom.id 𝕜) : (a : 𝕜) → 𝕜) (Set.range.{u_4, u_1 + 1} (ι := X) (⇑f : (a : X) → 𝕜)))
    (Set.range.{u_4, u_1 + 1} (ι := X) (⇑f : (a : X) → 𝕜))

Tactic:
exact Set.preimage_id

Premises used: Set.preimage_id
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
h : LE.le (α := Subalgebra ℝ C((↑I : Type), ℝ)) ⊤ (Subalgebra.topologicalClosure (polynomialFunctions I))
⊢ Eq (α := Subalgebra ℝ C((↑I : Type), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions I)) ⊤

Tactic:
apply top_unique

Premises used: top_unique
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
f : C((↑I : Type), ℝ)
⊢ Membership.mem (γ := Subalgebra ℝ C((↑I : Type), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions I)) f

Tactic:
mem_closure_of_tendsto (bernsteinApproximation_uniform f) <| .of_forall fun n ↦ ?_

Premises used: Set.Mem, setOf, Filter.Eventually.of_forall, closure, bernsteinApproximation_uniform, Set.sInter, mem_closure_of_tendsto
-- Module: Mathlib.Topology.ContinuousMap.Weierstrass
Goal:
f : C((↑I : Type), ℝ)
h :
  ∀ (n : ℕ), bernsteinApproximation n f ∈ (↑(Subalgebra.toSubsemiring (polynomialFunctions I)) : Set C((↑I : Type), ℝ))
⊢ Membership.mem (γ := Subalgebra ℝ C((↑I : Type), ℝ)) (Subalgebra.topologicalClosure (polynomialFunctions I)) f

Tactic:
refine mem_closure_of_tendsto (bernsteinApproximation_uniform f) <| .of_forall fun n ↦ ?_

Premises used: bernsteinApproximation_uniform, mem_closure_of_tendsto