Theorem: Real.pow_half_two (CvxLean/Lib/Math/Data/Real.lean)

State before:
x : ℝ
hx : 0 ≤ x
⊢ (x ^ (1 / 2)) ^ 2 = x
Tactic:
show rpow (rpow _ _) _ = _
State after:
x : ℝ
hx : 0 ≤ x
⊢ (x.rpow (1 / 2)).rpow 2 = x

State before:
x : ℝ
hx : 0 ≤ x
⊢ (x.rpow (1 / 2)).rpow 2 = x
Tactic:
rw [rpow_eq_pow, rpow_eq_pow, ← rpow_mul hx]
State after:
x : ℝ
hx : 0 ≤ x
⊢ x ^ (1 / 2 * 2) = x

State before:
x : ℝ
hx : 0 ≤ x
⊢ x ^ (1 / 2 * 2) = x
Tactic:
norm_num
State after:
no goals