awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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 : ℝ≥0
⊢ 0 ≤ a ^ x

Tactic:
cfcₙ_predicate _ a

Premises used: cfcₙ_predicate, CFC.nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
y : ℝ≥0
⊢ a ^ y = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow y) a

Tactic:
rfl

Premises used: CFC.nnrpow, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
rw :
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(x.toNNReal.nnrpow y) : ℝ)) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ (↑y : ℝ)) a
⊢ a ^ y = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ (↑y : ℝ)) a

Tactic:
rw [nnrpow_def, cfcₙ_nnreal_eq_real ..]

Premises used: CFC.nnrpow_def, cfcₙ_nnreal_eq_real
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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

Tactic:
cfcₙ_congr ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
refine : Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(x.toNNReal.nnrpow y) : ℝ)) (fun (x : ℝ) ↦ x ^ (↑y : ℝ)) (quasispectrum ℝ a)
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(x.toNNReal.nnrpow y) : ℝ)) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x ^ (↑y : ℝ)) a

Tactic:
refine cfcₙ_congr ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ 0 ≤ x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ 0 ≤ x

Tactic:
have : 0 ≤ x := by grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
this : 0 ≤ x
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ (↑(x.toNNReal.nnrpow y) : ℝ)) x) ((fun (x : ℝ) ↦ x ^ (↑y : ℝ)) x)

Tactic:
simp [this]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
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
⊢ a ^ (x + y) = a ^ x * a ^ y

Tactic:
simp only [nnrpow_def]

Premises used: CFC.nnrpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
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
⊢ 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:
rw [← cfcₙ_mul _ _ a]

Premises used: cfcₙ_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
h : ∀ (z : ℝ≥0), z.nnrpow (x + y) = z.nnrpow x * z.nnrpow 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

Tactic:
congr! 2 with z
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
z : ℝ≥0
⊢ z.nnrpow (x + y) = z.nnrpow x * z.nnrpow y

Tactic:
mod_cast z.rpow_add' <| ne_of_gt (add_pos hx hy)

Premises used: HMul.hMul, add_pos, cast, ne_of_gt, NNReal.rpow_add', HAdd.hAdd, NNReal.nnrpow, Eq.refl, Eq
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
z : ℝ≥0
⊢ z.nnrpow (x + y) = z.nnrpow x * z.nnrpow y

Tactic:
exact mod_cast z.rpow_add' <| ne_of_gt (add_pos hx hy)

Premises used: add_pos, ne_of_gt, NNReal.rpow_add'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ HPow.hPow (β := ℝ≥0) a 0 = 0

Tactic:
simp [nnrpow_def, cfcₙ_apply_of_not_map_zero]

Premises used: cfcₙ_apply_of_not_map_zero, CFC.nnrpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
simp : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x) a = a
⊢ HPow.hPow (β := ℝ≥0) a 1 = a

Tactic:
simp only [nnrpow_def, NNReal.nnrpow_def, NNReal.coe_one, NNReal.rpow_one]

Premises used: CFC.nnrpow_def, NNReal.nnrpow_def, NNReal.coe_one, NNReal.rpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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 rw₁ : a = a
⊢ cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) id a = a

Tactic:
rw [cfcₙ_id ℝ≥0 a]

Premises used: NNReal, cfcₙ_id
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ Set.EqOn (fun (a : A) ↦ HPow.hPow (β := ℝ≥0) a 1) id (Set.Ici 0)

Tactic:
fun _ ha => CFC.nnrpow_one _ ha

Premises used: CFC.nnrpow_one, Set.EqOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
simp : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x * x) a = a * a
⊢ HPow.hPow (β := ℝ≥0) a 2 = a * a

Tactic:
simp only [nnrpow_def, NNReal.nnrpow_def, NNReal.coe_ofNat, NNReal.rpow_ofNat, pow_two]

Premises used: pow_two, CFC.nnrpow_def, NNReal.rpow_ofNat, NNReal.nnrpow_def, NNReal.coe_ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
rw₁ rw₂ : a * a = a * a
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (z : ℝ≥0) ↦ id z * id z) a = a * a

Tactic:
rw [cfcₙ_mul id id a, cfcₙ_id ℝ≥0 a]

Premises used: id, NNReal, cfcₙ_id, cfcₙ_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
simp : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x * (x * x)) a = a * a * a
⊢ HPow.hPow (β := ℝ≥0) a 3 = a * a * a

Tactic:
simp only [nnrpow_def, NNReal.nnrpow_def, NNReal.coe_ofNat, NNReal.rpow_ofNat, pow_three]

Premises used: CFC.nnrpow_def, pow_three, NNReal.rpow_ofNat, NNReal.nnrpow_def, NNReal.coe_ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
rw₃ rw₄ : a * a * a = a * a * a
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (z : ℝ≥0) ↦ id z * (id z * id z)) a = a * a * a

Tactic:
rw [cfcₙ_mul id _ a, cfcₙ_mul id _ a, ← mul_assoc, cfcₙ_id ℝ≥0 a]

Premises used: mul_assoc, id, NNReal, cfcₙ_id, cfcₙ_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
x : ℝ≥0
⊢ HPow.hPow (α := A) 0 x = 0

Tactic:
simp [nnrpow_def]

Premises used: CFC.nnrpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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)
by_cases₁ : ∀ (ha : ¬0 ≤ a), (a ^ x) ^ y = a ^ (x * y)
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
by_cases ha : 0 ≤ a
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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)
inr : ∀ (hx : 0 < x), (a ^ x) ^ y = a ^ (x * y)
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
obtain (rfl | hx) := eq_zero_or_pos x

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
inl : HPow.hPow (β := ℝ≥0) (HPow.hPow (β := ℝ≥0) a 0) 0 = a ^ HMul.hMul (α := ℝ≥0) 0 0
inl₁ : ∀ (hy : 0 < y), HPow.hPow (β := ℝ≥0) a 0 ^ y = a ^ (0 * y)
⊢ HPow.hPow (β := ℝ≥0) a 0 ^ y = a ^ (0 * y)

Tactic:
obtain (rfl | hy) := eq_zero_or_pos y

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
hx : 0 < x
inr : HPow.hPow (β := ℝ≥0) (a ^ x) 0 = a ^ (x * 0)
inr₁ : ∀ (hy : 0 < y), (a ^ x) ^ y = a ^ (x * y)
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
obtain (rfl | hy) := eq_zero_or_pos y

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
ha : 0 ≤ a
⊢ HPow.hPow (β := ℝ≥0) (HPow.hPow (β := ℝ≥0) a 0) 0 = a ^ HMul.hMul (α := ℝ≥0) 0 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
ha : 0 ≤ a
⊢ HPow.hPow (β := ℝ≥0) (HPow.hPow (β := ℝ≥0) a 0) 0 = a ^ HMul.hMul (α := ℝ≥0) 0 0

Tactic:
try simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
hy : 0 < y
⊢ HPow.hPow (β := ℝ≥0) a 0 ^ y = a ^ (0 * y)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
hy : 0 < y
⊢ HPow.hPow (β := ℝ≥0) a 0 ^ y = a ^ (0 * y)

Tactic:
try simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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 : ℝ≥0
ha : 0 ≤ a
hx : 0 < x
⊢ HPow.hPow (β := ℝ≥0) (a ^ x) 0 = a ^ (x * 0)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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 : ℝ≥0
ha : 0 ≤ a
hx : 0 < x
⊢ HPow.hPow (β := ℝ≥0) (a ^ x) 0 = a ^ (x * 0)

Tactic:
try simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
hx : 0 < x
hy : 0 < y
inr :
  cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) ((fun (x : ℝ≥0) ↦ x.nnrpow y) ∘ fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a =
    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 : ℝ≥0) ↦ x.nnrpow y)
      (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_1 : ℝ≥0) ↦ x_1.nnrpow (x * y)) a

Tactic:
rw [← cfcₙ_comp _ _ a]

Premises used: cfcₙ_comp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
hx : 0 < x
hy : 0 < y
inr : ∀ (u : ℝ≥0), ((fun (x : ℝ≥0) ↦ x.nnrpow y) ∘ fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) u = u.nnrpow (x * y)
⊢ cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) ((fun (x : ℝ≥0) ↦ x.nnrpow y) ∘ fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a =
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow (x * y)) a

Tactic:
congr! 2 with u
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
hx : 0 < x
hy : 0 < y
u : ℝ≥0
inr : (↑(((fun (x : ℝ≥0) ↦ x.nnrpow y) ∘ fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) u) : ℝ) = (↑(u.nnrpow (x * y)) : ℝ)
⊢ ((fun (x : ℝ≥0) ↦ x.nnrpow y) ∘ fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) u = u.nnrpow (x * y)

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
hx : 0 < x
hy : 0 < y
u : ℝ≥0
⊢ (↑(((fun (x : ℝ≥0) ↦ x.nnrpow y) ∘ fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) u) : ℝ) = (↑(u.nnrpow (x * y)) : ℝ)

Tactic:
simp [Real.rpow_mul]

Premises used: Real.rpow_mul