mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: case mpr.refine_1
a b : ℝ
h : a < b
p : ℝ[X]
q : ℝ[X] := p.comp ((b - a) • X + Polynomial.C a)
⊢ q ∈ ↑⊤.toSubsemiring

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
p : ℚ[X]
m : p ∈ span ℚ (Set.range fun k_1 ↦ bernsteinPolynomial ℚ n ↑k_1)
⊢ eval 1 ((⇑derivative)^[n - k] 0) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ (X + (1 - X)) ^ n = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
⊢ f ∈ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
⊢ 0 • bernsteinPolynomial R n 0 = ↑0 * X ^ (0 - 1) * (1 - X) ^ (n - 0) * ↑(n.choose 0) * X

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n ν : ℕ
x : ↑I
⊢ { toFun := fun x ↦ Polynomial.eval (↑x) (↑(n.choose ν) * Polynomial.X ^ ν * (1 - Polynomial.X) ^ (n - ν)),
        continuous_toFun := ⋯ }
      x =
    ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: case e'_3
n : ℕ
hn : n ≠ 0
x : ↑I
⊢ ↑x * (1 - ↑x) / ↑n = (Polynomial.aeval ↑x) (n • Polynomial.X * (1 - Polynomial.X)) / ↑n ^ 2

Tactic:
simp

Goal state after:
case e'_3
n : ℕ
hn : n ≠ 0
x : ↑I
⊢ ↑x * (1 - ↑x) / ↑n = ↑n * ↑x * (1 - ↑x) / ↑n ^ 2
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
⊢ (0 * (0 - 1)) • bernsteinPolynomial R n 0 =
    ↑(n.choose 0) * ((1 - X) ^ (n - 0) * (↑0 * (↑(0 - 1) * X ^ (0 - 1 - 1)))) * X ^ 2

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
⊢ ((0 + 1) * (0 + 1 - 1)) • bernsteinPolynomial R n (0 + 1) =
    ↑(n.choose (0 + 1)) * ((1 - X) ^ (n - (0 + 1)) * (↑(0 + 1) * (↑(0 + 1 - 1) * X ^ (0 + 1 - 1 - 1)))) * X ^ 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁹ : CommRing R
inst✝¹⁸ : PartialOrder R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalRing R
inst✝¹³ : ContinuousStar R
inst✝¹² : ContinuousSqrt R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NoZeroDivisors R
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hg : ContinuousOn g (σₙ R a)
hf0 : f 0 = 0
hg0 : g 0 = 0
ha : p a
⊢ (∀ (x : ↑(σₙ R a)),
      { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ } x ≤
        { toFun := (σₙ R a).domRestrict g, continuous_toFun := ⋯, map_zero' := ⋯ } x) ↔
    ∀ x ∈ σₙ R a, f x ≤ g x

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : Semifield R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C(↑(σₙ R a), R)₀
h :
  ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
            toContinuousMapHom).toNonUnitalAlgHom
      f =
    ↑((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp
            toContinuousMapHom).toNonUnitalAlgHom
      g
⊢ f 0 = g 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
a✝ : X
⊢ ((g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound) a✝ = Polynomial.eval (↑f a✝) g

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑A = ↑A.topologicalClosure

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case e'_2.e'_3
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
u v : C(↑(σₙ R a), R)₀
⊢ (((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (u, v)).1 = 0

Tactic:
ext ⟨x, rfl⟩

Goal state after:
case e'_2.e'_3
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
u v : C(↑(σₙ R a), R)₀
⊢ (((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (u, v)).1 PUnit.unit = 0 PUnit.unit
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case e'_2.e'_4
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
u v : C(↑(σₙ R a), R)₀
⊢ (((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (u, v)).2 = 0

Tactic:
ext ⟨x, rfl⟩

Goal state after:
case e'_2.e'_4
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : Semifield R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra R A
inst✝¹ : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst✝ : CompleteSpace R
a : A
ha : p a
f : C(↑(spectrum R a), ↑(σₙ R a)) := { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
this✝ :
  inferInstance =
    UniformSpace.comap (fun x ↦ x.comp f) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp 0) inferInstance
this : ∀ U ∈ 𝓤 C(Unit, R), (0, 0) ∈ U
u v : C(↑(σₙ R a), R)₀
⊢ (((Prod.map (fun x ↦ x.comp 0) fun x ↦ x.comp 0) ∘ fun x ↦ (↑x.1, ↑x.2)) (u, v)).2 PUnit.unit = 0 PUnit.unit
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case calc_1.e_a.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
m : 0 ∈ Finset.range (n + 1)
⊢ (↑n * X - ↑0) ^ 2 = ↑0 * ↑(0 - 1) + (1 - 2 * ↑n * X) * ↑0 + ↑n ^ 2 * X ^ 2

Tactic:
simp

Goal state after:
case calc_1.e_a.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
m : 0 ∈ Finset.range (n + 1)
⊢ (↑n * X) ^ 2 = ↑n ^ 2 * X ^ 2
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case calc_1.e_a.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
n✝ : ℕ
m : n✝ + 1 ∈ Finset.range (n + 1)
⊢ (↑n * X - ↑(n✝ + 1)) ^ 2 = ↑(n✝ + 1) * ↑(n✝ + 1 - 1) + (1 - 2 * ↑n * X) * ↑(n✝ + 1) + ↑n ^ 2 * X ^ 2

Tactic:
simp

Goal state after:
case calc_1.e_a.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
n✝ : ℕ
m : n✝ + 1 ∈ Finset.range (n + 1)
⊢ (↑n * X - (↑n✝ + 1)) ^ 2 = (↑n✝ + 1) * ↑n✝ + (1 - 2 * ↑n * X) * (↑n✝ + 1) + ↑n ^ 2 * X ^ 2
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : TopologicalSpace A
inst✝³ : T2Space A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra 𝕜 A
s : Set 𝕜
x✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) = ψ (ContinuousMap.restrict s (ContinuousMap.id 𝕜))
a✝ : ↑s
⊢ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) a✝ = (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case calc_2.zero
R : Type u_1
inst✝ : CommRing R
p :
  ∑ x ∈ Finset.range (0 + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * 0) * X) * ↑x + ↑(0 ^ 2) * X ^ 2) * bernsteinPolynomial R 0 x =
    ↑(0 * (0 - 1)) * X ^ 2 + (1 - (2 * 0) • X) * 0 • X + 0 ^ 2 • X ^ 2 * 1
⊢ ↑0 * ↑(0 - 1) * X ^ 2 + (1 - 2 * ↑0 * X) * (↑0 * X) + ↑0 ^ 2 * X ^ 2 * 1 = ↑0 * X * (1 - X)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case calc_2.succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
p :
  ∑ x ∈ Finset.range (n✝ + 1 + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * (n✝ + 1)) * X) * ↑x + ↑((n✝ + 1) ^ 2) * X ^ 2) * bernsteinPolynomial R (n✝ + 1) x =
    ↑((n✝ + 1) * (n✝ + 1 - 1)) * X ^ 2 + (1 - (2 * (n✝ + 1)) • X) * (n✝ + 1) • X + (n✝ + 1) ^ 2 • X ^ 2 * 1
⊢ ↑(n✝ + 1) * ↑(n✝ + 1 - 1) * X ^ 2 + (1 - 2 * ↑(n✝ + 1) * X) * (↑(n✝ + 1) * X) + ↑(n✝ + 1) ^ 2 * X ^ 2 * 1 =
    ↑(n✝ + 1) * X * (1 - X)

Tactic:
simp

Goal state after:
case calc_2.succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
p :
  ∑ x ∈ Finset.range (n✝ + 1 + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * (n✝ + 1)) * X) * ↑x + ↑((n✝ + 1) ^ 2) * X ^ 2) * bernsteinPolynomial R (n✝ + 1) x =
    ↑((n✝ + 1) * (n✝ + 1 - 1)) * X ^ 2 + (1 - (2 * (n✝ + 1)) • X) * (n✝ + 1) • X + (n✝ + 1) ^ 2 • X ^ 2 * 1
⊢ (↑n✝ + 1) * ↑n✝ * X ^ 2 + (1 - 2 * (↑n✝ + 1) * X) * ((↑n✝ + 1) * X) + (↑n✝ + 1) ^ 2 * X ^ 2 = (↑n✝ + 1) * X * (1 - X)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
a✝ : X
⊢ ↑(((algebraMap ℝ C(X, ℝ)) ↑r).toNNReal a✝) = ↑(((algebraMap ℝ≥0 C(X, ℝ≥0)) r) a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
r : ℝ≥0
a✝ : X
⊢ ↑((-(algebraMap ℝ C(X, ℝ)) ↑r).toNNReal a✝) = ↑(0 a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
⊢ φ (ContinuousMap.toNNReal 1) - φ (-1).toNNReal = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁵ : TopologicalSpace X
A : Type u_2
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
⊢ φ (ContinuousMap.toNNReal 0) - φ (-0).toNNReal = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case e'_5.e_6
X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
f : C(X, ℝ≥0)
x : X
⊢ ↑(({ toFun := toReal, continuous_toFun := continuous_coe }.comp f).toNNReal x) = ↑(f x)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case e'_6.e_6
X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
f : C(X, ℝ≥0)
x : X
⊢ ↑((-{ toFun := toReal, continuous_toFun := continuous_coe }.comp f).toNNReal x) = ↑(0 x)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
A : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
φ ψ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝²] ⇑φ
hψ : Continuous[_, inst✝²] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) = ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this :
  ∀ (ξ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A),
    Continuous[_, inst✝²] ⇑ξ →
      let ξ' := ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e);
      Continuous[_, inst✝²] ⇑ξ' ∧
        ξ' (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) = ξ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hφ' : Continuous[_, inst✝²] ⇑(φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
hφ_id :
  (φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
      (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) =
    φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hψ' : Continuous[_, inst✝²] ⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
hψ_id :
  (ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
      (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) =
    ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hs' : CompactSpace ↑s'
h' :
  φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e) =
    ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e)
h'' :
  (φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e)).comp
      (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e.symm) =
    (ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e)).comp
      (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e.symm)
x✝ : C(↑s, ℝ)
⊢ ((ContinuousMap.compStarAlgHom' ℝ ℝ ↑e).comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e.symm)) x✝ =
    (StarAlgHom.id ℝ C(↑s, ℝ)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
x : A
⊢ ‖1 x‖ ≤ 1 * ‖x‖

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
f : C(X, ℝ)₀
⊢ (ContinuousMap.realToNNReal.comp ↑f) 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
⊢ f ∈ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
⊢ φ (toNNReal 0) - φ (-0).toNNReal = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case right
X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := ⋯
AK : Subalgebra ℝ C(↑K, ℝ) := ⋯
x y : ↑K
hxy : x ≠ y
w✝ : X → ℝ
hg_sep : w✝ ↑x ≠ w✝ ↑y
g : C(X, ℝ)
hg1 : g ∈ ↑A
hg2 : (fun f ↦ ⇑f) g = w✝
⊢ ↑restrict_on_K g = restrict_on_K g

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case right
X : Type u_2
inst✝ : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(↑K, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
hsep : AK.SeparatesPoints
gK : C(↑K, ℝ)
hgKAK✝ : gK ∈ AK
hgapprox : ∀ (x : ↑K), ‖↑⟨gK, hgKAK✝⟩ x - K.domRestrict (⇑f) x‖ < ε
g : C(X, ℝ)
hgA : g ∈ A
hgKAK : ↑restrict_on_K g = gK
x : X
hxK : x ∈ K
eqg : g x = gK ⟨x, hxK⟩
⊢ ‖gK ⟨x, hxK⟩ - f x‖ < ε

Tactic:
exact hgapprox ⟨x, hxK⟩

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case e'_5.e_6
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f : C(X, ℝ≥0)₀
x : X
⊢ ↑(({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal x) = ↑(f x)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case e'_6.e_6
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : Zero X
A : Type u_2
inst✝² : NonUnitalRing A
inst✝¹ : StarRing A
inst✝ : Module ℝ A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f : C(X, ℝ≥0)₀
x : X
⊢ ↑((-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal x) = ↑(0 x)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NonUnitalNormedRing A
inst✝ : NormedSpace 𝕜 A
x : WithLp 1 (Unitization 𝕜 A)
⊢ 0 < ENNReal.toReal 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.UnitizationL1

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NonUnitalNormedRing A
inst✝ : NormedSpace 𝕜 A
x : WithLp 1 (Unitization 𝕜 A)
⊢ (‖x.ofLp.toProd.1‖ ^ ENNReal.toReal 1 + ‖x.ofLp.toProd.2‖ ^ ENNReal.toReal 1) ^ (1 / ENNReal.toReal 1) =
    ‖x.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
⊢ (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}).topologicalClosure =
    (polynomialFunctions s).starClosure.topologicalClosure

Tactic:
polynomialFunctions.starClosure_eq_adjoin_X

Goal state after:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
⊢ (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}).topologicalClosure =
    (adjoin 𝕜 {(toContinuousMapOnAlgHom s) X}).topologicalClosure
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝ f : C(↑s, 𝕜)
hf : f ∈ (polynomialFunctions s).starClosure
⊢ p f

Tactic:
polynomialFunctions.starClosure_eq_adjoin_X

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝ f : C(↑s, 𝕜)
hf : f ∈ StarAlgebra.adjoin 𝕜 {(toContinuousMapOnAlgHom s) X}
⊢ p f
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝² x✝¹ : F
x✝ : WeakBilin B
⊢ { toLinearMap := B.flip (x✝² + x✝¹), cont := ⋯ } x✝ =
    ({ toLinearMap := B.flip x✝², cont := ⋯ } + { toLinearMap := B.flip x✝¹, cont := ⋯ }) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝² : 𝕜
x✝¹ : F
x✝ : WeakBilin B
⊢ { toLinearMap := B.flip (x✝² • x✝¹), cont := ⋯ } x✝ =
    ((RingHom.id 𝕜) x✝² • { toLinearMap := B.flip x✝¹, cont := ⋯ }) x✝

Tactic:
simp

Goal state after: