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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
y : ℝ≥0
ha : 0 ≤ a
inl : HPow.hPow (β := ℝ≥0) (HPow.hPow (β := ℝ≥0) a 0) 0 = a ^ HMul.hMul (α := ℝ≥0) 0 0
⊢ HPow.hPow (β := ℝ≥0) a 0 ^ y = a ^ (0 * y)
have inl₁ : ∀ (hy : 0 < y), HPow.hPow (β := ℝ≥0) a 0 ^ y = a ^ (0 * y)
Tactic: obtain (rfl | hy) := eq_zero_or_pos y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
x y : ℝ≥0
ha : 0 ≤ a
hx : 0 < x
⊢ (a ^ x) ^ y = a ^ (x * y)
have inr : HPow.hPow (β := ℝ≥0) (a ^ x) 0 = a ^ (x * 0)
Tactic: obtain (rfl | hy) := eq_zero_or_pos y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
x y : ℝ≥0
ha : 0 ≤ a
hx : 0 < x
inr : HPow.hPow (β := ℝ≥0) (a ^ x) 0 = a ^ (x * 0)
⊢ (a ^ x) ^ y = a ^ (x * y)
have inr₁ : ∀ (hy : 0 < y), (a ^ x) ^ y = a ^ (x * y)
Tactic: obtain (rfl | hy) := eq_zero_or_pos y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
x y : ℝ≥0
ha : 0 ≤ a
hx : 0 < x
hy : 0 < y
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow y)
      (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.nnrpow (x * y)) a
have inr : cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) ((fun (x : ℝ≥0) ↦ x.nnrpow y) ∘ fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a =
  cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow (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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
x y : ℝ≥0
ha : 0 ≤ a
hx : 0 < x
hy : 0 < y
⊢ cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) ((fun (x : ℝ≥0) ↦ x.nnrpow y) ∘ fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a =
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow (x * y)) a
have inr : ∀ (u : ℝ≥0), ((fun (x : ℝ≥0) ↦ x.nnrpow y) ∘ fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) u = u.nnrpow (x * y)
Tactic: congr! 2 with u
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
x y : ℝ≥0
ha : 0 ≤ a
hx : 0 < x
hy : 0 < y
u : ℝ≥0
⊢ ((fun (x : ℝ≥0) ↦ x.nnrpow y) ∘ fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) u = u.nnrpow (x * y)
have inr : (↑(((fun (x : ℝ≥0) ↦ x.nnrpow y) ∘ fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) u) : ℝ) = (↑(u.nnrpow (x * y)) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
B : Type u_2
inst_12 : PartialOrder B
inst_13 : NonUnitalRing B
inst_14 : TopologicalSpace B
inst_15 : StarRing B
inst_16 : Module ℝ B
inst_17 : SMulCommClass ℝ B B
inst_18 : IsScalarTower ℝ B B
inst_19 : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst_20 : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst_21 : IsSemitopologicalRing B
inst_22 : T2Space B
inst_23 : NonnegSpectrumClass ℝ B
inst_24 : NonnegSpectrumClass ℝ (A × B)
inst_25 : StarOrderedRing B
a : A
b : B
x : ℝ≥0
ha : 0 ≤ a
hb : 0 ≤ b
⊢ ContinuousOn (Y := ℝ≥0) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) (quasispectrum ℝ≥0 a ∪ quasispectrum ℝ≥0 b)
have funProp : 0 ∉ quasispectrum ℝ≥0 a ∪ quasispectrum ℝ≥0 b ∨ 0 ≤ (↑x : ℝ)
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
B : Type u_2
inst_12 : PartialOrder B
inst_13 : NonUnitalRing B
inst_14 : TopologicalSpace B
inst_15 : StarRing B
inst_16 : Module ℝ B
inst_17 : SMulCommClass ℝ B B
inst_18 : IsScalarTower ℝ B B
inst_19 : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst_20 : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst_21 : IsSemitopologicalRing B
inst_22 : T2Space B
inst_23 : NonnegSpectrumClass ℝ B
inst_24 : NonnegSpectrumClass ℝ (A × B)
inst_25 : StarOrderedRing B
a : A
b : B
x : ℝ≥0
ha : 0 ≤ a
hb : 0 ≤ b
⊢ cfcₙ (p := fun (x : A × B) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) (a, b) =
    (cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) a,
      cfcₙ (p := fun (x : B) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) b)
have refine : 0 ≤ (a, b)
Tactic: refine cfcₙ_map_prod (S := ℝ) _ a b (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
B : Type u_2
inst_12 : PartialOrder B
inst_13 : NonUnitalRing B
inst_14 : TopologicalSpace B
inst_15 : StarRing B
inst_16 : Module ℝ B
inst_17 : SMulCommClass ℝ B B
inst_18 : IsScalarTower ℝ B B
inst_19 : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst_20 : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst_21 : IsSemitopologicalRing B
inst_22 : T2Space B
inst_23 : NonnegSpectrumClass ℝ B
inst_24 : NonnegSpectrumClass ℝ (A × B)
inst_25 : StarOrderedRing B
a : A
b : B
x : ℝ≥0
ha : 0 ≤ a
hb : 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
B : Type u_2
inst_12 : PartialOrder B
inst_13 : NonUnitalRing B
inst_14 : TopologicalSpace B
inst_15 : StarRing B
inst_16 : Module ℝ B
inst_17 : SMulCommClass ℝ B B
inst_18 : IsScalarTower ℝ B B
inst_19 : NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst_20 : NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst_21 : IsSemitopologicalRing B
inst_22 : T2Space B
inst_23 : NonnegSpectrumClass ℝ B
inst_24 : NonnegSpectrumClass ℝ (A × B)
inst_25 : StarOrderedRing B
a : A
b : B
x : ℝ≥0
ha : 0 ≤ a
hb : 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 (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a : A
⊢ cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) a = a ^ (1 / 2)
have e_f : Eq (α := ℝ≥0 → ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x.nnrpow (1 / 2)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
a : A
⊢ Eq (α := ℝ≥0 → ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x.nnrpow (1 / 2)
have e_f : ∀ (x : ℝ≥0), (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑(x.nnrpow (1 / 2)) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
x : ℝ≥0
⊢ sqrt a ^ x = a ^ (x / 2)
have rw : (a ^ (1 / 2)) ^ x = a ^ (x / 2)
Tactic: rw [sqrt_eq_nnrpow, nnrpow_nnrpow, one_div_mul_eq_div 2 x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
x : ℝ≥0
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_nnrpow, nnrpow_nnrpow, one_div_mul_eq_div 2 x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
x : ℝ≥0
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_nnrpow, nnrpow_nnrpow, one_div_mul_eq_div 2 x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
⊢ HPow.hPow (β := ℝ≥0) (sqrt a) 2 = a
have simp : HPow.hPow (β := ℝ≥0) a 1 = a
Tactic: simp only [nnrpow_sqrt, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, div_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
⊢ HPow.hPow (β := ℝ≥0) a 1 = a
have rw : a = a
Tactic: rw [nnrpow_one a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt a * sqrt a = a
have rw : HPow.hPow (β := ℝ≥0) (sqrt a) 2 = a
Tactic: rw [← nnrpow_two _, nnrpow_sqrt_two _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
rw : HPow.hPow (β := ℝ≥0) (sqrt a) 2 = a
⊢ sqrt a * sqrt a = a
have rw₁ : a = a
Tactic: rw [← nnrpow_two _, nnrpow_sqrt_two _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt (HPow.hPow (β := ℝ≥0) a 2) = a
have simp : HPow.hPow (β := ℝ≥0) a 1 = a
Tactic: simp only [sqrt_nnrpow, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, div_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
⊢ HPow.hPow (β := ℝ≥0) a 1 = a
have rw : a = a
Tactic: rw [nnrpow_one _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt (a * a) = a
have rw : sqrt (HPow.hPow (β := ℝ≥0) a 2) = a
Tactic: rw [← nnrpow_two _, sqrt_nnrpow_two _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
rw : sqrt (HPow.hPow (β := ℝ≥0) a 2) = a
⊢ sqrt (a * a) = a
have rw₁ : a = a
Tactic: rw [← nnrpow_two _, sqrt_nnrpow_two _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt a = 0 ↔ a = 0
have rw : HMul.hMul (α := A) 0 0 = a ↔ a = 0
Tactic: rw [sqrt_eq_iff a _, mul_zero, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
rw : HMul.hMul (α := A) 0 0 = a ↔ a = 0
⊢ sqrt a = 0 ↔ a = 0
have rw₁ : 0 = a ↔ a = 0
Tactic: rw [sqrt_eq_iff a _, mul_zero, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
rw : HMul.hMul (α := A) 0 0 = a ↔ a = 0
rw₁ : 0 = a ↔ a = 0
⊢ sqrt a = 0 ↔ a = 0
have rw₂ : a = 0 ↔ a = 0
Tactic: rw [sqrt_eq_iff a _, mul_zero, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic (goal)
Goal:
A : Type u_1
inst : PartialOrder A
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
this : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a
⊢ sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
have rwa : ∀
  (this :
    cfcₙ (p := IsSelfAdjoint) Real.sqrt a * cfcₙ (p := IsSelfAdjoint) Real.sqrt a =
      cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a),
  sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
Tactic: rwa [cfcₙ_mul .., cfcₙ_id' ..,
      ← sqrt_eq_iff _ (hb := cfcₙ_nonneg (fun x _ ↦ Real.sqrt_nonneg x))] 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
this : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a
rwa :
  ∀
    (this :
      cfcₙ (p := IsSelfAdjoint) Real.sqrt a * cfcₙ (p := IsSelfAdjoint) Real.sqrt a =
        cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a),
    sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
⊢ sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
have rwa₁ : ∀ (this : cfcₙ (p := IsSelfAdjoint) Real.sqrt a * cfcₙ (p := IsSelfAdjoint) Real.sqrt a = a),
  sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
Tactic: rwa [cfcₙ_mul .., cfcₙ_id' ..,
      ← sqrt_eq_iff _ (hb := cfcₙ_nonneg (fun x _ ↦ Real.sqrt_nonneg x))] 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
this : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a
rwa :
  ∀
    (this :
      cfcₙ (p := IsSelfAdjoint) Real.sqrt a * cfcₙ (p := IsSelfAdjoint) Real.sqrt a =
        cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a),
    sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
rwa₁ :
  ∀ (this : cfcₙ (p := IsSelfAdjoint) Real.sqrt a * cfcₙ (p := IsSelfAdjoint) Real.sqrt a = a),
    sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
⊢ sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
have rwa₂ : ∀ (this : sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a), sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
Tactic: rwa [cfcₙ_mul .., cfcₙ_id' ..,
      ← sqrt_eq_iff _ (hb := cfcₙ_nonneg (fun x _ ↦ Real.sqrt_nonneg x))] 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 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : SMulCommClass ℝ A A
inst_6 : IsScalarTower ℝ A A
inst_7 : StarOrderedRing A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsSemitopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt a = cfcₙ (p := IsSelfAdjoint) Real.sqrt a
have suffices : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √x * √x) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) a
Tactic: suffices cfcₙ (fun x : ℝ ↦ √x * √x) a = cfcₙ (fun x : ℝ ↦ x) a by
    rwa [cfcₙ_mul .., cfcₙ_id' ..,
      ← sqrt_eq_iff _ (hb := cfcₙ_nonneg (fun x _ ↦ Real.sqrt_nonneg x))] at this