awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
rw : ‖a ^ (1 / 2)‖₊ = ‖a‖₊ ^ (1 / 2)
⊢ ‖sqrt a‖₊ = (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) ‖a‖₊

Tactic:
rw [sqrt_eq_nnrpow, NNReal.sqrt_eq_rpow]

Premises used: NNReal.sqrt_eq_rpow, CFC.sqrt_eq_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ 0 < 1 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ ‖a ^ (1 / 2)‖₊ = ‖a‖₊ ^ (1 / 2)

Tactic:
exact nnnorm_nnrpow a (by simp) ha

Premises used: CFC.nnnorm_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ ‖sqrt a‖ = √‖a‖

Tactic:
simpa using congr(NNReal.toReal $(nnnorm_sqrt a ha))
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : ContinuousStar A
inst_10 : CompleteSpace A
⊢ ContinuousOn sqrt {a : A | 0 ≤ a}

Tactic:
continuousOn_id.cfcₙ_nnreal_of_mem_nhdsSet _ Filter.univ_mem

Premises used: CFC.sqrt, ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet, continuousOn_id, Filter.univ_mem
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : ContinuousStar A
inst_10 : CompleteSpace A
r : ℝ≥0
inl : ContinuousOn (Y := A) (fun (x : A) ↦ HPow.hPow (β := ℝ≥0) x 0) {a : A | 0 ≤ a}
inr : ∀ (hr : 0 < r), ContinuousOn (Y := A) (fun (x : A) ↦ x ^ r) {a : A | 0 ≤ a}
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ x ^ r) {a : A | 0 ≤ a}

Tactic:
obtain (rfl | hr) := eq_zero_or_pos r

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : ContinuousStar A
inst_10 : CompleteSpace A
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ HPow.hPow (β := ℝ≥0) x 0) {a : A | 0 ≤ a}

Tactic:
simpa using continuousOn_const

Premises used: continuousOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : ContinuousStar A
inst_10 : CompleteSpace A
r : ℝ≥0
hr : 0 < r
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ x ^ r) {a : A | 0 ≤ a}

Tactic:
continuousOn_id.cfcₙ_nnreal_of_mem_nhdsSet _ Filter.univ_mem

Premises used: ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet, CFC.nnrpow, continuousOn_id, Filter.univ_mem
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : ContinuousStar A
inst_10 : CompleteSpace A
r : ℝ≥0
hr : 0 < r
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ x ^ r) {a : A | 0 ≤ a}

Tactic:
exact continuousOn_id.cfcₙ_nnreal_of_mem_nhdsSet _ Filter.univ_mem

Premises used: ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet, continuousOn_id, Filter.univ_mem
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : NonnegSpectrumClass ℝ A
inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
r : ℝ
hr : 0 < r
ha : 0 ≤ a
⊢ 0 ≤ r

Tactic:
hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : NonnegSpectrumClass ℝ A
inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
r : ℝ
hr : 0 < r
ha : 0 ≤ a
lift : ∀ (r : ℝ≥0) (hr : 0 < (↑r : ℝ)), ‖a ^ (↑r : ℝ)‖₊ = ‖a‖₊ ^ (↑r : ℝ)
⊢ ‖a ^ r‖₊ = ‖a‖₊ ^ r

Tactic:
lift r to ℝ≥0 using hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : NonnegSpectrumClass ℝ A
inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
r : ℝ≥0
hr : 0 < (↑r : ℝ)
rw rw₁ : 0 < r
⊢ ‖a ^ (↑r : ℝ)‖₊ = ‖a‖₊ ^ (↑r : ℝ)

Tactic:
rw [← nnrpow_eq_rpow, ← nnnorm_nnrpow a]

Premises used: CFC.nnrpow_eq_rpow, CFC.nnnorm_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : NonnegSpectrumClass ℝ A
inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
r : ℝ≥0
hr : 0 < (↑r : ℝ)
⊢ 0 < r

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : NonnegSpectrumClass ℝ A
inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
r : ℝ
hr : 0 < r
ha : 0 ≤ a
⊢ ‖a ^ r‖ = ‖a‖ ^ r

Tactic:
congr(NNReal.toReal $(nnnorm_rpow a hr ha))

Premises used: congrArg, id, CFC.nnnorm_rpow, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : NonnegSpectrumClass ℝ A
inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : ContinuousStar A
inst_8 : CompleteSpace A
r : ℝ
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ x ^ r) {a : A | IsStrictlyPositive a}

Tactic:
continuousOn_id.cfc_nnreal_of_mem_nhdsSet _ (s := {0}ᶜ) ?_

Premises used: ContinuousOn.cfc_nnreal_of_mem_nhdsSet, continuousOn_id, CFC.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : NonnegSpectrumClass ℝ A
inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : ContinuousStar A
inst_8 : CompleteSpace A
r : ℝ
refine :
  Membership.mem (γ := Filter ℝ≥0)
    (nhdsSet (⋃ (x : A), ⋃ (_ : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} x), spectrum ℝ≥0 (id x)))
    {0}ᶜ
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ x ^ r) {a : A | IsStrictlyPositive a}

Tactic:
refine continuousOn_id.cfc_nnreal_of_mem_nhdsSet _ (s := {0}ᶜ) ?_

Premises used: ContinuousOn.cfc_nnreal_of_mem_nhdsSet, continuousOn_id
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : NonnegSpectrumClass ℝ A
inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : ContinuousStar A
inst_8 : CompleteSpace A
r : ℝ
simp_rw : ∀ (i : A) (i_1 : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} i), spectrum ℝ≥0 (id i) ⊆ {0}ᶜ
⊢ Membership.mem (γ := Filter ℝ≥0)
    (nhdsSet (⋃ (x : A), ⋃ (_ : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} x), spectrum ℝ≥0 (id x)))
    {0}ᶜ

Tactic:
simp_rw [nhdsSet_iUnion, Filter.mem_iSup, isOpen_compl_singleton.mem_nhdsSet]

Premises used: nhdsSet_iUnion, Filter.mem_iSup, isOpen_compl_singleton, IsOpen.mem_nhdsSet
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : NonnegSpectrumClass ℝ A
inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : ContinuousStar A
inst_8 : CompleteSpace A
r : ℝ
a : A
ha : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} a
⊢ spectrum ℝ≥0 (id a) ⊆ {0}ᶜ

Tactic:
simpa using spectrum.zero_notMem _ ha.isUnit

Premises used: spectrum.zero_notMem, IsStrictlyPositive.isUnit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : StarRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : PartialOrder A
inst_4 : StarOrderedRing A
inst_5 : NonnegSpectrumClass ℝ A
inst_6 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : ContinuousStar A
inst_8 : CompleteSpace A
r : ℝ
⊢ ∀ (i : A) (i_1 : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} i), spectrum ℝ≥0 (id i) ⊆ {0}ᶜ

Tactic:
exact fun a ha ↦ by simpa using spectrum.zero_notMem _ ha.isUnit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : CStarRing A
inst_4 : NormedSpace ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
rw : ‖star b * a * b‖ = ‖sqrt a * b‖ * ‖sqrt a * b‖
rw₁ : ‖star b * a * b‖ = ‖star (sqrt a * b) * (sqrt a * b)‖
rw₂ : ‖star b * a * b‖ = ‖star b * star (sqrt a) * (sqrt a * b)‖
rw₃ : ‖star b * a * b‖ = ‖star b * sqrt a * (sqrt a * b)‖
rw₄ : ‖star b * a * b‖ = ‖star b * sqrt a * sqrt a * b‖
rw₅ : ‖star b * a * b‖ = ‖star b * (sqrt a * sqrt a) * b‖
rw₆ rw₇ : ‖star b * a * b‖ = ‖star b * a * b‖
⊢ ‖star b * a * b‖ = HPow.hPow (β := ℕ) ‖sqrt a * b‖ 2

Tactic:
rw [sq, ← CStarRing.norm_star_mul_self, star_mul, (CFC.sqrt_nonneg a).star_eq,
    ← mul_assoc _ (CFC.sqrt a), mul_assoc _ _ (CFC.sqrt a), CFC.sqrt_mul_sqrt_self a]

Premises used: LE.le.star_eq, CFC.sqrt, mul_assoc, sq, CStarRing.norm_star_mul_self, StarMul.star_mul, CFC.sqrt_nonneg, CFC.sqrt_mul_sqrt_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : CStarRing A
inst_4 : NormedSpace ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
hb : IsSelfAdjoint b
ha : 0 ≤ a
⊢ ‖b * a * b‖ = HPow.hPow (β := ℕ) ‖sqrt a * b‖ 2

Tactic:
simpa [hb.star_eq] using norm_star_mul_mul_self_of_nonneg b ha

Premises used: CFC.norm_star_mul_mul_self_of_nonneg, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : CStarRing A
inst_4 : NormedSpace ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
rw : ‖b * a * star b‖
| HPow.hPow (β := ℕ) ‖b * sqrt a‖ 2

Tactic:
rw [← (CFC.sqrt_nonneg a).star_eq, ← star_star b, ← star_mul, norm_star,
    ← norm_star_mul_mul_self_of_nonneg _ ha, star_star]

Premises used: norm_star, LE.le.star_eq, star_star, CFC.norm_star_mul_mul_self_of_nonneg, StarMul.star_mul, CFC.sqrt_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : CStarRing A
inst_4 : NormedSpace ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
ha : 0 ≤ a
conv_rhs : ‖b * a * star b‖ = HPow.hPow (β := ℕ) ‖b * sqrt a‖ 2
conv_rhs₁ : ‖b * a * star b‖ = ‖b * a * star b‖
⊢ ‖b * a * star b‖ = HPow.hPow (β := ℕ) ‖b * sqrt a‖ 2

Tactic:
conv_rhs => rw [← (CFC.sqrt_nonneg a).star_eq, ← star_star b, ← star_mul, norm_star,
    ← norm_star_mul_mul_self_of_nonneg _ ha, star_star]

Premises used: norm_star, LE.le.star_eq, star_star, CFC.norm_star_mul_mul_self_of_nonneg, StarMul.star_mul, CFC.sqrt_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : CStarRing A
inst_4 : NormedSpace ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a b : A
hb : IsSelfAdjoint b
ha : 0 ≤ a
⊢ ‖b * a * b‖ = HPow.hPow (β := ℕ) ‖b * sqrt a‖ 2

Tactic:
simpa [hb.star_eq] using norm_mul_mul_star_self_of_nonneg b ha

Premises used: CFC.norm_mul_mul_star_self_of_nonneg, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
obtain :
  ∀ (μ : Measure ℝ)
    (hμ :
      ∀ (a : A),
        Membership.mem (γ := Set A) (Ici 0) a →
          IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a)
              (Ioi 0) μ ∧
            a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ),
    MonotoneOn (β := A) (fun (a : A) ↦ a ^ p) (Ici 0)
⊢ MonotoneOn (β := A) (fun (a : A) ↦ a ^ p) (Ici 0)

Tactic:
obtain ⟨μ, hμ⟩ := CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁ A hp

Premises used: CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
⊢ EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)

Tactic:
have h₃' : (Ici 0).EqOn (fun a : A => a ^ p)
      (fun a : A => ∫ t in Ioi 0, cfcₙ (rpowIntegrand₀₁ p t) a ∂μ) :=
    fun a ha => (hμ a ha).2
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ MonotoneOn (β := A) (fun (a : A) ↦ a ^ p) (Ici 0)

Tactic:
MonotoneOn.congr ?_ h₃'.symm

Premises used: MonotoneOn.congr, Set.EqOn.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
refine :
  MonotoneOn (β := A) (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ)
    (Ici 0)
⊢ MonotoneOn (β := A) (fun (a : A) ↦ a ^ p) (Ici 0)

Tactic:
refine MonotoneOn.congr ?_ h₃'.symm

Premises used: MonotoneOn.congr, Set.EqOn.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
⊢ MonotoneOn (β := A) (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ)
    (Ici 0)

Tactic:
integral_monotoneOn_of_integrand_ae ?_ fun a ha => (hμ a ha).1

Premises used: And.left, MeasureTheory.integral_monotoneOn_of_integrand_ae
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
refine : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), MonotoneOn (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ x)) (Ici 0)
⊢ MonotoneOn (β := A) (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ)
    (Ici 0)

Tactic:
refine integral_monotoneOn_of_integrand_ae ?_ fun a ha => (hμ a ha).1

Premises used: And.left, MeasureTheory.integral_monotoneOn_of_integrand_ae
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
h :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    MonotoneOn (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t)) (Ici 0)
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), MonotoneOn (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ x)) (Ici 0)

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ MonotoneOn (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t)) (Ici 0)

Tactic:
monotoneOn_cfcₙ_rpowIntegrand₀₁ hp ht

Premises used: CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) p
μ : Measure ℝ
hμ :
  ∀ (a : A),
    Membership.mem (γ := Set A) (Ici 0) a →
      IntegrableOn.{0, u_1} (ε := A) (fun (t : ℝ) ↦ cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a) (Ioi 0)
          μ ∧
        a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ
h₃' :
  EqOn (β := A) (fun (a : A) ↦ a ^ p)
    (fun (a : A) ↦ ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t) a ∂μ) (Ici 0)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ MonotoneOn (cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₀₁ t)) (Ici 0)

Tactic:
exact monotoneOn_cfcₙ_rpowIntegrand₀₁ hp ht

Premises used: CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Icc 0 1) p
a b : A
hab : a ≤ b
pos : ∀ (ha : 0 ≤ a), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
neg : ∀ (ha : ¬0 ≤ a), LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)
⊢ LE.le.{u_1} (α := A) ((fun (a : A) ↦ a ^ p) a) ((fun (a : A) ↦ a ^ p) b)

Tactic:
by_cases ha : 0 ≤ a