Compfiles/Imo1972P4.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1972, Problem 4

Find all positive real solutions to:

(x_1^2 - x_3x_5)(x_2^2 - x_3x_5) ≤ 0 (x_2^2 - x_4x_1)(x_3^2 - x_4x_1) ≤ 0 (x_3^2 - x_5x_2)(x_4^2 - x_5x_2) ≤ 0 (x_4^2 - x_1x_3)(x_5^2 - x_1x_3) ≤ 0 (x_5^2 - x_2x_4)(x_1^2 - x_2x_4) ≤ 0

Imports (3)
Imported by 1 file
  1. determine Imo1972P4.solution_set line 32 source

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

    Statement uses: Set, Prod, Real

    Proof uses: Set.ofPred, Imo1972P4.solution_set.match_1, And, Eq

  2. problem Imo1972P4.imo1972_p4 line 35 source

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

    Statement uses: Real, And, LT.lt, OfNat.ofNat, Iff, LE.le, HMul.hMul, HSub.hSub, HPow.hPow, Nat, Membership.mem, Prod, Set, Imo1972P4.solution_set, Prod.mk

    Proof uses: Eq.mpr, Set.ofPred, Imo1972P4.solution_set.match_1, Eq, id, congrArg, Imo1972P4.solution_set.eq_1, Iff.intro, HAdd.hAdd, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne and 77 more

    91 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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