Compfiles/Imo1965P1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1965, Problem 1

Determine all values x in the interval 0 ≤ x ≤ 2π which satisfy the inequality

2 cos x ≤ |√(1 + sin 2x) − √(1 − sin 2x)| ≤ √2.

Imports (2)
Imported by 1 file
  1. determine Imo1965P1.the_answer line 30 source

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

    Statement uses: Set, Real

    Proof uses: Set.Icc, HDiv.hDiv, Real.pi, OfNat.ofNat, HMul.hMul

    10 instances, coercions and auxiliary constants left out.

  2. problem Imo1965P1.imo1965_p1 line 32 source

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

    Statement uses: Eq, Set, Real, Set.ofPred, And, Membership.mem, Set.Icc, OfNat.ofNat, HMul.hMul, Nat, Real.pi, Real.cos, Real.sqrt, abs, HSub.hSub, HAdd.hAdd, Real.sin, Imo1965P1.the_answer

    Proof uses: HPow.hPow, Eq.mpr, id, congrArg, Eq.symm, Real.sqrt_sq_eq_abs, Real.cos_sq', sub_sq, Real.sq_sqrt, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring and 162 more

    169 instances, coercions and auxiliary constants left out.

    Tactic trace: 106 steps

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