awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
have ha' : ¬IsUnit (sqrt a)
Tactic: have ha' : ¬IsUnit (sqrt a) := by rwa [CFC.isUnit_sqrt_iff_isStrictlyPositive]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
have neg : ∀ (H : ¬0 ≤ a), sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
Tactic: obtain (H | H) : ¬0 ≤ a ∨ ¬IsUnit a := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
neg : ∀ (H : ¬0 ≤ a), sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
have neg₁ : ∀ (H : ¬IsUnit a), sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
Tactic: obtain (H | H) : ¬0 ≤ a ∨ ¬IsUnit a := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
have neg : sqrt a⁻¹ʳ = 0
Tactic: rw [sqrt_of_not_nonneg H, inverse_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
⊢ sqrt a⁻¹ʳ = 0
have pos : ∀ (hunit : IsUnit a), sqrt a⁻¹ʳ = 0
Tactic: by_cases hunit : IsUnit a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
pos : ∀ (hunit : IsUnit a), sqrt a⁻¹ʳ = 0
⊢ sqrt a⁻¹ʳ = 0
have neg : ∀ (hunit : ¬IsUnit a), sqrt a⁻¹ʳ = 0
Tactic: by_cases hunit : IsUnit a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
hunit : IsUnit a
⊢ sqrt a⁻¹ʳ = 0
have h₂ : ¬0 ≤ a⁻¹ʳ
Tactic: have h₂ : ¬0 ≤ inverse a := by grind [CFC.ringInverse_nonneg_iff_nonneg_of_isUnit]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : ¬IsStrictlyPositive a
ha' : ¬IsUnit (sqrt a)
H : ¬0 ≤ a
hunit : IsUnit a
h₂ : ¬0 ≤ a⁻¹ʳ
⊢ sqrt a⁻¹ʳ = 0
have pos : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [sqrt_of_not_nonneg h₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
c a b : A
hab : a ≤ b
⊢ LE.le (α := A) ((conjSqrt c : (a : A) → A) a : A) ((conjSqrt c : (a : A) → A) b : A)
have pos : ∀ (hc : 0 ≤ c), LE.le (α := A) ((conjSqrt c : (a : A) → A) a : A) ((conjSqrt c : (a : A) → A) b : A)
Tactic: by_cases hc : 0 ≤ c
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
c a b : A
hab : a ≤ b
pos : ∀ (hc : 0 ≤ c), LE.le (α := A) ((conjSqrt c : (a : A) → A) a : A) ((conjSqrt c : (a : A) → A) b : A)
⊢ LE.le (α := A) ((conjSqrt c : (a : A) → A) a : A) ((conjSqrt c : (a : A) → A) b : A)
have neg : ∀ (hc : ¬0 ≤ c), LE.le (α := A) ((conjSqrt c : (a : A) → A) a : A) ((conjSqrt c : (a : A) → A) b : A)
Tactic: by_cases hc : 0 ≤ c
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt (hypothesis)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
⊢ IsStrictlyPositive (A := A) ((conjSqrt c : (a : A) → A) a : A) ↔ IsStrictlyPositive a
have hc' : IsSelfAdjoint (sqrt c)
Tactic: have hc' : IsSelfAdjoint (sqrt c) := by cfc_tac
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
hc' : IsSelfAdjoint (sqrt c)
⊢ IsStrictlyPositive (A := A) ((conjSqrt c : (a : A) → A) a : A) ↔ IsStrictlyPositive a
have rw : IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a
Tactic: rw [conjSqrt_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
hc' : IsSelfAdjoint (sqrt c)
⊢ IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a
have pos : ∀ (ha : IsSelfAdjoint a), IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
hc' : IsSelfAdjoint (sqrt c)
pos : ∀ (ha : IsSelfAdjoint a), IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a
⊢ IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a
have neg : ∀ (ha : ¬IsSelfAdjoint a), IsStrictlyPositive (sqrt c * a * sqrt c) ↔ IsStrictlyPositive a
Tactic: by_cases ha : IsSelfAdjoint a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
⊢ Eq (α := A) (((conjSqrt c : (a : A) → A) a)⁻¹ʳ : A) ((conjSqrt c⁻¹ʳ : (a : A) → A) a⁻¹ʳ : A)
have pos : ∀ (ha : IsUnit a), Eq (α := A) (((conjSqrt c : (a : A) → A) a)⁻¹ʳ : A) ((conjSqrt c⁻¹ʳ : (a : A) → A) a⁻¹ʳ : A)
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
pos : ∀ (ha : IsUnit a), Eq (α := A) (((conjSqrt c : (a : A) → A) a)⁻¹ʳ : A) ((conjSqrt c⁻¹ʳ : (a : A) → A) a⁻¹ʳ : A)
⊢ Eq (α := A) (((conjSqrt c : (a : A) → A) a)⁻¹ʳ : A) ((conjSqrt c⁻¹ʳ : (a : A) → A) a⁻¹ʳ : A)
have neg : ∀ (ha : ¬IsUnit a), Eq (α := A) (((conjSqrt c : (a : A) → A) a)⁻¹ʳ : A) ((conjSqrt c⁻¹ʳ : (a : A) → A) a⁻¹ʳ : A)
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt (hypothesis)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c a : A
hc : IsStrictlyPositive c
ha : ¬IsUnit a
⊢ Eq (α := A) (((conjSqrt c : (a : A) → A) a)⁻¹ʳ : A) ((conjSqrt c⁻¹ʳ : (a : A) → A) a⁻¹ʳ : A)
have this : ¬IsUnit (M := A) ((conjSqrt c : (a : A) → A) a : A)
Tactic: have : ¬IsUnit (conjSqrt c a) := by grind [conjSqrt_apply, IsUnit.mul_left_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c : A
hc : 0 ≤ c
⊢ (conjSqrt c : (a : A) → A) 1 = c
have rw : sqrt c * 1 * sqrt c = c
Tactic: rw [conjSqrt_apply, mul_one, sqrt_mul_sqrt_self _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c : A
hc : 0 ≤ c
rw : sqrt c * 1 * sqrt c = c
⊢ (conjSqrt c : (a : A) → A) 1 = c
have rw₁ : sqrt c * sqrt c = c
Tactic: rw [conjSqrt_apply, mul_one, sqrt_mul_sqrt_self _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : TopologicalSpace A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : SeparatelyContinuousMul A
inst_9 : IsSemitopologicalRing A
inst_10 : T2Space A
c : A
hc : 0 ≤ c
rw : sqrt c * 1 * sqrt c = c
rw₁ : sqrt c * sqrt c = c
⊢ (conjSqrt c : (a : A) → A) 1 = c
have rw₂ : c = c
Tactic: rw [conjSqrt_apply, mul_one, sqrt_mul_sqrt_self _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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‖₊ = (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) ‖a‖₊
have rw : ‖a ^ (1 / 2)‖₊ = ‖a‖₊ ^ (1 / 2)
Tactic: rw [sqrt_eq_nnrpow, NNReal.sqrt_eq_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ x ^ r) {a : A | 0 ≤ a}
have inl : ContinuousOn (Y := A) (fun (x : A) ↦ HPow.hPow (β := ℝ≥0) x 0) {a : A | 0 ≤ a}
Tactic: obtain (rfl | hr) := eq_zero_or_pos r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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}
⊢ ContinuousOn (Y := A) (fun (x : A) ↦ x ^ r) {a : A | 0 ≤ a}
have inr : ∀ (hr : 0 < r), ContinuousOn (Y := A) (fun (x : A) ↦ x ^ r) {a : A | 0 ≤ a}
Tactic: obtain (rfl | hr) := eq_zero_or_pos r
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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
have lift : ∀ (r : ℝ≥0) (hr : 0 < (↑r : ℝ)), ‖a ^ (↑r : ℝ)‖₊ = ‖a‖₊ ^ (↑r : ℝ)
Tactic: lift r to ℝ≥0 using hr.le
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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 : ℝ)
⊢ ‖a ^ (↑r : ℝ)‖₊ = ‖a‖₊ ^ (↑r : ℝ)
have rw : 0 < r
Tactic: rw [← nnrpow_eq_rpow, ← nnnorm_nnrpow a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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}
have refine : Membership.mem (γ := Filter ℝ≥0)
  (nhdsSet (⋃ (x : A), ⋃ (_ : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} x), spectrum ℝ≥0 (id x))) {0}ᶜ
Tactic: refine continuousOn_id.cfc_nnreal_of_mem_nhdsSet _ (s := {0}ᶜ) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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 : ℝ
⊢ Membership.mem (γ := Filter ℝ≥0)
    (nhdsSet (⋃ (x : A), ⋃ (_ : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} x), spectrum ℝ≥0 (id x)))
    {0}ᶜ
have simp_rw : ∀ (i : A) (i_1 : Membership.mem (γ := Set A) {a : A | IsStrictlyPositive a} i), spectrum ℝ≥0 (id i) ⊆ {0}ᶜ
Tactic: simp_rw [nhdsSet_iUnion, Filter.mem_iSup, isOpen_compl_singleton.mem_nhdsSet]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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
⊢ ‖star b * a * b‖ = HPow.hPow (β := ℕ) ‖sqrt a * b‖ 2
have rw : ‖star b * a * b‖ = ‖sqrt a * b‖ * ‖sqrt a * b‖
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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‖
⊢ ‖star b * a * b‖ = HPow.hPow (β := ℕ) ‖sqrt a * b‖ 2
have rw₁ : ‖star b * a * b‖ = ‖star (sqrt a * b) * (sqrt a * b)‖
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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)‖
⊢ ‖star b * a * b‖ = HPow.hPow (β := ℕ) ‖sqrt a * b‖ 2
have rw₂ : ‖star b * a * b‖ = ‖star b * star (sqrt a) * (sqrt a * b)‖
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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)‖
⊢ ‖star b * a * b‖ = HPow.hPow (β := ℕ) ‖sqrt a * b‖ 2
have rw₃ : ‖star b * a * b‖ = ‖star b * sqrt a * (sqrt a * b)‖
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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)‖
⊢ ‖star b * a * b‖ = HPow.hPow (β := ℕ) ‖sqrt a * b‖ 2
have rw₄ : ‖star b * a * b‖ = ‖star b * sqrt a * sqrt a * b‖
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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‖
⊢ ‖star b * a * b‖ = HPow.hPow (β := ℕ) ‖sqrt a * b‖ 2
have rw₅ : ‖star b * a * b‖ = ‖star b * (sqrt a * sqrt a) * b‖
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric (goal)
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‖
⊢ ‖star b * a * b‖ = HPow.hPow (β := ℕ) ‖sqrt a * b‖ 2
have rw₆ : ‖star b * a * b‖ = ‖star b * a * b‖
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]