Compfiles/Singapore2019P7.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

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}$.

Imports (2)
Imported by 1 file
  1. determine Singapore2019R1P7.solution line 25 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real

    Proof uses: OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

  2. problem Singapore2019R1P7.singapore2019_r1_p7 line 27 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Eq, Real.tan, OfNat.ofNat, Nat, HDiv.hDiv, HAdd.hAdd, Real.sin, HMul.hMul, Real.cos, Singapore2019R1P7.solution

    Proof uses: Ne, id, Eq.mpr, congrArg, Real.tan_eq_sin_div_cos, of_eq_true, Eq.trans, True, congrFun', div_zero, eq_self, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 116 more

    112 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

    Open to load the checked before-and-after goal states.