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
ha : 0 ≤ a
⊢ IsUnit (a ^ (1 / 2)) ↔ IsUnit a

Tactic:
exact isUnit_rpow_iff a _ (by simp) ha

Premises used: CFC.isUnit_rpow_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
⊢ IsStrictlyPositive a → IsUnit (sqrt a)

Tactic:
grind [isUnit_sqrt_iff]

Premises used: CFC.isUnit_sqrt_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
refine : ∀ (h : IsUnit (sqrt a)), IsStrictlyPositive a
⊢ IsUnit (sqrt a) ↔ IsStrictlyPositive a

Tactic:
refine ⟨fun h => ?_, by grind [isUnit_sqrt_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
h : IsUnit (sqrt a)
⊢ Nontrivial A

Tactic:
nontriviality
-- 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
h : IsUnit (sqrt a)
h_1 : Nontrivial A
by_contra : ∀ (H : ¬0 ≤ a), False
⊢ 0 ≤ a

Tactic:
by_contra H
-- 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
h : IsUnit (sqrt a)
h_1 : Nontrivial A
H : ¬0 ≤ a
⊢ IsUnit.{u_1} (M := A) 0

Tactic:
rw [CFC.sqrt_of_not_nonneg H] at h

Premises used: CFC.sqrt_of_not_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
h : IsUnit (sqrt a)
h_1 : Nontrivial A
H : ¬0 ≤ a
h₁ : IsUnit.{u_1} (M := A) 0
⊢ Nontrivial A

Tactic:
rw [CFC.sqrt_of_not_nonneg H] at h

Premises used: CFC.sqrt_of_not_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
h : IsUnit (sqrt a)
h_1 : Nontrivial A
H : ¬0 ≤ a
h₁ : IsUnit.{u_1} (M := A) 0
a₁ : Nontrivial A
⊢ ¬0 ≤ a

Tactic:
rw [CFC.sqrt_of_not_nonneg H] at h

Premises used: CFC.sqrt_of_not_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
h : IsUnit.{u_1} (M := A) 0
h_1 : Nontrivial A
H : ¬0 ≤ a
⊢ False

Tactic:
not_isUnit_zero h

Premises used: not_isUnit_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
h : IsUnit.{u_1} (M := A) 0
h_1 : Nontrivial A
H : ¬0 ≤ a
⊢ False

Tactic:
exact not_isUnit_zero h

Premises used: not_isUnit_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
h : IsUnit (sqrt a)
⊢ 0 ≤ a

Tactic:
have ha : 0 ≤ a := by
    nontriviality
    by_contra H
    rw [CFC.sqrt_of_not_nonneg H] at h
    exact not_isUnit_zero h
-- 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
h : IsUnit (sqrt a)
ha : 0 ≤ a
⊢ 0 ≤ a ∧ IsUnit a

Tactic:
⟨ha, ?_⟩

Premises used: And.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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
h : IsUnit (sqrt a)
ha : 0 ≤ a
refine : IsUnit a
⊢ 0 ≤ a ∧ IsUnit a

Tactic:
refine ⟨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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
a : A
h : IsUnit (sqrt a)
ha : 0 ≤ a
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : IsUnit a) (ha : 0 ≤ a), IsUnit a
⊢ IsUnit a

Tactic:
rwa [isUnit_sqrt_iff _ ha] at h

Premises used: CFC.isUnit_sqrt_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 : IsStrictlyPositive a
⊢ IsUnit (sqrt 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
y : ℝ≥0
hy : y ≠ 0
ha : IsStrictlyPositive a
⊢ IsStrictlyPositive (a ^ y)

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
ha : IsStrictlyPositive a
⊢ IsStrictlyPositive (CFC.sqrt 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
a : A
y : ℝ
ha : IsStrictlyPositive a
⊢ IsStrictlyPositive (a ^ y)

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 : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
y : ℝ
⊢ 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 : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
rw : a ^ (-x) = a ^ (x * -1)
⊢ a ^ (-x) = HPow.hPow (β := ℝ) (a ^ x) (-1)

Tactic:
rw [rpow_rpow (hx := hx) (ha := by grind)]

Premises used: CFC.rpow_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 : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ a ^ (-x) = a ^ (x * -1)

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 : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
⊢ a ^ (-x) = HPow.hPow (β := ℝ) (a ^ x) (-1)

Tactic:
have : a ^ (-x) = (a ^ x) ^ (-1 : ℝ) := by
    rw [rpow_rpow (hx := hx) (ha := by grind)]
    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 : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
this : a ^ (-x) = HPow.hPow (β := ℝ) (a ^ x) (-1)
⊢ IsStrictlyPositive (a ^ x)

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 : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
this : a ^ (-x) = HPow.hPow (β := ℝ) (a ^ x) (-1)
⊢ a ^ (-x) = (a ^ x)⁻¹ʳ

Tactic:
rw [← inverse_eq_rpow_neg_one (by grind)] at this

Premises used: CFC.inverse_eq_rpow_neg_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
a : A
x : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
this : a ^ (-x) = (a ^ x)⁻¹ʳ
rw rw₁ : (a ^ x)⁻¹ʳ = (a ^ x)⁻¹ʳ
⊢ (a ^ x)⁻¹ʳ = a ^ (-x)

Tactic:
rw [this]
-- 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
rw : IsStrictlyPositive (HPow.hPow (β := ℝ) a (-1))
⊢ IsStrictlyPositive a⁻¹ʳ

Tactic:
rw [CFC.inverse_eq_rpow_neg_one]

Premises used: CFC.inverse_eq_rpow_neg_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
a : A
ha : IsStrictlyPositive a
⊢ IsStrictlyPositive (HPow.hPow (β := ℝ) a (-1))

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
a : 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
h : Nontrivial A
⊢ IsStrictlyPositive a⁻¹ʳ ↔ IsStrictlyPositive a

Tactic:
⟨fun h => ?_, IsStrictlyPositive.ringInverse⟩

Premises used: IsStrictlyPositive.ringInverse, 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
h : Nontrivial A
refine : ∀ (h : IsStrictlyPositive a⁻¹ʳ), IsStrictlyPositive a
⊢ IsStrictlyPositive a⁻¹ʳ ↔ IsStrictlyPositive a

Tactic:
refine ⟨fun h => ?_, IsStrictlyPositive.ringInverse⟩
-- 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
h_1 : Nontrivial A
h : IsStrictlyPositive a⁻¹ʳ
by_contra : ∀ (H : ¬IsUnit a), False
⊢ IsUnit a

Tactic:
by_contra H
-- 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
h_1 : Nontrivial A
h : IsStrictlyPositive a⁻¹ʳ
H : ¬IsUnit a
⊢ LE.le.{u_1} (α := A) 0 0 ∧ IsUnit.{u_1} (M := A) 0

Tactic:
rw [Ring.inverse_non_unit _ H, IsStrictlyPositive.iff_of_unital] at h

Premises used: Ring.inverse_non_unit, IsStrictlyPositive.iff_of_unital
-- 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
h_1 : Nontrivial A
h : IsStrictlyPositive a⁻¹ʳ
H : ¬IsUnit a
h₁ : LE.le.{u_1} (α := A) 0 0 ∧ IsUnit.{u_1} (M := A) 0
⊢ ¬IsUnit a

Tactic:
rw [Ring.inverse_non_unit _ H, IsStrictlyPositive.iff_of_unital] at h

Premises used: Ring.inverse_non_unit, IsStrictlyPositive.iff_of_unital
-- 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
h_1 : Nontrivial A
h : LE.le.{u_1} (α := A) 0 0 ∧ IsUnit.{u_1} (M := A) 0
H : ¬IsUnit a
⊢ False

Tactic:
not_isUnit_zero h.2

Premises used: not_isUnit_zero, And.right
-- 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
h_1 : Nontrivial A
h : LE.le.{u_1} (α := A) 0 0 ∧ IsUnit.{u_1} (M := A) 0
H : ¬IsUnit a
⊢ False

Tactic:
exact not_isUnit_zero h.2

Premises used: not_isUnit_zero, And.right
-- 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
h_1 : Nontrivial A
h : IsStrictlyPositive a⁻¹ʳ
⊢ IsUnit a

Tactic:
have ha : IsUnit a := by
    by_contra H
    rw [Ring.inverse_non_unit _ H, IsStrictlyPositive.iff_of_unital] at h
    exact not_isUnit_zero h.2
-- 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
h_1 : Nontrivial A
h : IsStrictlyPositive a⁻¹ʳ
ha : IsUnit a
rw : IsStrictlyPositive a⁻¹ʳ⁻¹ʳ
⊢ IsStrictlyPositive a

Tactic:
rw [← Ring.inverse_inverse ha]

Premises used: Ring.inverse_inverse
-- 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
h_1 : Nontrivial A
h : IsStrictlyPositive a⁻¹ʳ
ha : IsUnit a
⊢ IsStrictlyPositive a⁻¹ʳ⁻¹ʳ

Tactic:
h.ringInverse

Premises used: IsStrictlyPositive.ringInverse
-- 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
h_1 : Nontrivial A
h : IsStrictlyPositive a⁻¹ʳ
ha : IsUnit a
⊢ IsStrictlyPositive a⁻¹ʳ⁻¹ʳ

Tactic:
exact h.ringInverse

Premises used: IsStrictlyPositive.ringInverse
-- 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
⊢ 0 ≤ a⁻¹ʳ ↔ 0 ≤ a

Tactic:
grind [isStrictlyPositive_ringInverse_iff]

Premises used: isStrictlyPositive_ringInverse_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
pos : ∀ (ha : IsStrictlyPositive a), sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
neg : ∀ (ha : ¬IsStrictlyPositive a), sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ

Tactic:
by_cases ha : IsStrictlyPositive a

Premises used: IsStrictlyPositive
-- 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 : IsStrictlyPositive a
⊢ 1 / 2 ≠ 0

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
ha : IsStrictlyPositive a
⊢ Ne (α := ℝ) (-1) 0

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
ha : IsStrictlyPositive a
pos : a ^ (-1 * (1 / 2)) = a ^ (-(1 / 2))
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ

Tactic:
rw [sqrt_eq_rpow, sqrt_eq_rpow, inverse_rpow _ _ (by grind),
        inverse_eq_rpow_neg_one, rpow_rpow _ _ _ (by grind)]

Premises used: CFC.sqrt_eq_rpow, CFC.rpow_rpow, CFC.inverse_rpow, CFC.inverse_eq_rpow_neg_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
a : A
ha : IsStrictlyPositive a
⊢ a ^ (-1 * (1 / 2)) = a ^ (-(1 / 2))

Tactic:
grind only
-- 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 rwa rwa₁ rwa₂ rwa₃ : ¬IsStrictlyPositive a
⊢ ¬IsUnit (sqrt a)

Tactic:
rwa [CFC.isUnit_sqrt_iff_isStrictlyPositive]

Premises used: CFC.isUnit_sqrt_iff_isStrictlyPositive
-- 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 : ¬IsStrictlyPositive a
⊢ ¬IsUnit (sqrt a)

Tactic:
have ha' : ¬IsUnit (sqrt a) := by rwa [CFC.isUnit_sqrt_iff_isStrictlyPositive]