awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
have h₂ : (↑x : ℝ) / 2 = (↑(x / 2) : ℝ)
Tactic: have h₂ : (x : ℝ) / 2 = NNReal.toReal (x / 2) := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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) : ℝ)
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
have h₃ : 0 < x / 2
Tactic: have h₃ : 0 < x / 2 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
have inr : sqrt (a ^ x) = a ^ ((↑x : ℝ) / 2)
Tactic: rw [← nnrpow_eq_rpow h₁, h₂, ← nnrpow_eq_rpow h₃, sqrt_nnrpow (A := A)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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)
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
have inr₁ : sqrt (a ^ x) = a ^ (↑(x / 2) : ℝ)
Tactic: rw [← nnrpow_eq_rpow h₁, h₂, ← nnrpow_eq_rpow h₃, sqrt_nnrpow (A := A)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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) : ℝ)
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
have inr₂ : sqrt (a ^ x) = a ^ (x / 2)
Tactic: rw [← nnrpow_eq_rpow h₁, h₂, ← nnrpow_eq_rpow h₃, sqrt_nnrpow (A := A)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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)
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
have inr₃ : a ^ (x / 2) = a ^ (x / 2)
Tactic: rw [← nnrpow_eq_rpow h₁, h₂, ← nnrpow_eq_rpow h₃, sqrt_nnrpow (A := A)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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)
have x₁ : 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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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)
have x₁ : 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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
⊢ sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)
have by_cases : ∀ (hx : x = 0), sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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)
⊢ sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)
have by_cases₁ : ∀ (hx : ¬x = 0), sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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)
have ha' : 0 ≤ sqrt a
Tactic: have ha' : 0 ≤ sqrt a := sqrt_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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)
have h₁ : 0 ≤ (↑x : ℝ)
Tactic: have h₁ : 0 ≤ (x : ℝ) := NNReal.zero_le_coe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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 : ℝ)
⊢ sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)
have rw : (a ^ (1 / 2)) ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)
Tactic: rw [sqrt_eq_rpow, rpow_rpow_of_exponent_nonneg _ _ _ (by simp) h₁, one_div_mul_eq_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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)
⊢ sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)
have rw₁ : a ^ (1 / 2 * (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
Tactic: rw [sqrt_eq_rpow, rpow_rpow_of_exponent_nonneg _ _ _ (by simp) h₁, one_div_mul_eq_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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)
⊢ sqrt a ^ (↑x : ℝ) = a ^ ((↑x : ℝ) / 2)
have rw₂ : a ^ ((↑x : ℝ) / 2) = a ^ ((↑x : ℝ) / 2)
Tactic: rw [sqrt_eq_rpow, rpow_rpow_of_exponent_nonneg _ _ _ (by simp) h₁, one_div_mul_eq_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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)
have case : ∀ (h₁ : 0 ≤ (↑x : ℝ)), 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
have rw : IsUnit (a ^ (↑y : ℝ)) ↔ IsUnit a
Tactic: rw [nnrpow_eq_rpow (pos_of_ne_zero hy)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
have refine : (↑y : ℝ) ≠ 0
Tactic: refine isUnit_rpow_iff a y ?_ ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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 (sqrt a) ↔ IsUnit a
have rw : IsUnit (a ^ (1 / 2)) ↔ IsUnit a
Tactic: rw [sqrt_eq_rpow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
⊢ IsUnit (sqrt a) ↔ IsStrictlyPositive a
have refine : ∀ (h : IsUnit (sqrt a)), IsStrictlyPositive a
Tactic: refine ⟨fun h => ?_, by grind [isUnit_sqrt_iff]⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
have a₁ : Nontrivial A
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
⊢ 0 ≤ a
have by_contra : ∀ (H : ¬0 ≤ a), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
⊢ False
have h₁ : IsUnit.{u_1} (M := A) 0
Tactic: rw [CFC.sqrt_of_not_nonneg H] at h
Cleared hypotheses: h, h_1, H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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 ∧ IsUnit a
have ha : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
have refine : IsUnit a
Tactic: refine ⟨ha, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
⊢ IsUnit a
have rwa : ∀ (h : IsUnit a) (ha : 0 ≤ a), IsUnit a
Tactic: rwa [isUnit_sqrt_iff _ ha] at h
Cleared hypotheses: h, ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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)
have rw : a ^ (-x) = a ^ (x * -1)
Tactic: rw [rpow_rpow (hx := hx) (ha := by grind)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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)
have this : a ^ (-x) = HPow.hPow (β := ℝ) (a ^ x) (-1)
Tactic: have : a ^ (-x) = (a ^ x) ^ (-1 : ℝ) := by
    rw [rpow_rpow (hx := hx) (ha := by grind)]
    simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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)
have this₁ : a ^ (-x) = (a ^ x)⁻¹ʳ
Tactic: rw [← inverse_eq_rpow_neg_one (by grind)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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)⁻¹ʳ
⊢ (a ^ x)⁻¹ʳ = a ^ (-x)
have rw : (a ^ x)⁻¹ʳ = (a ^ x)⁻¹ʳ
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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 a⁻¹ʳ
have rw : IsStrictlyPositive (HPow.hPow (β := ℝ) a (-1))
Tactic: rw [CFC.inverse_eq_rpow_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
⊢ IsStrictlyPositive a⁻¹ʳ ↔ IsStrictlyPositive a
have a₁ : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
have refine : ∀ (h : IsStrictlyPositive a⁻¹ʳ), IsStrictlyPositive a
Tactic: refine ⟨fun h => ?_, IsStrictlyPositive.ringInverse⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
have by_contra : ∀ (H : ¬IsUnit a), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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
⊢ False
have h₁ : 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
Cleared hypotheses: h, H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
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⁻¹ʳ
⊢ IsStrictlyPositive a
have ha : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
have rw : IsStrictlyPositive a⁻¹ʳ⁻¹ʳ
Tactic: rw [← Ring.inverse_inverse ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
have pos : ∀ (ha : IsStrictlyPositive a), sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
Tactic: by_cases ha : IsStrictlyPositive a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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)⁻¹ʳ
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
have neg : ∀ (ha : ¬IsStrictlyPositive a), sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
Tactic: by_cases ha : IsStrictlyPositive a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
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
⊢ sqrt a⁻¹ʳ = (sqrt a)⁻¹ʳ
have pos : a ^ (-1 * (1 / 2)) = a ^ (-(1 / 2))
Tactic: rw [sqrt_eq_rpow, sqrt_eq_rpow, inverse_rpow _ _ (by grind),
        inverse_eq_rpow_neg_one, rpow_rpow _ _ _ (by grind)]