z x✝ y x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = x ^ (1 / 2 * r)
z x✝ y x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = sqrt x ^ r
rw [sqrt_eq_rpow, ← rpow_mul hx]
case e_a
z x✝ y x r : ℝ
hx : 0 ≤ x
⊢ r / 2 = 1 / 2 * r
z x✝ y x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = x ^ (1 / 2 * r)
congr
no goals
case e_a
z x✝ y x r : ℝ
hx : 0 ≤ x
⊢ r / 2 = 1 / 2 * r
ring