Compfiles/Singapore2019P11.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Singapore Math Olympiad (Senior) 2019 (Round 1), Problem 11

http://www.realsutra.com/limjeck/SMO_Senior_2019.pdf

Find the value of 448 * (sin 12 degrees) * (sin 39 degrees) * (sin 51 degrees) / sin 24 degrees

Imports (2)
Imported by 1 file
  1. determine Singapore2019R1P11.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 Singapore2019R1P11.singapore2019_r1_p11 line 27 source

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

    Statement uses: Eq, Real, HDiv.hDiv, HMul.hMul, OfNat.ofNat, Nat, Real.sin, Real.pi, Singapore2019R1P11.solution

    Proof uses: Eq.mpr, Real.cos, id, congrArg, HSub.hSub, Eq.symm, Real.sin_pi_div_two_sub, Eq.rec, Eq.refl, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast, NNRat.rawCast, Mathlib.Tactic.Ring.Common.div_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.atom_pf and 145 more

    125 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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