import Mathlib
/-!
# Singapore Math Olympiad (Senior) 2019 (Round 1), Problem 4
http://www.realsutra.com/limjeck/SMO_Senior_2019.pdf
If $\log_{21} 3 = x$, express $\log_7 9$ in terms of $x$.
-/
open Real
namespace Singapore2019R1P4
noncomputable /- determine -/ abbrev solution (x : ℝ) : ℝ := sorry
theorem singapore2019_r1_p4 (x : ℝ) (hx : Real.logb 21 3 = x) :
Real.logb 7 9 = solution x := sorry
This problem has a complete formalized solution.