awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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 : y = 0
⊢ False

Tactic:
exact hy h
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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.{u_1} (M := A) 0

Tactic:
rw [cfc_apply_of_not_continuousOn a hf] at h

Premises used: cfc_apply_of_not_continuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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)
h₁ : IsUnit.{u_1} (M := A) 0
⊢ ¬ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)

Tactic:
rw [cfc_apply_of_not_continuousOn a hf] at h

Premises used: cfc_apply_of_not_continuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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.{u_1} (M := A) 0
hf : ¬ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
⊢ IsUnit a

Tactic:
False.elim <| not_isUnit_zero h

Premises used: False.elim, not_isUnit_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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.{u_1} (M := A) 0
hf : ¬ContinuousOn (Y := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) (spectrum ℝ≥0 a)
⊢ IsUnit a

Tactic:
exact False.elim <| not_isUnit_zero h

Premises used: False.elim, not_isUnit_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ 0 ∉ spectrum ℝ≥0 a

Tactic:
have ha'' : 0 ∉ spectrum ℝ≥0 a := spectrum.zero_notMem _ ha
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ 0 ∉ spectrum ℝ≥0 b

Tactic:
have hb'' : 0 ∉ spectrum ℝ≥0 b := spectrum.zero_notMem _ hb
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
funProp : 0 ∉ spectrum ℝ≥0 a ∪ spectrum ℝ≥0 b ∨ 0 ≤ x
⊢ ContinuousOn (Y := ℝ≥0) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) (spectrum ℝ≥0 a ∪ spectrum ℝ≥0 b)

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

Tactic:
refine cfc_map_prod (R := ℝ≥0) (S := ℝ) _ a b (by cfc_cont_tac) ?_

Premises used: cfc_map_prod
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
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 : 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

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

Tactic:
rpow_map_prod ha hb

Premises used: CFC.rpow_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 : ι) → 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
⊢ ∀ (i : ι), 0 ∉ spectrum ℝ≥0 (c i)

Tactic:
have hc'' : ∀ i, 0 ∉ spectrum ℝ≥0 (c i) := fun i => spectrum.zero_notMem _ (hc i)
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
hc'' : ∀ (i : ι), 0 ∉ spectrum ℝ≥0 (c i)
⊢ cfc (p := fun (x : (i : ι) → C i) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) c = fun (i : ι) ↦
    cfc (p := fun (x : C i) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) (c i)

Tactic:
cfc_map_pi (S := ℝ) _ c

Premises used: Pi.ringHom, 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 : ι) → 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
hc'' : ∀ (i : ι), 0 ∉ spectrum ℝ≥0 (c i)
⊢ cfc (p := fun (x : (i : ι) → C i) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ x) c = fun (i : ι) ↦
    cfc (p := fun (x : C i) ↦ 0 ≤ x) (fun (x_1 : ℝ≥0) ↦ x_1 ^ 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 : ι) → 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 = c ^ x

Tactic:
rpow_map_pi hc

Premises used: CFC.rpow_map_pi
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
rw₂ 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 : ℝ)

Tactic:
rw [nnrpow_def (A := A), rpow_def, cfcₙ_eq_cfc]

Premises used: CFC.rpow_def, cfcₙ_eq_cfc, CFC.nnrpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ a ^ (1 / 2) = a ^ (↑(1 / 2) : ℝ)

Tactic:
have : a ^ (1 / 2 : ℝ) = a ^ ((1 / 2 : ℝ≥0) : ℝ) := rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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) : ℝ)
⊢ 0 < 1 / 2

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

Tactic:
rw [this, ← nnrpow_eq_rpow (by simp), sqrt_eq_nnrpow a]

Premises used: CFC.sqrt_eq_nnrpow, CFC.nnrpow_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
rw 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
⊢ 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]

Premises used: cfcₙ_eq_cfc
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
rw₁ rw₂ : a = a
⊢ sqrt (HPow.hPow (β := ℕ) a 2) = a

Tactic:
rw [pow_two, sqrt_mul_self (A := A) a]

Premises used: pow_two, CFC.sqrt_mul_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
rw₁ rw₂ : a = a
⊢ HPow.hPow (β := ℕ) (sqrt a) 2 = a

Tactic:
rw [pow_two, sqrt_mul_sqrt_self (A := A) a]

Premises used: pow_two, CFC.sqrt_mul_sqrt_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
simp_rw : a * a = b * b ↔ a = b
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b

Tactic:
simp_rw [sq, mul_self_eq_mul_self_iff a b]

Premises used: sq, CFC.mul_self_eq_mul_self_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [sqrt_eq_cfc, cfc_algebraMap]

Premises used: CFC.sqrt_eq_cfc, cfc_algebraMap
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ Eq.{u_1 + 1} (α := A) (sqrt 1) 1

Tactic:
simp [sqrt_eq_cfc]

Premises used: CFC.sqrt_eq_cfc
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
rw₂ rw₃ : a = 1 ↔ a = 1
⊢ sqrt a = 1 ↔ a = 1

Tactic:
rw [sqrt_eq_iff a _, mul_one, eq_comm]

Premises used: CFC.sqrt_eq_iff, eq_comm, mul_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
subst : Eq.{u_1 + 1} (α := A) (sqrt 1) 1
⊢ sqrt a = 1

Tactic:
subst h
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ Eq.{u_1 + 1} (α := A) (sqrt 1) 1

Tactic:
sqrt_one

Premises used: CFC.sqrt_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
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
⊢ Eq.{u_1 + 1} (α := A) (sqrt 1) 1

Tactic:
exact sqrt_one

Premises used: CFC.sqrt_one