Compfiles/Imo1962P2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1962, Problem 2

Determine all real numbers x which satisfy

√(3 - x) - √(x + 1) > 1/2.

Imports (2)
Imported by 1 file
  1. lemma Imo1962P2.lemma1 line 29 source

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

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

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. lemma Imo1962P2.lemma2 line 34 source

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

    Statement uses: Real, LE.le, OfNat.ofNat, HSub.hSub, Nat, HAdd.hAdd, Eq, HPow.hPow, Real.sqrt, HMul.hMul

    Proof uses: Trans.trans, sub_sq, Eq.mpr, id, congrArg, Real.sq_sqrt, propext, add_left_cancel_iff, Eq.refl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo and 36 more

    79 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  3. determine Imo1962P2.SolutionSet line 47 source

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

    Statement uses: Set, Real

    Proof uses: Set.Ico, Neg.neg, OfNat.ofNat, HSub.hSub, HDiv.hDiv, Real.sqrt

    13 instances, coercions and auxiliary constants left out.

  4. problem Imo1962P2.imo1962_p2 line 49 source

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

    Statement uses: Real, Iff, Membership.mem, Set, Imo1962P2.SolutionSet, And, LE.le, OfNat.ofNat, Nat, Neg.neg, LT.lt, HDiv.hDiv, HSub.hSub, Real.sqrt, HAdd.hAdd

    Proof uses: Eq.mpr, id, Eq, congrArg, Set.Ico, propext, Set.mem_Ico, Iff.intro, div_pos, Real.sqrt_pos_of_pos, Mathlib.Meta.Positivity.pos_of_isNat, inferInstance, PartialOrder, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl and 116 more

    158 instances, coercions and auxiliary constants left out.

    Tactic trace: 59 steps

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