Compfiles/Singapore2019P2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

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

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

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

    Statement uses: Real

    Proof uses: HAdd.hAdd, OfNat.ofNat, HMul.hMul, Real.sqrt

    9 instances, coercions and auxiliary constants left out.

  2. problem Singapore2019R1P2.singapore2019_r1_p2 line 27 source

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

    Statement uses: Eq, Real, HMul.hMul, HPow.hPow, HSub.hSub, Real.sqrt, OfNat.ofNat, Nat, HDiv.hDiv, HAdd.hAdd, Singapore2019R1P2.solution

    Proof uses: Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAtLeastTwo, congr, Mathlib.Meta.NormNum.IsNNRat.to_eq, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNNRat_inv_pos, Nat.mul, Mathlib.Meta.NormNum.isNNRat_add, Nat.cast_one, eq_self and 97 more

    110 instances, coercions and auxiliary constants left out.

    Tactic trace: 38 steps

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