awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
case pos =>
    obtain (rfl | hx) := eq_zero_or_pos x <;> obtain (rfl | hy) := eq_zero_or_pos y
    all_goals try simp
    simp only [nnrpow_def]
    rw [← cfcₙ_comp _ _ a]
    congr! 2 with u
    ext
    simp [Real.rpow_mul]

Premises used: cfcₙ_comp, CFC.nnrpow_def, eq_zero_or_pos, Real.rpow_mul, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
simp [nnrpow_def, cfcₙ_apply_of_not_predicate a ha]

Premises used: CFC.nnrpow_def, cfcₙ_apply_of_not_predicate
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
case neg =>
    simp [nnrpow_def, cfcₙ_apply_of_not_predicate a ha]

Premises used: CFC.nnrpow_def, cfcₙ_apply_of_not_predicate
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
hx : x ≠ 0
ha : 0 ≤ a
⊢ (a ^ x) ^ x⁻¹ = a

Tactic:
simp [mul_inv_cancel₀ hx, nnrpow_one _ ha]

Premises used: mul_inv_cancel₀, CFC.nnrpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
hx : x ≠ 0
ha : 0 ≤ a
⊢ (a ^ x⁻¹) ^ x = a

Tactic:
simp [inv_mul_cancel₀ hx, nnrpow_one _ ha]

Premises used: CFC.nnrpow_one, inv_mul_cancel₀
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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 b : A
x : ℝ≥0
hx : x ≠ 0
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ x⁻¹ = b ↔ b ^ x = a

Tactic:
⟨fun h ↦ nnrpow_inv_nnrpow a hx ▸ congr($(h) ^ x).symm,
    fun h ↦ nnrpow_nnrpow_inv b hx ▸ congr($(h) ^ x⁻¹).symm⟩

Premises used: congrArg, Eq.rec, CFC.nnrpow_inv_nnrpow, id, Inv.inv, HPow.hPow, Iff.intro, CFC.nnrpow_nnrpow_inv, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
funProp funProp₁ : 0 ∉ quasispectrum ℝ≥0 a ∪ quasispectrum ℝ≥0 b ∨ 0 ≤ (↑x : ℝ)
⊢ ContinuousOn (Y := ℝ≥0) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) (quasispectrum ℝ≥0 a ∪ quasispectrum ℝ≥0 b)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
refine : 0 ≤ (a, 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)

Tactic:
refine cfcₙ_map_prod (S := ℝ) _ a b (by fun_prop) ?_

Premises used: cfcₙ_map_prod
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
right : 0.2 ≤ (a, b).2
⊢ 0.1 ≤ (a, b).1 ∧ 0.2 ≤ (a, b).2

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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

Tactic:
simp [ha, hb]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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.2 ≤ (a, b).2

Tactic:
simp [ha, hb]
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ nnrpow (a, b) x = (a, b) ^ x

Tactic:
nnrpow_map_prod

Premises used: CFC.nnrpow_map_prod
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
ι : Type u_2
C : ι → Type u_3
inst : (i : ι) → PartialOrder (C i)
inst_1 : (i : ι) → NonUnitalRing (C i)
inst_2 : (i : ι) → TopologicalSpace (C i)
inst_3 : (i : ι) → StarRing (C i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_3} (C i)
inst_5 : StarOrderedRing ((i : ι) → C i)
inst_6 : (i : ι) → Module ℝ (C i)
inst_7 : ∀ (i : ι), SMulCommClass.{0, u_3, u_3} ℝ (C i) (C i)
inst_8 : ∀ (i : ι), IsScalarTower.{0, u_3, u_3} ℝ (C i) (C i)
inst_9 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus.{0, u_3} ℝ (C i) IsSelfAdjoint
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst_11 : ∀ (i : ι), IsSemitopologicalRing.{u_3} (C i)
inst_12 : ∀ (i : ι), T2Space.{u_3} (C i)
inst_13 : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst_14 : ∀ (i : ι), NonnegSpectrumClass.{0, u_3} ℝ (C i)
c : (i : ι) → C i
x : ℝ≥0
hc : ∀ (i : ι), 0 ≤ c i
⊢ cfcₙ (p := fun (x : (i : ι) → C i) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) c = fun (i : ι) ↦
    cfcₙ (p := fun (x : C i) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) (c i)

Tactic:
cfcₙ_map_pi (S := ℝ) _ c

Premises used: cfcₙ_map_pi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
ι : Type u_2
C : ι → Type u_3
inst : (i : ι) → PartialOrder (C i)
inst_1 : (i : ι) → NonUnitalRing (C i)
inst_2 : (i : ι) → TopologicalSpace (C i)
inst_3 : (i : ι) → StarRing (C i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_3} (C i)
inst_5 : StarOrderedRing ((i : ι) → C i)
inst_6 : (i : ι) → Module ℝ (C i)
inst_7 : ∀ (i : ι), SMulCommClass.{0, u_3, u_3} ℝ (C i) (C i)
inst_8 : ∀ (i : ι), IsScalarTower.{0, u_3, u_3} ℝ (C i) (C i)
inst_9 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus.{0, u_3} ℝ (C i) IsSelfAdjoint
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst_11 : ∀ (i : ι), IsSemitopologicalRing.{u_3} (C i)
inst_12 : ∀ (i : ι), T2Space.{u_3} (C i)
inst_13 : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst_14 : ∀ (i : ι), NonnegSpectrumClass.{0, u_3} ℝ (C i)
c : (i : ι) → C i
x : ℝ≥0
hc : ∀ (i : ι), 0 ≤ c i
⊢ cfcₙ (p := fun (x : (i : ι) → C i) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) c = fun (i : ι) ↦
    cfcₙ (p := fun (x : C i) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1.nnrpow x) (c i)

Tactic:
exact cfcₙ_map_pi (S := ℝ) _ c

Premises used: cfcₙ_map_pi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
Goal:
ι : Type u_2
C : ι → Type u_3
inst : (i : ι) → PartialOrder (C i)
inst_1 : (i : ι) → NonUnitalRing (C i)
inst_2 : (i : ι) → TopologicalSpace (C i)
inst_3 : (i : ι) → StarRing (C i)
inst_4 : ∀ (i : ι), StarOrderedRing.{u_3} (C i)
inst_5 : StarOrderedRing ((i : ι) → C i)
inst_6 : (i : ι) → Module ℝ (C i)
inst_7 : ∀ (i : ι), SMulCommClass.{0, u_3, u_3} ℝ (C i) (C i)
inst_8 : ∀ (i : ι), IsScalarTower.{0, u_3, u_3} ℝ (C i) (C i)
inst_9 : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus.{0, u_3} ℝ (C i) IsSelfAdjoint
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst_11 : ∀ (i : ι), IsSemitopologicalRing.{u_3} (C i)
inst_12 : ∀ (i : ι), T2Space.{u_3} (C i)
inst_13 : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst_14 : ∀ (i : ι), NonnegSpectrumClass.{0, u_3} ℝ (C i)
c : (i : ι) → C i
x : ℝ≥0
hc : ∀ (i : ι), 0 ≤ c i
⊢ nnrpow c x = c ^ x

Tactic:
nnrpow_map_pi

Premises used: CFC.nnrpow_map_pi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ 0 ≤ sqrt a

Tactic:
cfcₙ_predicate _ a

Premises used: CFC.sqrt, cfcₙ_predicate
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
e_f : Eq (α := ℝ≥0 → ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x.nnrpow (1 / 2)
⊢ cfcₙ (R := ℝ≥0) (p := fun (x : A) ↦ 0 ≤ x) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) a = a ^ (1 / 2)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
e_f : ∀ (x : ℝ≥0), (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑(x.nnrpow (1 / 2)) : ℝ)
⊢ Eq (α := ℝ≥0 → ℝ≥0) (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) fun (x : ℝ≥0) ↦ x.nnrpow (1 / 2)

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
x : ℝ≥0
⊢ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑(x.nnrpow (1 / 2)) : ℝ)

Tactic:
exact_mod_cast NNReal.sqrt_eq_rpow _

Premises used: NNReal.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
ha : ¬0 ≤ a
⊢ sqrt a = 0

Tactic:
cfcₙ_apply_of_not_predicate a ha

Premises used: CFC.sqrt, cfcₙ_apply_of_not_predicate
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ sqrt 0 = 0

Tactic:
simp [sqrt]

Premises used: CFC.sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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)
rw₂ rw₃ : a ^ (x / 2) = a ^ (x / 2)
⊢ sqrt a ^ x = a ^ (x / 2)

Tactic:
rw [sqrt_eq_nnrpow, nnrpow_nnrpow, one_div_mul_eq_div 2 x]

Premises used: CFC.sqrt_eq_nnrpow, CFC.nnrpow_nnrpow, one_div_mul_eq_div, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
simp : HPow.hPow (β := ℝ≥0) a 1 = a
⊢ HPow.hPow (β := ℝ≥0) (sqrt a) 2 = a

Tactic:
simp only [nnrpow_sqrt, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, div_self]

Premises used: OfNat.ofNat_ne_zero, ne_eq, CFC.nnrpow_sqrt, not_false_eq_true, div_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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 rw₁ : a = a
⊢ HPow.hPow (β := ℝ≥0) a 1 = a

Tactic:
rw [nnrpow_one a]

Premises used: CFC.nnrpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
rw₁ rw₂ : a = a
⊢ sqrt a * sqrt a = a

Tactic:
rw [← nnrpow_two _, nnrpow_sqrt_two _]

Premises used: CFC.nnrpow_sqrt_two, CFC.nnrpow_two
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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)

Tactic:
simp [sqrt_eq_nnrpow, div_eq_mul_inv]

Premises used: CFC.sqrt_eq_nnrpow, div_eq_mul_inv
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
simp : HPow.hPow (β := ℝ≥0) a 1 = a
⊢ sqrt (HPow.hPow (β := ℝ≥0) a 2) = a

Tactic:
simp only [sqrt_nnrpow, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, div_self]

Premises used: OfNat.ofNat_ne_zero, ne_eq, CFC.sqrt_nnrpow, not_false_eq_true, div_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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 rw₁ : a = a
⊢ HPow.hPow (β := ℝ≥0) a 1 = a

Tactic:
rw [nnrpow_one _]

Premises used: CFC.nnrpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
rw₁ rw₂ : a = a
⊢ sqrt (a * a) = a

Tactic:
rw [← nnrpow_two _, sqrt_nnrpow_two _]

Premises used: CFC.sqrt_nnrpow_two, CFC.nnrpow_two
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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 b : A
h : sqrt a = b
ha : 0 ≤ a
⊢ b * b = a

Tactic:
h ▸ sqrt_mul_sqrt_self _ ha

Premises used: Eq.rec, CFC.sqrt_mul_sqrt_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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 b : A
h : b * b = a
hb : 0 ≤ b
⊢ sqrt a = b

Tactic:
h ▸ sqrt_mul_self b

Premises used: Eq.rec, CFC.sqrt_mul_self