import Mathlib
/-!
# Singapore Math Olympiad (Senior) 2019 (Round 1), Problem 2
http://www.realsutra.com/limjeck/SMO_Senior_2019.pdf
Simplify $(sqrt{10} - sqrt{2})^{1/3} * (sqrt{10} + sqrt{2})^{7/3}$.
-/
open Real
namespace Singapore2019R1P2
noncomputable /- determine -/ abbrev solution : ℝ := sorry
theorem singapore2019_r1_p2 : (√10 - √2)^(1 / 3 : ℝ) * (√10 + √2)^(7 / 3 : ℝ) = solution := sorry
This problem has a complete formalized solution.