Theorem: Iran1998P3.cube_root_cube (Compfiles/Iran1998P3.lean)

State before:
x : ℝ
h : 0 ≤ x
⊢ (x ^ 3) ^ (1 / 3) = x
Tactic:
rw [←Real.rpow_mul h, mul_div_cancel₀ (1 : ℝ) three_ne_zero]
State after:
x : ℝ
h : 0 ≤ x
⊢ x ^ 1 = x

State before:
x : ℝ
h : 0 ≤ x
⊢ x ^ 1 = x
Tactic:
exact Real.rpow_one x
State after:
no goals