awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha : 0 ≤ a
rw :
  cfc (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) ((fun (x : ℝ≥0) ↦ x ^ y) ∘ fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x * y)) a
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y)
      (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a) =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (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 : 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
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha : 0 ≤ a
⊢ cfc (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) ((fun (x : ℝ≥0) ↦ x ^ y) ∘ fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x * y)) a

Tactic:
cfc_congr fun _ _ => ?_

Premises used: cfc_congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha : 0 ≤ a
refine : ∀ x_1 ∈ spectrum ℝ≥0 a, ((fun (x : ℝ≥0) ↦ x ^ y) ∘ fun (x_3 : ℝ≥0) ↦ x_3 ^ x) x_1 = x_1 ^ (x * y)
⊢ cfc (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) ((fun (x : ℝ≥0) ↦ x ^ y) ∘ fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x * y)) a

Tactic:
refine cfc_congr fun _ _ => ?_

Premises used: cfc_congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha : 0 ≤ a
x_1 : ℝ≥0
h : x_1 ∈ spectrum ℝ≥0 a
⊢ ((fun (x : ℝ≥0) ↦ x ^ y) ∘ fun (x_2 : ℝ≥0) ↦ x_2 ^ x) x_1 = x_1 ^ (x * y)

Tactic:
simp [NNReal.rpow_mul]

Premises used: NNReal.rpow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
x : ℝ
ha : IsStrictlyPositive a
rw : a ^ (x + -x) = 1
rw₁ : HPow.hPow (β := ℝ) a 0 = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := A) 1 1
⊢ a ^ x * a ^ (-x) = 1

Tactic:
rw [← rpow_add ha.isUnit, add_neg_cancel, rpow_zero a]

Premises used: add_neg_cancel, CFC.rpow_add, IsStrictlyPositive.isUnit, CFC.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
x : ℝ
ha : IsStrictlyPositive a
rw : a ^ (-x + x) = 1
rw₁ : HPow.hPow (β := ℝ) a 0 = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := A) 1 1
⊢ a ^ (-x) * a ^ x = 1

Tactic:
rw [← rpow_add ha.isUnit, neg_add_cancel, rpow_zero a]

Premises used: CFC.rpow_add, neg_add_cancel, IsStrictlyPositive.isUnit, CFC.rpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : Aˣ
ha : 0 ≤ (↑a : A)
⊢ HPow.hPow (β := ℝ) (↑a : A) (-1) = (↑a⁻¹ : A)

Tactic:
a.inv_eq_of_mul_eq_one_left ?_ |>.symm

Premises used: Units.inv_eq_of_mul_eq_one_left, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : Aˣ
ha : 0 ≤ (↑a : A)
refine : HPow.hPow (β := ℝ) (↑a : A) (-1) * (↑a : A) = 1
⊢ HPow.hPow (β := ℝ) (↑a : A) (-1) = (↑a⁻¹ : A)

Tactic:
refine a.inv_eq_of_mul_eq_one_left ?_ |>.symm

Premises used: Units.inv_eq_of_mul_eq_one_left, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : Aˣ
ha : 0 ≤ (↑a : A)
⊢ HPow.hPow (β := ℝ) (↑a : A) (-1) * (↑a : A) = 1

Tactic:
simpa [rpow_one (a : A)] using rpow_neg_mul_rpow 1 (a.isStrictlyPositive_iff.mpr ha)

Premises used: Iff.mpr, Units.val, CFC.rpow_one, Units.isStrictlyPositive_iff, OfNat.ofNat, CFC.rpow_neg_mul_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
A : Type u_2
inst : PartialOrder A
inst_1 : NormedRing A
inst_2 : StarRing A
inst_3 : StarOrderedRing A
inst_4 : NormedAlgebra ℝ A
inst_5 : NonnegSpectrumClass ℝ A
inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
⊢ HPow.hPow (β := ℝ) a (-1) = cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x⁻¹) a

Tactic:
cfc_congr fun x _ ↦ NNReal.rpow_neg_one x

Premises used: NNReal.rpow_neg_one, cfc_congr, CFC.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
ha : IsStrictlyPositive a
obtain : ∀ (ax : Aˣ) (hax : (↑ax : A) = a), Ring.inverse a = HPow.hPow (β := ℝ) a (-1)
⊢ Ring.inverse a = HPow.hPow (β := ℝ) a (-1)

Tactic:
obtain ⟨ax, hax⟩ := ha.isUnit

Premises used: IsStrictlyPositive.isUnit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
ha : IsStrictlyPositive a
ax : Aˣ
hax : (↑ax : A) = a
⊢ Ring.inverse a = HPow.hPow (β := ℝ) a (-1)

Tactic:
simp only [← hax, Ring.inverse_invertible, invOf_units, CFC.rpow_neg_one_eq_inv ax]

Premises used: Ring.inverse_invertible, CFC.rpow_neg_one_eq_inv, invOf_units
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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ˣ
x : ℝ
ha' : 0 ≤ (↑a : A)
h₁ : ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ x) (Inv.inv '' spectrum ℝ≥0 (↑a : A))
rw :
  cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (-x)) (↑a : A) =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1⁻¹ ^ x) (↑a : A)
⊢ (↑a : A) ^ (-x) = (↑a⁻¹ : A) ^ x

Tactic:
rw [← cfc_inv_id (R := ℝ≥0) a, rpow_def, rpow_def,
        ← cfc_comp' (fun z => z ^ x) (Inv.inv : ℝ≥0 → ℝ≥0) (a : A) h₁]

Premises used: Units.val, CFC.rpow_def, cfc_comp', cfc_inv_id, Inv.inv, HPow.hPow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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ˣ
x : ℝ
ha' : 0 ≤ (↑a : A)
h₁ : ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ x) (Inv.inv '' spectrum ℝ≥0 (↑a : A))
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (-x)) (↑a : A) =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1⁻¹ ^ x) (↑a : A)

Tactic:
cfc_congr fun _ _ => ?_

Premises used: cfc_congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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ˣ
x : ℝ
ha' : 0 ≤ (↑a : A)
h₁ : ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ x) (Inv.inv '' spectrum ℝ≥0 (↑a : A))
refine : ∀ x_1 ∈ spectrum ℝ≥0 (↑a : A), x_1 ^ (-x) = x_1⁻¹ ^ x
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (-x)) (↑a : A) =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1⁻¹ ^ x) (↑a : A)

Tactic:
refine cfc_congr fun _ _ => ?_

Premises used: cfc_congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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ˣ
x : ℝ
ha' : 0 ≤ (↑a : A)
h₁ : ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ x) (Inv.inv '' spectrum ℝ≥0 (↑a : A))
x_1 : ℝ≥0
h : x_1 ∈ spectrum ℝ≥0 (↑a : A)
⊢ x_1 ^ (-x) = x_1⁻¹ ^ x

Tactic:
simp [NNReal.rpow_neg, NNReal.inv_rpow]

Premises used: NNReal.inv_rpow, NNReal.rpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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ˣ
x : ℝ
ha' : 0 ≤ (↑a : A)
suffices : ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ x) (Inv.inv '' spectrum ℝ≥0 (↑a : A))
⊢ (↑a : A) ^ (-x) = (↑a⁻¹ : A) ^ x

Tactic:
suffices h₁ : ContinuousOn (fun z ↦ z ^ x) (Inv.inv '' (spectrum ℝ≥0 (a : A))) by
    rw [← cfc_inv_id (R := ℝ≥0) a, rpow_def, rpow_def,
        ← cfc_comp' (fun z => z ^ x) (Inv.inv : ℝ≥0 → ℝ≥0) (a : A) h₁]
    refine cfc_congr fun _ _ => ?_
    simp [NNReal.rpow_neg, NNReal.inv_rpow]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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ˣ
x : ℝ
ha' : 0 ≤ (↑a : A)
⊢ ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ x) (Inv.inv '' spectrum ℝ≥0 (↑a : A))

Tactic:
NNReal.continuousOn_rpow_const (.inl ?_)

Premises used: NNReal.continuousOn_rpow_const, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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ˣ
x : ℝ
ha' : 0 ≤ (↑a : A)
refine : 0 ∉ Inv.inv '' spectrum ℝ≥0 (↑a : A)
⊢ ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ x) (Inv.inv '' spectrum ℝ≥0 (↑a : A))

Tactic:
refine NNReal.continuousOn_rpow_const (.inl ?_)

Premises used: NNReal.continuousOn_rpow_const, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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ˣ
x : ℝ
ha' : 0 ≤ (↑a : A)
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 (↑a : A)
hz' : z⁻¹ = 0
⊢ False

Tactic:
spectrum.zero_notMem ℝ≥0 a.isUnit <| inv_eq_zero.mp hz' ▸ hz

Premises used: inv_eq_zero, spectrum.zero_notMem, Eq.rec, NNReal, Iff.mp, Units.isUnit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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ˣ
x : ℝ
ha' : 0 ≤ (↑a : A)
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 (↑a : A)
hz' : z⁻¹ = 0
⊢ False

Tactic:
exact spectrum.zero_notMem ℝ≥0 a.isUnit <| inv_eq_zero.mp hz' ▸ hz

Premises used: spectrum.zero_notMem, NNReal, Units.isUnit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : Aˣ
n : ℤ
ha : 0 ≤ (↑a : A)
rw :
  cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑a : A) =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ n) (↑a : A)
⊢ HPow.hPow (β := ℝ) (↑a : A) (↑n : ℝ) = (↑(a ^ n) : A)

Tactic:
rw [← cfc_zpow (R := ℝ≥0) a n, rpow_def]

Premises used: CFC.rpow_def, cfc_zpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : Aˣ
n : ℤ
ha : 0 ≤ (↑a : A)
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑a : A) =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ n) (↑a : A)

Tactic:
cfc_congr fun _ _ => ?_

Premises used: cfc_congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : Aˣ
n : ℤ
ha : 0 ≤ (↑a : A)
refine : ∀ x ∈ spectrum ℝ≥0 (↑a : A), HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑a : A) =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ n) (↑a : A)

Tactic:
refine cfc_congr fun _ _ => ?_

Premises used: cfc_congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : Aˣ
n : ℤ
ha : 0 ≤ (↑a : A)
x : ℝ≥0
h : x ∈ spectrum ℝ≥0 (↑a : A)
⊢ HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
ha : IsUnit a
x : ℝ
ha_nonneg : 0 ≤ a
⊢ IsUnit (a ^ x)

Tactic:
ha.unit.cfcRpow x |>.isUnit

Premises used: Units.cfcRpow, IsUnit.unit, Units.isUnit
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
x : ℝ
h : ContinuousOn (Y := ℝ≥0) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) (spectrum ℝ≥0 a)
ha : 0 ≤ a
⊢ spectrum ℝ≥0 (a ^ x) = (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) '' spectrum ℝ≥0 a

Tactic:
cfc_map_spectrum (· ^ x : ℝ≥0 → ℝ≥0) a ha h

Premises used: cfc_map_spectrum, HPow.hPow, CFC.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h : Nontrivial A
⊢ IsUnit (a ^ y) ↔ IsUnit a

Tactic:
⟨fun h => ?_, fun h => h.cfcRpow y ha⟩

Premises used: IsUnit.cfcRpow, Iff.intro
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h : Nontrivial A
refine : ∀ (h : IsUnit (a ^ y)), IsUnit a
⊢ IsUnit (a ^ y) ↔ IsUnit a

Tactic:
refine ⟨fun h => ?_, fun h => h.cfcRpow y ha⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : IsUnit (a ^ y)
⊢ IsUnit (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) a)

Tactic:
rw [rpow_def] at h

Premises used: CFC.rpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : IsUnit (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) a)
pos : ∀ (hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)), IsUnit a
neg : ∀ (hf : ¬ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)), IsUnit a
⊢ IsUnit a

Tactic:
by_cases hf : ContinuousOn (fun x : ℝ≥0 => x ^ y) (spectrum ℝ≥0 a)

Premises used: spectrum, NNReal, HPow.hPow, ContinuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : IsUnit (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) a)
hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
⊢ ∀ x ∈ spectrum ℝ≥0 a, x ^ y ≠ 0

Tactic:
rw [isUnit_cfc_iff _ a hf] at h

Premises used: isUnit_cfc_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : IsUnit (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) a)
hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
h₁ : ∀ x ∈ spectrum ℝ≥0 a, x ^ y ≠ 0
⊢ ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)

Tactic:
rw [isUnit_cfc_iff _ a hf] at h

Premises used: isUnit_cfc_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : ∀ x ∈ spectrum ℝ≥0 a, x ^ y ≠ 0
hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
⊢ IsUnit a

Tactic:
spectrum.isUnit_of_zero_notMem ℝ≥0 ?_

Premises used: NNReal, spectrum.isUnit_of_zero_notMem
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : ∀ x ∈ spectrum ℝ≥0 a, x ^ y ≠ 0
hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
pos : 0 ∉ spectrum ℝ≥0 a
⊢ IsUnit a

Tactic:
refine spectrum.isUnit_of_zero_notMem ℝ≥0 ?_

Premises used: NNReal, spectrum.isUnit_of_zero_notMem
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : ∀ x ∈ spectrum ℝ≥0 a, x ^ y ≠ 0
hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
h0 : 0 ∈ spectrum ℝ≥0 a
⊢ HPow.hPow (α := ℝ≥0) 0 y ≠ 0

Tactic:
specialize h 0 h0

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
h0 : 0 ∈ spectrum ℝ≥0 a
h : HPow.hPow (α := ℝ≥0) 0 y ≠ 0
⊢ y = 0

Tactic:
simp only [ne_eq, NNReal.rpow_eq_zero_iff, true_and, Decidable.not_not] at h

Premises used: ne_eq, NNReal.rpow_eq_zero_iff, Decidable.not_not, true_and
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
h0 : 0 ∈ spectrum ℝ≥0 a
h : y = 0
⊢ False

Tactic:
hy h