import Mathlib
/-!
# Singapore Math Olympiad (Senior) 2019 (Round 1), Problem 7
http://www.realsutra.com/limjeck/SMO_Senior_2019.pdf
Suppose that $\tan x = 5$. Find the value of $\frac{6 + \sin 2x}{1 + \cos 2x}$.
-/
open Real
namespace Singapore2019R1P7
noncomputable /- determine -/ abbrev solution : ℝ := sorry
theorem singapore2019_r1_p7 (x : ℝ) (hx : tan x = 5) :
(6 + sin (2 * x)) / (1 + cos (2 * x)) = solution := sorry
This problem has a complete formalized solution.