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
a : A
x y : ℝ
hx : x ≠ 0
ha : IsStrictlyPositive a
ha₁' : 0 ∉ spectrum ℝ≥0 a
⊢ cfc (R := ℝ≥0) (p := LE.le 0) ((fun (x : ℝ≥0) ↦ x ^ y) ∘ fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x * y)) a
have refine : ∀ x_1 ∈ spectrum ℝ≥0 a, ((fun (x : ℝ≥0) ↦ x ^ y) ∘ fun (x_3 : ℝ≥0) ↦ x_3 ^ x) x_1 = x_1 ^ (x * y)
Tactic: refine cfc_congr fun _ _ => ?_
-- 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) ^ x⁻¹ = a
have rw : a ^ (x * x⁻¹) = a
Tactic: rw [rpow_rpow a x x⁻¹ hx, mul_inv_cancel₀ hx, rpow_one a ha.nonneg]
-- 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
rw : a ^ (x * x⁻¹) = a
⊢ (a ^ x) ^ x⁻¹ = a
have rw₁ : HPow.hPow (β := ℝ) a 1 = a
Tactic: rw [rpow_rpow a x x⁻¹ hx, mul_inv_cancel₀ hx, rpow_one a ha.nonneg]
-- 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
rw : a ^ (x * x⁻¹) = a
rw₁ : HPow.hPow (β := ℝ) a 1 = a
⊢ (a ^ x) ^ x⁻¹ = a
have rw₂ : a = a
Tactic: rw [rpow_rpow a x x⁻¹ hx, mul_inv_cancel₀ hx, rpow_one a ha.nonneg]
-- 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 y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha : 0 ≤ a
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y)
      (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a) =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x * y)) a
have rw : cfc (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) ((fun (x : ℝ≥0) ↦ x ^ y) ∘ fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a =
  cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x * y)) a
Tactic: rw [← cfc_comp _ _ 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 y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha : 0 ≤ a
⊢ cfc (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) ((fun (x : ℝ≥0) ↦ x ^ y) ∘ fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (x * y)) a
have refine : ∀ x_1 ∈ spectrum ℝ≥0 a, ((fun (x : ℝ≥0) ↦ x ^ y) ∘ fun (x_3 : ℝ≥0) ↦ x_3 ^ x) x_1 = x_1 ^ (x * y)
Tactic: refine cfc_congr fun _ _ => ?_
-- 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
x : ℝ
ha : IsStrictlyPositive a
⊢ a ^ x * a ^ (-x) = 1
have rw : a ^ (x + -x) = 1
Tactic: rw [← rpow_add ha.isUnit, add_neg_cancel, rpow_zero 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
x : ℝ
ha : IsStrictlyPositive a
rw : a ^ (x + -x) = 1
⊢ a ^ x * a ^ (-x) = 1
have rw₁ : HPow.hPow (β := ℝ) a 0 = 1
Tactic: rw [← rpow_add ha.isUnit, add_neg_cancel, rpow_zero 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
x : ℝ
ha : IsStrictlyPositive a
rw : a ^ (x + -x) = 1
rw₁ : HPow.hPow (β := ℝ) a 0 = 1
⊢ a ^ x * a ^ (-x) = 1
have rw₂ : Eq.{u_1 + 1} (α := A) 1 1
Tactic: rw [← rpow_add ha.isUnit, add_neg_cancel, rpow_zero 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
x : ℝ
ha : IsStrictlyPositive a
⊢ a ^ (-x) * a ^ x = 1
have rw : a ^ (-x + x) = 1
Tactic: rw [← rpow_add ha.isUnit, neg_add_cancel, rpow_zero 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
x : ℝ
ha : IsStrictlyPositive a
rw : a ^ (-x + x) = 1
⊢ a ^ (-x) * a ^ x = 1
have rw₁ : HPow.hPow (β := ℝ) a 0 = 1
Tactic: rw [← rpow_add ha.isUnit, neg_add_cancel, rpow_zero 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
x : ℝ
ha : IsStrictlyPositive a
rw : a ^ (-x + x) = 1
rw₁ : HPow.hPow (β := ℝ) a 0 = 1
⊢ a ^ (-x) * a ^ x = 1
have rw₂ : Eq.{u_1 + 1} (α := A) 1 1
Tactic: rw [← rpow_add ha.isUnit, neg_add_cancel, rpow_zero 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ˣ
ha : 0 ≤ (↑a : A)
⊢ HPow.hPow (β := ℝ) (↑a : A) (-1) = (↑a⁻¹ : A)
have refine : HPow.hPow (β := ℝ) (↑a : A) (-1) * (↑a : A) = 1
Tactic: refine a.inv_eq_of_mul_eq_one_left ?_ |>.symm
-- 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
⊢ Ring.inverse a = HPow.hPow (β := ℝ) a (-1)
have obtain : ∀ (ax : Aˣ) (hax : (↑ax : A) = a), Ring.inverse a = HPow.hPow (β := ℝ) a (-1)
Tactic: obtain ⟨ax, hax⟩ := ha.isUnit
-- 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 : ℝ
ha' : 0 ≤ (↑a : A)
h₁ : ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ x) (Inv.inv '' spectrum ℝ≥0 (↑a : A))
⊢ (↑a : A) ^ (-x) = (↑a⁻¹ : A) ^ x
have rw : cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (-x)) (↑a : A) =
  cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1⁻¹ ^ x) (↑a : A)
Tactic: rw [← cfc_inv_id (R := ℝ≥0) a, rpow_def, rpow_def,
        ← cfc_comp' (fun z => z ^ x) (Inv.inv : ℝ≥0 → ℝ≥0) (a : A) h₁]
-- 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 : ℝ
ha' : 0 ≤ (↑a : A)
h₁ : ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ x) (Inv.inv '' spectrum ℝ≥0 (↑a : A))
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ (-x)) (↑a : A) =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1⁻¹ ^ x) (↑a : A)
have refine : ∀ x_1 ∈ spectrum ℝ≥0 (↑a : A), x_1 ^ (-x) = x_1⁻¹ ^ x
Tactic: refine cfc_congr fun _ _ => ?_
-- 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 : ℝ
ha' : 0 ≤ (↑a : A)
⊢ (↑a : A) ^ (-x) = (↑a⁻¹ : A) ^ x
have suffices : ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ x) (Inv.inv '' spectrum ℝ≥0 (↑a : A))
Tactic: suffices h₁ : ContinuousOn (fun z ↦ z ^ x) (Inv.inv '' (spectrum ℝ≥0 (a : A))) by
    rw [← cfc_inv_id (R := ℝ≥0) a, rpow_def, rpow_def,
        ← cfc_comp' (fun z => z ^ x) (Inv.inv : ℝ≥0 → ℝ≥0) (a : A) h₁]
    refine cfc_congr fun _ _ => ?_
    simp [NNReal.rpow_neg, NNReal.inv_rpow]
-- 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 : ℝ
ha' : 0 ≤ (↑a : A)
⊢ ContinuousOn (Y := ℝ≥0) (fun (z : ℝ≥0) ↦ z ^ x) (Inv.inv '' spectrum ℝ≥0 (↑a : A))
have refine : 0 ∉ Inv.inv '' spectrum ℝ≥0 (↑a : A)
Tactic: refine NNReal.continuousOn_rpow_const (.inl ?_)
-- 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ˣ
n : ℤ
ha : 0 ≤ (↑a : A)
⊢ HPow.hPow (β := ℝ) (↑a : A) (↑n : ℝ) = (↑(a ^ n) : A)
have rw : cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑a : A) =
  cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ n) (↑a : A)
Tactic: rw [← cfc_zpow (R := ℝ≥0) a n, rpow_def]
-- 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ˣ
n : ℤ
ha : 0 ≤ (↑a : A)
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ HPow.hPow (β := ℝ) x (↑n : ℝ)) (↑a : A) =
    cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ n) (↑a : A)
have refine : ∀ x ∈ spectrum ℝ≥0 (↑a : A), HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ n
Tactic: refine cfc_congr fun _ _ => ?_
-- 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
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
⊢ IsUnit (a ^ y) ↔ IsUnit 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
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h : Nontrivial A
⊢ IsUnit (a ^ y) ↔ IsUnit a
have refine : ∀ (h : IsUnit (a ^ y)), IsUnit a
Tactic: refine ⟨fun h => ?_, fun h => h.cfcRpow y ha⟩
-- 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
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : IsUnit (a ^ y)
⊢ IsUnit a
have h₁ : IsUnit (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) a)
Tactic: rw [rpow_def] 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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : IsUnit (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) a)
⊢ IsUnit a
have pos : ∀ (hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)), IsUnit a
Tactic: by_cases hf : ContinuousOn (fun x : ℝ≥0 => x ^ y) (spectrum ℝ≥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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : IsUnit (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) a)
pos : ∀ (hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)), IsUnit a
⊢ IsUnit a
have neg : ∀ (hf : ¬ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)), IsUnit a
Tactic: by_cases hf : ContinuousOn (fun x : ℝ≥0 => x ^ y) (spectrum ℝ≥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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : IsUnit (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) a)
hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
⊢ IsUnit a
have h₁ : ∀ x ∈ spectrum ℝ≥0 a, x ^ y ≠ 0
Tactic: rw [isUnit_cfc_iff _ a hf] at h
Cleared hypotheses: h, hf
-- 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
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : ∀ x ∈ spectrum ℝ≥0 a, x ^ y ≠ 0
hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
⊢ IsUnit a
have pos : 0 ∉ spectrum ℝ≥0 a
Tactic: refine spectrum.isUnit_of_zero_notMem ℝ≥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
a : A
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : ∀ x ∈ spectrum ℝ≥0 a, x ^ y ≠ 0
hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
h0 : 0 ∈ spectrum ℝ≥0 a
⊢ False
have h₁ : HPow.hPow (α := ℝ≥0) 0 y ≠ 0
Tactic: specialize h 0 h0
Cleared hypotheses: 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
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
hf : ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
h0 : 0 ∈ spectrum ℝ≥0 a
h : HPow.hPow (α := ℝ≥0) 0 y ≠ 0
⊢ False
have h₁ : y = 0
Tactic: simp only [ne_eq, NNReal.rpow_eq_zero_iff, true_and, Decidable.not_not] at h
Cleared hypotheses: 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
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
h_1 : Nontrivial A
h : IsUnit (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x ^ y) a)
hf : ¬ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
⊢ IsUnit a
have h₁ : IsUnit.{u_1} (M := A) 0
Tactic: rw [cfc_apply_of_not_continuousOn a hf] at h
Cleared hypotheses: h, hf
-- 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
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
⊢ rpow (a, b) x = (a ^ x, b ^ x)
have ha'' : 0 ∉ spectrum ℝ≥0 a
Tactic: have ha'' : 0 ∉ spectrum ℝ≥0 a := spectrum.zero_notMem _ ha
-- 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
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
⊢ rpow (a, b) x = (a ^ x, b ^ x)
have hb'' : 0 ∉ spectrum ℝ≥0 b
Tactic: have hb'' : 0 ∉ spectrum ℝ≥0 b := spectrum.zero_notMem _ hb
-- 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
⊢ ContinuousOn (Y := ℝ≥0) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) (spectrum ℝ≥0 a ∪ spectrum ℝ≥0 b)
have funProp : 0 ∉ spectrum ℝ≥0 a ∪ spectrum ℝ≥0 b ∨ 0 ≤ x
Tactic: cfc_cont_tac
-- 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
⊢ cfc (p := fun (x : A × B) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) (a, b) =
    (cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) a,
      cfc (p := fun (x : B) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) b)
have refine : 0 ≤ (a, b)
Tactic: refine cfc_map_prod (R := ℝ≥0) (S := ℝ) _ a b (by cfc_cont_tac) ?_