mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
r : ℝ
⊢ cfc (fun x ↦ x⁻) ((algebraMap ℝ A) r) = (algebraMap ℝ A) r⁻

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
r : ℝ≥0
⊢ cfc (fun x ↦ x⁺) ((algebraMap ℝ A) ((algebraMap ℝ≥0 ℝ) r)) = (algebraMap ℝ A) ((algebraMap ℝ≥0 ℝ) r)

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : -(star c * c) = a⁻ ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x ↦ ContinuousMap.realToNNReal x
⊢ 0 ≤ ↑2

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
b : A
a : A := star b * b
a_def : a = star b * b
ha : IsSelfAdjoint a
c : A := b * a⁻
h_eq_negPart_a : 0 = cfcₙ (fun x ↦ x⁻) a ^ 3
h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x ↦ ContinuousMap.realToNNReal x
h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal
⊢ 0⁻ = 0

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
a✝ : Nontrivial A
⊢ ∀ x ∈ spectrum ℝ 0, 0 ≤ x

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a✝ : Nontrivial A
⊢ ∀ x ∈ spectrum ℝ ↑0, 0 ≤ x

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ 0 < 1 / 2

Tactic:
simp

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

Goal state before:
pp: case mpr.mem
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p s : A
⊢ SpectrumRestricts ↑((fun s ↦ star s * s) s) ⇑ContinuousMap.realToNNReal

Tactic:
SpectrumRestricts.nnreal_iff,

Goal state after:
case mpr.mem
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p s : A
⊢ ∀ x ∈ spectrum ℝ ↑((fun s ↦ star s * s) s), 0 ≤ x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: case mpr.zero
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
x p : A
⊢ IsSelfAdjoint 0 ∧ ∀ x ∈ spectrum ℝ ↑0, 0 ≤ x

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : a ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
x✝ : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this✝ : StarOrderedRing (Unitization ℂ A)
this :
  (Unitization.inrNonUnitalStarAlgHom ℂ A) a ∈
    AddSubmonoid.closure (Set.range (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) ∘ fun s ↦ star s * s))
s : A
⊢ (fun s ↦ star s * s) ↑s = (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) ∘ fun s ↦ star s * s) s

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: case inl.inl
A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ (a ^ 0) ^ 0 = a ^ (0 * 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: case inl.inr
A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
y : ℝ≥0
ha : 0 ≤ a
hy : 0 < y
⊢ (a ^ 0) ^ y = a ^ (0 * y)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: case inr.inl
A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : 0 ≤ a
hx : 0 < x
⊢ (a ^ x) ^ 0 = a ^ (x * 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: case inr.inr
A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ≥0
ha : 0 ≤ a
hx : 0 < x
hy : 0 < y
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
simp

Goal state after:
case inr.inr
A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ≥0
ha : 0 ≤ a
hx : 0 < x
hy : 0 < y
⊢ (a ^ x) ^ y = a ^ (x * y)
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: case h.left.«0».left
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ 0 ≤ ![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

Goal state after:
case h.left.«0».left
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ 0 ≤ (↑(realPart a))⁺
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: case h.left.«1».left
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ 0 ≤ ![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

Goal state after:
case h.left.«1».left
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ 0 ≤ (↑(imaginaryPart a))⁺
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: case h.left.«2».left
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ 0 ≤ ![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
simp

Goal state after:
case h.left.«2».left
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ 0 ≤ (↑(realPart a))⁻
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: case h.left.«3».left
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ 0 ≤ ![(↑(realPart a))⁺, (↑(imaginaryPart a))⁺, (↑(realPart a))⁻, (↑(imaginaryPart a))⁻] ((fun i ↦ i) ⟨3, ⋯⟩)

Tactic:
simp

Goal state after:
case h.left.«3».left
A : Type u_2
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ 0 ≤ (↑(imaginaryPart a))⁻
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case inl
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring 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
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f ⊥ (spectrum R a)
hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (spectrum R a)
⊢ Tendsto (fun x ↦ cfc (F x) a) ⊥ (𝓝 (cfc f a))

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: case e_f
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
n : ℕ
ha : 0 ≤ a
⊢ (fun x ↦ x ^ ↑n) = fun x ↦ x ^ n

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ a ^ 1 = a

Tactic:
rpow_one a ha.nonneg

Goal state after:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ a = a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{spectrum R a}] R
⊢ f ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)} →
    ∀ ⦃y : R →ᵤ[{spectrum R a}] R⦄,
      y ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)} →
        edist ((fun f ↦ cfc ((toFun {spectrum R a}) f) a) f) ((fun f ↦ cfc ((toFun {spectrum R a}) f) a) y) ≤
          ↑1 * edist f y

Tactic:
hf

Goal state after:
case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{spectrum R a}] R
hf : f ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
⊢ ∀ ⦃y : R →ᵤ[{spectrum R a}] R⦄,
    y ∈ {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)} →
      edist ((fun f ↦ cfc ((toFun {spectrum R a}) f) a) f) ((fun f ↦ cfc ((toFun {spectrum R a}) f) a) y) ≤
        ↑1 * edist f y
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : Aˣ
n : ℤ
ha : 0 ≤ ↑a
x✝¹ : ℝ≥0
x✝ : x✝¹ ∈ spectrum ℝ≥0 ↑a
⊢ x✝¹ ^ ↑n = x✝¹ ^ n

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
this : a ^ (1 / 2) = a ^ ↑(1 / 2)
⊢ 0 < 1 / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
h : IsUnit a
ha : 0 ≤ a
this : IsStrictlyPositive a
⊢ 2⁻¹ ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
htriv : 0 ≤ a
h₁ : 0 < x
⊢ ↑x / 2 = ↑(x / 2)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : 0 ≤ a
hx : ¬x = 0
h₁ : 0 ≤ ↑x
⊢ 0 ≤ 1 / 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ 1 / 2 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ a ^ (-x) = a ^ (x * -1)

Tactic:
simp

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

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
nontriv : Subsingleton A
⊢ a ≤ (algebraMap ℝ A) ‖a‖

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
tfae_1_iff_8 : IsStrictlyPositive a ↔ 0 ≤ a ∧ IsUnit a
tfae_1_iff_9 : IsStrictlyPositive a ↔ IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x
tfae_1_to_2 : IsStrictlyPositive a → IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a
tfae_2_to_3 : IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a → IsUnit (sqrt a) ∧ a = sqrt a * sqrt a
tfae_3_to_4 : IsUnit (sqrt a) ∧ a = sqrt a * sqrt a → ∃ b, IsStrictlyPositive b ∧ a = b * b
⊢ [IsStrictlyPositive a, IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a, IsUnit (sqrt a) ∧ a = sqrt a * sqrt a,
      ∃ b, IsStrictlyPositive b ∧ a = b * b, ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b,
      ∃ b, IsUnit b ∧ a = star b * b, ∃ b, IsUnit b ∧ a = b * star b, 0 ≤ a ∧ IsUnit a,
      IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x].TFAE

Tactic:
tfae_have 4 → 5 := fun ⟨b, hb, hab⟩ => ⟨b, hb.isUnit, hb.isSelfAdjoint, hab⟩

Goal state after:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
tfae_1_iff_8 : IsStrictlyPositive a ↔ 0 ≤ a ∧ IsUnit a
tfae_1_iff_9 : IsStrictlyPositive a ↔ IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x
tfae_1_to_2 : IsStrictlyPositive a → IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a
tfae_2_to_3 : IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a → IsUnit (sqrt a) ∧ a = sqrt a * sqrt a
tfae_3_to_4 : IsUnit (sqrt a) ∧ a = sqrt a * sqrt a → ∃ b, IsStrictlyPositive b ∧ a = b * b
tfae_4_to_5 : (∃ b, IsStrictlyPositive b ∧ a = b * b) → ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b
⊢ [IsStrictlyPositive a, IsStrictlyPositive (sqrt a) ∧ a = sqrt a * sqrt a, IsUnit (sqrt a) ∧ a = sqrt a * sqrt a,
      ∃ b, IsStrictlyPositive b ∧ a = b * b, ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b,
      ∃ b, IsUnit b ∧ a = star b * b, ∃ b, IsUnit b ∧ a = b * star b, 0 ≤ a ∧ IsUnit a,
      IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x].TFAE
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ -1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1 ↔ ‖sqrt a * ↑b ^ (-1 * (1 / 2))‖ ≤ 1

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul A E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
a : A
x y : E
⊢ ⟪a •> x, y⟫ = ⟪x, y⟫ * star a

Tactic:
← star_inner

Goal state after:
A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul A E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
a : A
x y : E
⊢ star ⟪y, a •> x⟫ = ⟪x, y⟫ * star a
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul A E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
a : A
x y : E
⊢ star ⟪y, a •> x⟫ = ⟪x, y⟫ * star a

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℂ
x y : E
⊢ ⟪z •> x, y⟫ = star z •> ⟪x, y⟫

Tactic:
← star_inner

Goal state after:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℂ
x y : E
⊢ star ⟪y, z •> x⟫ = star z •> ⟪x, y⟫
Module: Mathlib.Analysis.CStarAlgebra.Module.Defs

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℂ
x y : E
⊢ star ⟪y, z •> x⟫ = star z •> ⟪x, y⟫

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
⊢ z •> x = ↑z •> x

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> x = ↑z •> x
⊢ star (↑z •> ⟪y, x⟫) = z •> ⟪x, y⟫

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
⊢ z •> y = ↑z •> y

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z : ℝ
x y : E
h₁ : z •> y = ↑z •> y
⊢ star (star ↑z •> ⟪y, x⟫) = z •> ⟪x, y⟫

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
x z y : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
x : E
z : ℂ
y : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul A E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
z y x✝ : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

Goal state after: