awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ‖a⁺‖ ≤ ‖a‖
have pos : ∀ (x : ℝ) (hx : x ∈ quasispectrum ℝ a), ‖x⁺‖ ≤ ‖a‖
Tactic: refine norm_cfcₙ_le fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
⊢ ‖x⁺‖ ≤ ‖a‖
have pos : ∀ (h : x ≤ 0), ‖x⁺‖ ≤ ‖a‖
Tactic: obtain (h | h) := le_or_gt x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
pos : ∀ (h : x ≤ 0), ‖x⁺‖ ≤ ‖a‖
⊢ ‖x⁺‖ ≤ ‖a‖
have pos₁ : ∀ (h : 0 < x), ‖x⁺‖ ≤ ‖a‖
Tactic: obtain (h | h) := le_or_gt x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
h : 0 < x
⊢ ‖x⁺‖ ≤ ‖a‖
have pos : ‖x‖ ≤ ‖a‖
Tactic: simp only [posPart_def, max_eq_left h.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ‖a‖ = max ‖a⁺‖ ‖a⁻‖
have refine : ‖a‖ ≤ max ‖a⁺‖ ‖a⁻‖
Tactic: refine le_antisymm ?_ <| max_le (norm_posPart_le a) (norm_negPart_le a)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
| ‖a‖
have rw : ‖cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a‖
Tactic: rw [← cfcₙ_id' ℝ a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ‖a‖ ≤ max ‖a⁺‖ ‖a⁻‖
have conv_lhs : ‖cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a‖ ≤ max ‖a⁺‖ ‖a⁻‖
Tactic: conv_lhs => rw [← cfcₙ_id' ℝ a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ ‖cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a‖ ≤ max ‖a⁺‖ ‖a⁻‖
have rw : ∀ x ∈ quasispectrum ℝ a, ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖
Tactic: rw [norm_cfcₙ_le_iff ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
⊢ ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖
have inl : ∀ (hx' : 0 ≤ x), ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖
Tactic: obtain (hx' | hx') := le_total 0 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
inl : ∀ (hx' : 0 ≤ x), ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖
⊢ ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖
have inr : ∀ (hx' : x ≤ 0), ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖
Tactic: obtain (hx' | hx') := le_total 0 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : 0 ≤ x
⊢ ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖
have inl : ‖x‖ ≤ ‖a⁺‖
Tactic: apply le_max_of_le_left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : 0 ≤ x
⊢ ‖x‖ ≤ ‖a⁺‖
have inl : ‖x‖ = ‖x⁺‖
Tactic: refine le_of_eq_of_le ?_ <| norm_apply_le_norm_cfcₙ _ a hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : 0 ≤ x
⊢ ‖x‖ = ‖x⁺‖
have inl : ‖x‖ = ‖x‖
Tactic: rw [posPart_eq_self.mpr hx']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : x ≤ 0
⊢ ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖
have inr : ‖x‖ ≤ ‖a⁻‖
Tactic: apply le_max_of_le_right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : x ≤ 0
⊢ ‖x‖ ≤ ‖a⁻‖
have inr : ‖x‖ = ‖x⁻‖
Tactic: refine le_of_eq_of_le ?_ <| norm_apply_le_norm_cfcₙ _ a hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : x ≤ 0
⊢ ‖x‖ = ‖x⁻‖
have inr : ‖x‖ = ‖-x‖
Tactic: rw [negPart_eq_neg.mpr hx', norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : StarRing A
inst_5 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : x ≤ 0
inr : ‖x‖ = ‖-x‖
⊢ ‖x‖ = ‖x⁻‖
have inr₁ : ‖x‖ = ‖x‖
Tactic: rw [negPart_eq_neg.mpr hx', norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
a : A
y : ℝ≥0
ha : 0 ≤ a
⊢ a ^ y = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ (↑y : ℝ)) a
have rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(x.toNNReal.nnrpow y) : ℝ)) a =
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ (↑y : ℝ)) a
Tactic: rw [nnrpow_def, cfcₙ_nnreal_eq_real ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
a : A
y : ℝ≥0
ha : 0 ≤ a
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(x.toNNReal.nnrpow y) : ℝ)) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ (↑y : ℝ)) a
have refine : Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(x.toNNReal.nnrpow y) : ℝ)) (fun (x : ℝ) ↦ x ^ (↑y : ℝ)) (quasispectrum ℝ a)
Tactic: refine cfcₙ_congr ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
a : A
y : ℝ≥0
ha : 0 ≤ a
x : ℝ
hx : x ∈ quasispectrum ℝ a
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ (↑(x.toNNReal.nnrpow y) : ℝ)) x) ((fun (x : ℝ) ↦ x ^ (↑y : ℝ)) x)
have this : 0 ≤ x
Tactic: have : 0 ≤ x := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
⊢ a ^ (x + y) = a ^ x * a ^ y
have simp : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow (x + y)) a =
  cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a *
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow y) a
Tactic: simp only [nnrpow_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow (x + y)) a =
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a *
      cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow y) a
have rw : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow (x + y)) a =
  cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x * x_1.nnrpow y) a
Tactic: rw [← cfcₙ_mul _ _ a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow (x + y)) a =
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x * x_1.nnrpow y) a
have h : ∀ (z : ℝ≥0), z.nnrpow (x + y) = z.nnrpow x * z.nnrpow y
Tactic: congr! 2 with z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
ha : 0 ≤ a
⊢ HPow.hPow (β := ℝ≥0) a 1 = a
have simp : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x) a = a
Tactic: simp only [nnrpow_def, NNReal.nnrpow_def, NNReal.coe_one, NNReal.rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
ha : 0 ≤ a
⊢ cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a = a
have rw : a = a
Tactic: rw [cfcₙ_id ℝ≥0 a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
ha : 0 ≤ a
⊢ HPow.hPow (β := ℝ≥0) a 2 = a * a
have simp : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x * x) a = a * a
Tactic: simp only [nnrpow_def, NNReal.nnrpow_def, NNReal.coe_ofNat, NNReal.rpow_ofNat, pow_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
ha : 0 ≤ a
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (z : ℝ≥0) ↦ id z * id z) a = a * a
have rw : cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a * cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a = a * a
Tactic: rw [cfcₙ_mul id id a, cfcₙ_id ℝ≥0 a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
ha : 0 ≤ a
rw : cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a * cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a = a * a
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (z : ℝ≥0) ↦ id z * id z) a = a * a
have rw₁ : a * a = a * a
Tactic: rw [cfcₙ_mul id id a, cfcₙ_id ℝ≥0 a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
ha : 0 ≤ a
⊢ HPow.hPow (β := ℝ≥0) a 3 = a * a * a
have simp : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x * (x * x)) a = a * a * a
Tactic: simp only [nnrpow_def, NNReal.nnrpow_def, NNReal.coe_ofNat, NNReal.rpow_ofNat, pow_three]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
ha : 0 ≤ a
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (z : ℝ≥0) ↦ id z * (id z * id z)) a = a * a * a
have rw : cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a * cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (z : ℝ≥0) ↦ id z * id z) a =
  a * a * a
Tactic: rw [cfcₙ_mul id _ a, cfcₙ_mul id _ a, ← mul_assoc, cfcₙ_id ℝ≥0 a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
ha : 0 ≤ a
rw :
  cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a * cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (z : ℝ≥0) ↦ id z * id z) a =
    a * a * a
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (z : ℝ≥0) ↦ id z * (id z * id z)) a = a * a * a
have rw₁ : cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a *
    (cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a * cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a) =
  a * a * a
Tactic: rw [cfcₙ_mul id _ a, cfcₙ_mul id _ a, ← mul_assoc, cfcₙ_id ℝ≥0 a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
ha : 0 ≤ a
rw :
  cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a * cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (z : ℝ≥0) ↦ id z * id z) a =
    a * a * a
rw₁ :
  cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a *
      (cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a * cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a) =
    a * a * a
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (z : ℝ≥0) ↦ id z * (id z * id z)) a = a * a * a
have rw₂ : cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a * cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a *
    cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a =
  a * a * a
Tactic: rw [cfcₙ_mul id _ a, cfcₙ_mul id _ a, ← mul_assoc, cfcₙ_id ℝ≥0 a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ 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 : A
ha : 0 ≤ a
rw :
  cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a * cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (z : ℝ≥0) ↦ id z * id z) a =
    a * a * a
rw₁ :
  cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a *
      (cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a * cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a) =
    a * a * a
rw₂ :
  cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a * cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a *
      cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a =
    a * a * a
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (z : ℝ≥0) ↦ id z * (id z * id z)) a = a * a * a
have rw₃ : a * a * a = a * a * a
Tactic: rw [cfcₙ_mul id _ a, cfcₙ_mul id _ a, ← mul_assoc, cfcₙ_id ℝ≥0 a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
x y : ℝ≥0
⊢ (a ^ x) ^ y = a ^ (x * y)
have by_cases : ∀ (ha : 0 ≤ a), (a ^ x) ^ y = a ^ (x * y)
Tactic: by_cases ha : 0 ≤ a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
x y : ℝ≥0
by_cases : ∀ (ha : 0 ≤ a), (a ^ x) ^ y = a ^ (x * y)
⊢ (a ^ x) ^ y = a ^ (x * y)
have by_cases₁ : ∀ (ha : ¬0 ≤ a), (a ^ x) ^ y = a ^ (x * y)
Tactic: by_cases ha : 0 ≤ a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
x y : ℝ≥0
ha : 0 ≤ a
⊢ (a ^ x) ^ y = a ^ (x * y)
have inl : HPow.hPow (β := ℝ≥0) a 0 ^ y = a ^ (0 * y)
Tactic: obtain (rfl | hx) := eq_zero_or_pos x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
x y : ℝ≥0
ha : 0 ≤ a
inl : HPow.hPow (β := ℝ≥0) a 0 ^ y = a ^ (0 * y)
⊢ (a ^ x) ^ y = a ^ (x * y)
have inr : ∀ (hx : 0 < x), (a ^ x) ^ y = a ^ (x * y)
Tactic: obtain (rfl | hx) := eq_zero_or_pos x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
y : ℝ≥0
ha : 0 ≤ a
⊢ HPow.hPow (β := ℝ≥0) a 0 ^ y = a ^ (0 * y)
have inl : HPow.hPow (β := ℝ≥0) (HPow.hPow (β := ℝ≥0) a 0) 0 = a ^ HMul.hMul (α := ℝ≥0) 0 0
Tactic: obtain (rfl | hy) := eq_zero_or_pos y
Cleared hypotheses: y