awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
B : Type u_2
inst_10 : PartialOrder B
inst_11 : Ring B
inst_12 : StarRing B
inst_13 : TopologicalSpace B
inst_14 : StarOrderedRing B
inst_15 : Algebra ℝ B
inst_16 : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst_17 : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst_18 : IsSemitopologicalRing B
inst_19 : T2Space B
inst_20 : StarOrderedRing (A × B)
inst_21 : NonnegSpectrumClass ℝ B
inst_22 : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
x : ℝ
ha : IsUnit a
hb : IsUnit b
ha' : 0 ≤ a
hb' : 0 ≤ b
ha'' : 0 ∉ spectrum ℝ≥0 a
hb'' : 0 ∉ spectrum ℝ≥0 b
⊢ 0.1 ≤ (a, b).1 ∧ 0.2 ≤ (a, b).2
have left : 0.1 ≤ (a, b).1
Tactic: constructor
-- 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
B : Type u_2
inst_10 : PartialOrder B
inst_11 : Ring B
inst_12 : StarRing B
inst_13 : TopologicalSpace B
inst_14 : StarOrderedRing B
inst_15 : Algebra ℝ B
inst_16 : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst_17 : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst_18 : IsSemitopologicalRing B
inst_19 : T2Space B
inst_20 : StarOrderedRing (A × B)
inst_21 : NonnegSpectrumClass ℝ B
inst_22 : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
x : ℝ
ha : IsUnit a
hb : IsUnit b
ha' : 0 ≤ a
hb' : 0 ≤ b
ha'' : 0 ∉ spectrum ℝ≥0 a
hb'' : 0 ∉ spectrum ℝ≥0 b
left : 0.1 ≤ (a, b).1
⊢ 0.1 ≤ (a, b).1 ∧ 0.2 ≤ (a, b).2
have right : 0.2 ≤ (a, b).2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (hypothesis)
Goal:
ι : Type u_2
C : ι → Type u_3
inst : (i : ι) → PartialOrder (C i)
inst_1 : (i : ι) → Ring (C i)
inst_2 : (i : ι) → StarRing (C i)
inst_3 : (i : ι) → TopologicalSpace (C i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_3} (C i)
inst_5 : StarOrderedRing ((i : ι) → C i)
inst_6 : (i : ι) → Algebra ℝ (C i)
inst_7 : ∀ (i : ι), ContinuousFunctionalCalculus.{0, u_3} ℝ (C i) IsSelfAdjoint
inst_8 : ContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst_9 : ∀ (i : ι), IsSemitopologicalRing.{u_3} (C i)
inst_10 : ∀ (i : ι), T2Space.{u_3} (C i)
inst_11 : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst_12 : ∀ (i : ι), NonnegSpectrumClass.{0, u_3} ℝ (C i)
c : (i : ι) → C i
x : ℝ
hc : ∀ (i : ι), IsUnit (c i)
hc' : ∀ (i : ι), 0 ≤ c i
⊢ rpow c x = fun (i : ι) ↦ c i ^ x
have hc'' : ∀ (i : ι), 0 ∉ spectrum ℝ≥0 (c i)
Tactic: have hc'' : ∀ i, 0 ∉ spectrum ℝ≥0 (c i) := fun i => spectrum.zero_notMem _ (hc i)
-- 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
hx : 0 < x
⊢ a ^ x = a ^ (↑x : ℝ)
have rw : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a = a ^ (↑x : ℝ)
Tactic: rw [nnrpow_def (A := A), rpow_def, cfcₙ_eq_cfc]
-- 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
hx : 0 < x
rw : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a = a ^ (↑x : ℝ)
⊢ a ^ x = a ^ (↑x : ℝ)
have rw₁ : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a =
  cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (↑x : ℝ)) a
Tactic: rw [nnrpow_def (A := A), rpow_def, cfcₙ_eq_cfc]
-- 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
hx : 0 < x
rw : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a = a ^ (↑x : ℝ)
rw₁ :
  cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (↑x : ℝ)) a
⊢ a ^ x = a ^ (↑x : ℝ)
have rw₂ : cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a =
  cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (↑x : ℝ)) a
Tactic: rw [nnrpow_def (A := A), rpow_def, cfcₙ_eq_cfc]
-- 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
⊢ sqrt a = a ^ (1 / 2)
have this : a ^ (1 / 2) = a ^ (↑(1 / 2) : ℝ)
Tactic: have : a ^ (1 / 2 : ℝ) = a ^ ((1 / 2 : ℝ≥0) : ℝ) := rfl
-- 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
this : a ^ (1 / 2) = a ^ (↑(1 / 2) : ℝ)
⊢ sqrt a = a ^ (1 / 2)
have rw : sqrt a = a ^ (↑(1 / 2) : ℝ)
Tactic: rw [this, ← nnrpow_eq_rpow (by simp), sqrt_eq_nnrpow 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
this : a ^ (1 / 2) = a ^ (↑(1 / 2) : ℝ)
rw : sqrt a = a ^ (↑(1 / 2) : ℝ)
⊢ sqrt a = a ^ (1 / 2)
have rw₁ : sqrt a = a ^ (1 / 2)
Tactic: rw [this, ← nnrpow_eq_rpow (by simp), sqrt_eq_nnrpow 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
this : a ^ (1 / 2) = a ^ (↑(1 / 2) : ℝ)
rw : sqrt a = a ^ (↑(1 / 2) : ℝ)
rw₁ : sqrt a = a ^ (1 / 2)
⊢ sqrt a = a ^ (1 / 2)
have rw₂ : a ^ (1 / 2) = a ^ (1 / 2)
Tactic: rw [this, ← nnrpow_eq_rpow (by simp), sqrt_eq_nnrpow 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
⊢ cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) a =
    cfc (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) a
have rw : cfc (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) a =
  cfc (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) a
Tactic: rw [cfcₙ_eq_cfc]
-- 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
⊢ sqrt (HPow.hPow (β := ℕ) a 2) = a
have rw : sqrt (a * a) = a
Tactic: rw [pow_two, sqrt_mul_self (A := 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
ha : 0 ≤ a
rw : sqrt (a * a) = a
⊢ sqrt (HPow.hPow (β := ℕ) a 2) = a
have rw₁ : a = a
Tactic: rw [pow_two, sqrt_mul_self (A := 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
ha : 0 ≤ a
⊢ HPow.hPow (β := ℕ) (sqrt a) 2 = a
have rw : sqrt a * sqrt a = a
Tactic: rw [pow_two, sqrt_mul_sqrt_self (A := 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
ha : 0 ≤ a
rw : sqrt a * sqrt a = a
⊢ HPow.hPow (β := ℕ) (sqrt a) 2 = a
have rw₁ : a = a
Tactic: rw [pow_two, sqrt_mul_sqrt_self (A := 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 b : A
ha : 0 ≤ a
hb : 0 ≤ b
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b
have simp_rw : a * a = b * b ↔ a = b
Tactic: simp_rw [sq, mul_self_eq_mul_self_iff a b]
-- 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
r : ℝ≥0
⊢ Eq (α := A) (sqrt ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) r) : A)
    ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) r : ℝ≥0) : A)
have rw : cfc (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) r) =
  (algebraMap ℝ≥0 A : (a : ℝ≥0) → A) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) r : ℝ≥0)
Tactic: rw [sqrt_eq_cfc, cfc_algebraMap]
-- 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
r : ℝ≥0
rw :
  cfc (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) r) =
    (algebraMap ℝ≥0 A : (a : ℝ≥0) → A) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) r : ℝ≥0)
⊢ Eq (α := A) (sqrt ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) r) : A)
    ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) r : ℝ≥0) : A)
have rw₁ : Eq (α := A) ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) r : ℝ≥0) : A)
  ((algebraMap ℝ≥0 A : (a : ℝ≥0) → A) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) r : ℝ≥0) : A)
Tactic: rw [sqrt_eq_cfc, cfc_algebraMap]
-- 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
⊢ sqrt a = 1 ↔ a = 1
have rw : HMul.hMul (α := A) 1 1 = a ↔ a = 1
Tactic: rw [sqrt_eq_iff a _, mul_one, eq_comm]
-- 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
rw : HMul.hMul (α := A) 1 1 = a ↔ a = 1
⊢ sqrt a = 1 ↔ a = 1
have rw₁ : 1 = a ↔ a = 1
Tactic: rw [sqrt_eq_iff a _, mul_one, eq_comm]
-- 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
rw : HMul.hMul (α := A) 1 1 = a ↔ a = 1
rw₁ : 1 = a ↔ a = 1
⊢ sqrt a = 1 ↔ a = 1
have rw₂ : a = 1 ↔ a = 1
Tactic: rw [sqrt_eq_iff a _, mul_one, eq_comm]
-- 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
inst_10 : Nontrivial A
a : A
h : a = 1
⊢ sqrt a = 1
have subst : Eq.{u_1 + 1} (α := A) (sqrt 1) 1
Tactic: subst h
Cleared hypotheses: a, 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
inst_10 : Nontrivial A
a : A
⊢ sqrt a = 1 ↔ a = 1
have refine : ∀ (h : sqrt a = 1), 0 ≤ a
Tactic: refine ⟨fun h ↦ sqrt_eq_one_iff a ?_ |>.mp h, fun h ↦ by subst h; exact sqrt_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
inst_8 : IsSemitopologicalRing A
inst_9 : T2Space A
inst_10 : Nontrivial A
a : A
h : sqrt a = 1
⊢ 0 ≤ a
have 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) sorry : (a : ContinuousMapZero (↑(quasispectrum ℝ≥0 a) : Type) ℝ≥0) → A)
      { toFun := (quasispectrum ℝ≥0 a).restrict (π := fun (a : ℝ≥0) ↦ ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0),
        continuous_toFun := sorry, map_zero' := sorry : ContinuousMapZero (↑(quasispectrum ℝ≥0 a) : Type) ℝ≥0 }
  else 0)
  1
Tactic: rw [sqrt, cfcₙ] at h
Cleared hypotheses: 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
x : ℝ
h : IsUnit a
hx : x ≠ 0
⊢ sqrt (a ^ x) = a ^ (x / 2)
have by_cases : ∀ (hnonneg : 0 ≤ a), sqrt (a ^ x) = a ^ (x / 2)
Tactic: by_cases hnonneg : 0 ≤ 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 : ℝ
h : IsUnit a
hx : x ≠ 0
by_cases : ∀ (hnonneg : 0 ≤ a), sqrt (a ^ x) = a ^ (x / 2)
⊢ sqrt (a ^ x) = a ^ (x / 2)
have by_cases₁ : ∀ (hnonneg : ¬0 ≤ a), sqrt (a ^ x) = a ^ (x / 2)
Tactic: by_cases hnonneg : 0 ≤ 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 : ℝ
h : IsUnit a
hx : x ≠ 0
hnonneg : 0 ≤ a
⊢ sqrt (a ^ x) = a ^ (x / 2)
have this : IsStrictlyPositive a
Tactic: have : IsStrictlyPositive a := 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 : ℝ
h : IsUnit a
ha : 0 ≤ a
⊢ sqrt a ^ x = a ^ (x / 2)
have this : IsStrictlyPositive a
Tactic: have : IsStrictlyPositive a := by grind
-- 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 : ℝ
h : IsUnit a
ha : 0 ≤ a
this : IsStrictlyPositive a
⊢ sqrt a ^ x = a ^ (x / 2)
have rw : (a ^ (1 / 2)) ^ x = a ^ (x / 2)
Tactic: rw [sqrt_eq_rpow, div_eq_mul_inv, one_mul,
      rpow_rpow _ _ _ (by simp), inv_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 : ℝ
h : IsUnit a
ha : 0 ≤ a
this : IsStrictlyPositive a
rw : (a ^ (1 / 2)) ^ x = a ^ (x / 2)
⊢ sqrt a ^ x = a ^ (x / 2)
have rw₁ : (a ^ HMul.hMul (α := ℝ) 1 2⁻¹) ^ x = a ^ (x / 2)
Tactic: rw [sqrt_eq_rpow, div_eq_mul_inv, one_mul,
      rpow_rpow _ _ _ (by simp), inv_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 : ℝ
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)
⊢ sqrt a ^ x = a ^ (x / 2)
have rw₂ : HPow.hPow (β := ℝ) a 2⁻¹ ^ x = a ^ (x / 2)
Tactic: rw [sqrt_eq_rpow, div_eq_mul_inv, one_mul,
      rpow_rpow _ _ _ (by simp), inv_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 : ℝ
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)
⊢ sqrt a ^ x = a ^ (x / 2)
have rw₃ : a ^ (2⁻¹ * x) = a ^ (x / 2)
Tactic: rw [sqrt_eq_rpow, div_eq_mul_inv, one_mul,
      rpow_rpow _ _ _ (by simp), inv_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 : ℝ
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)
⊢ sqrt a ^ x = a ^ (x / 2)
have rw₄ : a ^ (x / 2) = a ^ (x / 2)
Tactic: rw [sqrt_eq_rpow, div_eq_mul_inv, one_mul,
      rpow_rpow _ _ _ (by simp), inv_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
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
have by_cases : ∀ (htriv : 0 ≤ a), sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
Tactic: by_cases htriv : 0 ≤ 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
by_cases : ∀ (htriv : 0 ≤ a), sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
⊢ sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
have by_cases₁ : ∀ (htriv : ¬0 ≤ a), sqrt (a ^ (↑x : ℝ)) = a ^ ((↑x : ℝ) / 2)
Tactic: by_cases htriv : 0 ≤ a