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
inst_10 : Nontrivial A
a : A
refine : ∀ (h : sqrt a = 1), 0 ≤ a
⊢ sqrt a = 1 ↔ a = 1

Tactic:
refine ⟨fun h ↦ sqrt_eq_one_iff a ?_ |>.mp h, fun h ↦ by subst h; exact sqrt_one⟩
-- 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
inst_10 : Nontrivial A
a : A
h : sqrt a = 1
⊢ Eq.{u_1 + 1} (α := A)
    (if h :
        0 ≤ a ∧
          ContinuousOn (Y := ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (quasispectrum ℝ≥0 a) ∧
            Eq (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) 0) 0 then
      (cfcₙHom (p := fun (x : A) ↦ 0 ≤ x) ⋯ : (a : ContinuousMapZero (↑(quasispectrum ℝ≥0 a) : Type) ℝ≥0) → A)
        { toFun := (quasispectrum ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0),
          continuous_toFun := ⋯, map_zero' := ⋯ : ContinuousMapZero (↑(quasispectrum ℝ≥0 a) : Type) ℝ≥0 }
    else 0)
    1

Tactic:
rw [sqrt, cfcₙ] at h

Premises used: cfcₙ, CFC.sqrt
-- 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
inst_10 : Nontrivial A
a : A
h :
  Eq.{u_1 + 1} (α := A)
    (if h :
        0 ≤ a ∧
          ContinuousOn (Y := ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (quasispectrum ℝ≥0 a) ∧
            Eq (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) 0) 0 then
      (cfcₙHom (p := fun (x : A) ↦ 0 ≤ x) ⋯ : (a : ContinuousMapZero (↑(quasispectrum ℝ≥0 a) : Type) ℝ≥0) → A)
        { toFun := (quasispectrum ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0),
          continuous_toFun := ⋯, map_zero' := ⋯ : ContinuousMapZero (↑(quasispectrum ℝ≥0 a) : Type) ℝ≥0 }
    else 0)
    1
⊢ 0 ≤ a

Tactic:
cfc_tac
-- 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 : ℝ
h : IsUnit a
hx : x ≠ 0
by_cases : ∀ (hnonneg : 0 ≤ a), sqrt (a ^ x) = a ^ (x / 2)
by_cases₁ : ∀ (hnonneg : ¬0 ≤ a), sqrt (a ^ x) = a ^ (x / 2)
⊢ sqrt (a ^ x) = a ^ (x / 2)

Tactic:
by_cases hnonneg : 0 ≤ 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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : 0 ≤ a
⊢ IsStrictlyPositive a

Tactic:
grind
-- 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 : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : 0 ≤ a
⊢ IsStrictlyPositive a

Tactic:
have : IsStrictlyPositive a := by grind
-- 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 : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : 0 ≤ a
this : IsStrictlyPositive a
⊢ sqrt (a ^ x) = a ^ (x / 2)

Tactic:
simp [sqrt_eq_rpow, div_eq_mul_inv, one_mul, rpow_rpow _ _ _ hx]

Premises used: CFC.sqrt_eq_rpow, CFC.rpow_rpow, div_eq_mul_inv, one_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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : 0 ≤ a
⊢ sqrt (a ^ x) = a ^ (x / 2)

Tactic:
case pos =>
    have : IsStrictlyPositive a := by grind
    simp [sqrt_eq_rpow, div_eq_mul_inv, one_mul, rpow_rpow _ _ _ hx]

Premises used: CFC.sqrt_eq_rpow, CFC.rpow_rpow, div_eq_mul_inv, one_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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : ¬0 ≤ a
⊢ sqrt (a ^ x) = a ^ (x / 2)

Tactic:
simp [sqrt_eq_cfc, rpow_def, cfc_apply_of_not_predicate a hnonneg]

Premises used: CFC.rpow_def, cfc_apply_of_not_predicate, CFC.sqrt_eq_cfc
-- 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 : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : ¬0 ≤ a
⊢ sqrt (a ^ x) = a ^ (x / 2)

Tactic:
case neg =>
    simp [sqrt_eq_cfc, rpow_def, cfc_apply_of_not_predicate a hnonneg]

Premises used: CFC.rpow_def, cfc_apply_of_not_predicate, CFC.sqrt_eq_cfc
-- 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 : ℝ
h : IsUnit a
ha : 0 ≤ a
⊢ IsStrictlyPositive a

Tactic:
grind
-- 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 : ℝ
h : IsUnit a
ha : 0 ≤ a
⊢ IsStrictlyPositive a

Tactic:
have : IsStrictlyPositive a := by grind
-- 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 : ℝ
h : IsUnit a
ha : 0 ≤ a
this : IsStrictlyPositive a
⊢ Ne (α := ℝ) 2⁻¹ 0

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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ
h : IsUnit a
ha : 0 ≤ a
this : IsStrictlyPositive a
rw : (a ^ (1 / 2)) ^ x = a ^ (x / 2)
rw₁ : (a ^ HMul.hMul (α := ℝ) 1 2⁻¹) ^ x = a ^ (x / 2)
rw₂ : HPow.hPow (β := ℝ) a 2⁻¹ ^ x = a ^ (x / 2)
rw₃ : a ^ (2⁻¹ * x) = a ^ (x / 2)
rw₄ rw₅ : a ^ (x / 2) = a ^ (x / 2)
⊢ sqrt a ^ x = a ^ (x / 2)

Tactic:
rw [sqrt_eq_rpow, div_eq_mul_inv, one_mul,
      rpow_rpow _ _ _ (by simp), inv_mul_eq_div]

Premises used: CFC.sqrt_eq_rpow, inv_mul_eq_div, CFC.rpow_rpow, div_eq_mul_inv, one_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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ≥0
by_cases : ∀ (htriv : 0 ≤ a), sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
by_cases₁ : ∀ (htriv : ¬0 ≤ a), sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)

Tactic:
by_cases htriv : 0 ≤ 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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ≥0
htriv : ¬0 ≤ a
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)

Tactic:
simp [sqrt_eq_cfc, rpow_def, cfc_apply_of_not_predicate a htriv]

Premises used: CFC.rpow_def, cfc_apply_of_not_predicate, CFC.sqrt_eq_cfc
-- 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 : ℝ≥0
htriv : ¬0 ≤ a
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)

Tactic:
case neg => simp [sqrt_eq_cfc, rpow_def, cfc_apply_of_not_predicate a htriv]

Premises used: CFC.rpow_def, cfc_apply_of_not_predicate, CFC.sqrt_eq_cfc
-- 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 : ℝ≥0
htriv : 0 ≤ a
hx : x = 0
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)

Tactic:
simp [hx, rpow_zero _ htriv]

Premises used: 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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ≥0
htriv : 0 ≤ a
h₁ : 0 < x
⊢ (↑x : ℝ) / 2 = (↑(x / 2) : ℝ)

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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ≥0
htriv : 0 ≤ a
h₁ : 0 < x
⊢ (↑x : ℝ) / 2 = (↑(x / 2) : ℝ)

Tactic:
have h₂ : (x : ℝ) / 2 = NNReal.toReal (x / 2) := by 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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ≥0
htriv : 0 ≤ a
h₁ : 0 < x
h₂ : (↑x : ℝ) / 2 = (↑(x / 2) : ℝ)
⊢ 0 < x / 2

Tactic:
positivity
-- 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 : ℝ≥0
htriv : 0 ≤ a
h₁ : 0 < x
h₂ : (↑x : ℝ) / 2 = (↑(x / 2) : ℝ)
⊢ 0 < x / 2

Tactic:
have h₃ : 0 < x / 2 := by positivity
-- 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 : ℝ≥0
htriv : 0 ≤ a
h₁ : 0 < x
h₂ : (↑x : ℝ) / 2 = (↑(x / 2) : ℝ)
h₃ : 0 < x / 2
inr : sqrt (a ^ x) = a ^ ((↑x : ℝ) / 2)
inr₁ : sqrt (a ^ x) = a ^ (↑(x / 2) : ℝ)
inr₂ : sqrt (a ^ x) = a ^ (x / 2)
inr₃ inr₄ : a ^ (x / 2) = a ^ (x / 2)
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)

Tactic:
rw [← nnrpow_eq_rpow h₁, h₂, ← nnrpow_eq_rpow h₃, sqrt_nnrpow (A := A)]

Premises used: CFC.sqrt_nnrpow, CFC.nnrpow_eq_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 : ℝ≥0
htriv : 0 ≤ a
⊢ x = 0 ∨ 0 < x

Tactic:
cases eq_zero_or_pos x with
    | inl hx => simp [hx, rpow_zero _ htriv]
    | inr h₁ =>
      have h₂ : (x : ℝ) / 2 = NNReal.toReal (x / 2) := by simp
      have h₃ : 0 < x / 2 := by positivity
      rw [← nnrpow_eq_rpow h₁, h₂, ← nnrpow_eq_rpow h₃, sqrt_nnrpow (A := A)]

Premises used: eq_zero_or_pos, CFC.sqrt_nnrpow, 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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ≥0
htriv : 0 ≤ a
⊢ x = 0 ∨ 0 < x

Tactic:
case pos =>
    cases eq_zero_or_pos x with
    | inl hx => simp [hx, rpow_zero _ htriv]
    | inr h₁ =>
      have h₂ : (x : ℝ) / 2 = NNReal.toReal (x / 2) := by simp
      have h₃ : 0 < x / 2 := by positivity
      rw [← nnrpow_eq_rpow h₁, h₂, ← nnrpow_eq_rpow h₃, sqrt_nnrpow (A := A)]

Premises used: eq_zero_or_pos, CFC.sqrt_nnrpow, 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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ≥0
ha : 0 ≤ a
by_cases : ∀ (hx : x = 0), sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)
by_cases₁ : ∀ (hx : ¬x = 0), sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)
⊢ sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)

Tactic:
by_cases hx : x = 0
-- 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 : ℝ≥0
ha : 0 ≤ a
hx : x = 0
⊢ 0 ≤ sqrt a

Tactic:
have ha' : 0 ≤ sqrt a := sqrt_nonneg _
-- 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 : ℝ≥0
ha : 0 ≤ a
hx : x = 0
ha' : 0 ≤ sqrt a
⊢ sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)

Tactic:
simp [hx, rpow_zero _ ha', rpow_zero _ ha]

Premises used: 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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ≥0
ha : 0 ≤ a
hx : x = 0
⊢ sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)

Tactic:
case pos =>
    have ha' : 0 ≤ sqrt a := sqrt_nonneg _
    simp [hx, rpow_zero _ ha', rpow_zero _ ha]

Premises used: 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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ≥0
ha : 0 ≤ a
hx : ¬x = 0
⊢ 0 ≤ (↑x : ℝ)

Tactic:
have h₁ : 0 ≤ (x : ℝ) := NNReal.zero_le_coe
-- 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 : ℝ≥0
ha : 0 ≤ a
hx : ¬x = 0
h₁ : 0 ≤ (↑x : ℝ)
⊢ 0 ≤ 1 / 2

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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
x : ℝ≥0
ha : 0 ≤ a
hx : ¬x = 0
h₁ : 0 ≤ (↑x : ℝ)
rw : (a ^ (1 / 2)) ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)
rw₁ : a ^ (1 / 2 * (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
rw₂ rw₃ : a ^ ((↑x : ℝ) / 2) = a ^ ((↑x : ℝ) / 2)
⊢ sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)

Tactic:
rw [sqrt_eq_rpow, rpow_rpow_of_exponent_nonneg _ _ _ (by simp) h₁, one_div_mul_eq_div]

Premises used: CFC.sqrt_eq_rpow, CFC.rpow_rpow_of_exponent_nonneg, one_div_mul_eq_div
-- 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 : ℝ≥0
ha : 0 ≤ a
hx : ¬x = 0
case case₁ case₂ : ∀ (h₁ : 0 ≤ (↑x : ℝ)), sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)
⊢ sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)

Tactic:
case neg =>
    have h₁ : 0 ≤ (x : ℝ) := NNReal.zero_le_coe
    rw [sqrt_eq_rpow, rpow_rpow_of_exponent_nonneg _ _ _ (by simp) h₁, one_div_mul_eq_div]

Premises used: CFC.sqrt_eq_rpow, one_div_mul_eq_div
-- 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
y : ℝ≥0
hy : y ≠ 0
ha : 0 ≤ a
rw : IsUnit (a ^ (↑y : ℝ)) ↔ IsUnit a
⊢ IsUnit (a ^ y) ↔ IsUnit a

Tactic:
rw [nnrpow_eq_rpow (pos_of_ne_zero hy)]

Premises used: pos_of_ne_zero, CFC.nnrpow_eq_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
y : ℝ≥0
hy : y ≠ 0
ha : 0 ≤ a
⊢ IsUnit (a ^ (↑y : ℝ)) ↔ IsUnit a

Tactic:
isUnit_rpow_iff a y ?_ ha

Premises used: CFC.isUnit_rpow_iff, NNReal.toReal
-- 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
y : ℝ≥0
hy : y ≠ 0
ha : 0 ≤ a
refine : (↑y : ℝ) ≠ 0
⊢ IsUnit (a ^ (↑y : ℝ)) ↔ IsUnit a

Tactic:
refine isUnit_rpow_iff a y ?_ ha

Premises used: CFC.isUnit_rpow_iff, NNReal.toReal
-- 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
y : ℝ≥0
hy : y ≠ 0
ha : 0 ≤ a
⊢ (↑y : ℝ) ≠ 0

Tactic:
exact_mod_cast hy
-- 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
y : ℝ≥0
ha_unit : IsUnit a
hy : y ≠ 0
ha : 0 ≤ a
⊢ IsUnit (a ^ y)

Tactic:
(isUnit_nnrpow_iff a y hy ha).mpr ha_unit

Premises used: Iff.mpr, CFC.isUnit_nnrpow_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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
ha : 0 ≤ a
rw : IsUnit (a ^ (1 / 2)) ↔ IsUnit a
⊢ IsUnit (sqrt a) ↔ IsUnit a

Tactic:
rw [sqrt_eq_rpow]

Premises used: CFC.sqrt_eq_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
ha : 0 ≤ a
⊢ 1 / 2 ≠ 0

Tactic:
simp