-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_sqrt_nnreal {a : A} {x : ℝ≥0}
    (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : ¬x = 0
h₁ : 0 ≤ ↑x
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Tactic:
rw [sqrt_eq_rpow, rpow_rpow_of_exponent_nonneg _ _ _ (by norm_num) h₁, one_div_mul_eq_div]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : x = 0
ha' : 0 ≤ sqrt a
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Tactic:
simp [hx, rpow_zero _ ha', rpow_zero _ ha]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : ¬x = 0
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Tactic:
have h₁ : 0 ≤ (x : ℝ) := by exact NNReal.zero_le_coe

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : ¬x = 0
h₁ : 0 ≤ ↑x
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : x = 0
⊢ 0 ≤ sqrt a

Tactic:
exact sqrt_nonneg

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : ¬x = 0
h₁ : 0 ≤ ↑x
⊢ 0 ≤ 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
case neg
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : ¬x = 0
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Tactic:
case neg =>
  have h₁ : 0 ≤ (x : ℝ) := by exact NNReal.zero_le_coe
  rw [sqrt_eq_rpow, rpow_rpow_of_exponent_nonneg _ _ _ (by norm_num) h₁, one_div_mul_eq_div]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : x = 0
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Tactic:
have ha' : 0 ≤ sqrt a := by exact sqrt_nonneg

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : x = 0
ha' : 0 ≤ sqrt a
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Proof state:
case pos
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : x = 0
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

case neg
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : ¬x = 0
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Tactic:
case pos =>
  have ha' : 0 ≤ sqrt a := by exact sqrt_nonneg
  simp [hx, rpow_zero _ ha', rpow_zero _ ha]

Result:
case neg
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : ¬x = 0
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Tactic:
by_cases hx : x = 0

Result:
case pos
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : x = 0
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

case neg
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : ¬x = 0
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
hx : ¬x = 0
⊢ 0 ≤ ↑x

Tactic:
exact NNReal.zero_le_coe

Result:
no goals