mathlib-initiative/mathlib-tactics huggingface dataset:
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:
·

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 - 1) + (1 - 2 * ↑n * X) * ↑(n✝ + 1) + ↑n ^ 2 * X ^ 2
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case calc_2
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 * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1 = n • X * (1 - X)

Tactic:
·

Goal state after:
case calc_2
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 * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1 = n • X * (1 - X)
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)

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:
·

Goal state after:
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)
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:
·

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✝ + 1 - 1) * X ^ 2 + (1 - 2 * ↑(n✝ + 1) * X) * (↑(n✝ + 1) * X) + ↑(n✝ + 1) ^ 2 * X ^ 2 * 1 =
    ↑(n✝ + 1) * X * (1 - X)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
⊢ (f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal =
    (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal

Tactic:
by
  ext x
  simp [max_neg_zero, add_mul, mul_add]
  abel

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

Goal state before:
pp: case inl
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
r : ℝ
hr : 0 ≤ r
⊢ φ ((algebraMap ℝ C(X, ℝ)) r).toNNReal - φ (-(algebraMap ℝ C(X, ℝ)) r).toNNReal = (algebraMap ℝ A) r

pp: case inr
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
r : ℝ
hr : r ≤ 0
⊢ φ ((algebraMap ℝ C(X, ℝ)) r).toNNReal - φ (-(algebraMap ℝ C(X, ℝ)) r).toNNReal = (algebraMap ℝ A) r

Tactic:
·

Goal state after:
case inl
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
r : ℝ
hr : 0 ≤ r
⊢ φ ((algebraMap ℝ C(X, ℝ)) r).toNNReal - φ (-(algebraMap ℝ C(X, ℝ)) r).toNNReal = (algebraMap ℝ A) r
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case inr
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
r : ℝ
hr : r ≤ 0
⊢ φ ((algebraMap ℝ C(X, ℝ)) r).toNNReal - φ (-(algebraMap ℝ C(X, ℝ)) r).toNNReal = (algebraMap ℝ A) r

Tactic:
·

Goal state after:
case inr
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
r : ℝ
hr : r ≤ 0
⊢ φ ((algebraMap ℝ C(X, ℝ)) r).toNNReal - φ (-(algebraMap ℝ C(X, ℝ)) r).toNNReal = (algebraMap ℝ A) r
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
x : X
⊢ IsOpen[inst✝¹] (W x)

pp: case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
x : X
⊢ x ∈ W x

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
x : X
⊢ IsOpen[inst✝¹] (W x)
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
x : X
⊢ x ∈ W x

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun x ↦ ⋯.choose
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ :=
  fun x ↦ Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhds_y x))
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := fun x ↦ ⟨(ys x).sup' ⋯ fun y ↦ g x y, ⋯⟩
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := fun x ↦ {z | ↑(h x) z < f z + ε}
x : X
⊢ x ∈ W x
Module: Mathlib.Analysis.Normed.Algebra.Unitization

Goal state before:
pp: case refine_1
𝕜 : 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 : Unitization 𝕜 A
⊢ ‖((addEquiv 𝕜 A) x).1‖ ≤ 2 * max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖

pp: case refine_2
𝕜 : 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 : Unitization 𝕜 A
⊢ ‖((addEquiv 𝕜 A) x).2‖ ≤ 2 * max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖

Tactic:
·

Goal state after:
case refine_1
𝕜 : 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 : Unitization 𝕜 A
⊢ ‖((addEquiv 𝕜 A) x).1‖ ≤ 2 * max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖
Module: Mathlib.Analysis.Normed.Algebra.Unitization

Goal state before:
pp: case refine_2
𝕜 : 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 : Unitization 𝕜 A
⊢ ‖((addEquiv 𝕜 A) x).2‖ ≤ 2 * max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖

Tactic:
·

Goal state after:
case refine_2
𝕜 : 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 : Unitization 𝕜 A
⊢ ‖((addEquiv 𝕜 A) x).2‖ ≤ 2 * max ‖x.toProd.1‖ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖
Module: Mathlib.Analysis.Normed.Algebra.Unitization

Goal state before:
pp: case refine_1
𝕜 : 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 : Unitization 𝕜 A
⊢ ‖x.toProd.1‖ ≤ 2 * max ‖((addEquiv 𝕜 A) x).1‖ ‖((addEquiv 𝕜 A) x).2‖

pp: case refine_2
𝕜 : 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 : Unitization 𝕜 A
⊢ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖ ≤ 2 * max ‖((addEquiv 𝕜 A) x).1‖ ‖((addEquiv 𝕜 A) x).2‖

Tactic:
·

Goal state after:
case refine_1
𝕜 : 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 : Unitization 𝕜 A
⊢ ‖x.toProd.1‖ ≤ 2 * max ‖((addEquiv 𝕜 A) x).1‖ ‖((addEquiv 𝕜 A) x).2‖
Module: Mathlib.Analysis.Normed.Algebra.Unitization

Goal state before:
pp: case refine_2
𝕜 : 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 : Unitization 𝕜 A
⊢ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖ ≤ 2 * max ‖((addEquiv 𝕜 A) x).1‖ ‖((addEquiv 𝕜 A) x).2‖

Tactic:
·

Goal state after:
case refine_2
𝕜 : 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 : Unitization 𝕜 A
⊢ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.toProd.1 + (mul 𝕜 A) x.toProd.2‖ ≤ 2 * max ‖((addEquiv 𝕜 A) x).1‖ ‖((addEquiv 𝕜 A) x).2‖
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ ((fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1).Nonempty

pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ ∀ a_1 ∈ (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1, a_1 ≤ ‖a‖₊

pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r < ‖a‖₊
⊢ ∃ a_1 ∈ (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1, r < a_1

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ ((fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1).Nonempty
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ ∀ a_1 ∈ (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1, a_1 ≤ ‖a‖₊

pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r < ‖a‖₊
⊢ ∃ a_1 ∈ (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1, r < a_1

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
⊢ ∀ a_1 ∈ (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1, a_1 ≤ ‖a‖₊
Module: Mathlib.Analysis.Real.Spectrum

Goal state before:
pp: case refine_1
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ 0 ≤ x

pp: case refine_2
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal

Tactic:
·

Goal state after:
case refine_1
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ 0 ≤ x
Module: Mathlib.Analysis.Real.Spectrum

Goal state before:
pp: case refine_2
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal

Tactic:
·

Goal state after:
case refine_2
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal
Module: Mathlib.Analysis.Real.Spectrum

Goal state before:
pp: A : Type u_1
inst✝³ : NonUnitalRing A
inst✝² : Module ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
a : A
⊢ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x

Tactic:
rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
    Unitization.quasispectrum_eq_spectrum_inr' _ ℝ, SpectrumRestricts.nnreal_iff]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r < ‖a‖₊
⊢ ∃ a_1 ∈ (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1, r < a_1

Tactic:
·

Goal state after:
case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r < ‖a‖₊
⊢ ∃ a_1 ∈ (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) '' Metric.closedBall 0 1, r < a_1
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case refine_3.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ k • a⋆ ∈ Metric.closedBall 0 1

pp: case refine_3.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) (k • a⋆)

Tactic:
·

Goal state after:
case refine_3.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ k • a⋆ ∈ Metric.closedBall 0 1
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case refine_3.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) (k • a⋆)

Tactic:
·

Goal state after:
case refine_3.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DenselyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing E
inst✝⁴ : StarRing E
inst✝³ : CStarRing E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ r < (fun x ↦ ‖((mul 𝕜 E) a) x‖₊) (k • a⋆)
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case pos.left
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := ⋯
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := ⋯
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := ⋯
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := ⋯
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯
xs_w : ⋃ x ∈ xs, W x = ⊤ := ⋯
xs_nonempty : xs.Nonempty
k : ↑L := ⋯
z : X
⊢ ↑k z < f z + ε

pp: case pos.right
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := ⋯
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := ⋯
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := ⋯
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := ⋯
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯
xs_w : ⋃ x ∈ xs, W x = ⊤ := ⋯
xs_nonempty : xs.Nonempty
k : ↑L := ⋯
z : X
⊢ f z - ε < ↑k z

Tactic:
·

Goal state after:
case pos.left
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := ⋯
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := ⋯
ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → ↑L := ⋯
lt_h : ∀ (x z : X), f z - ε < ↑(h x) z
h_eq : ∀ (x : X), ↑(h x) x = f x
W : X → Set X := ⋯
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯
xs_w : ⋃ x ∈ xs, W x = ⊤ := ⋯
xs_nonempty : xs.Nonempty
k : ↑L := ⋯
z : X
⊢ ↑k z < f z + ε