Compfiles/Imo2008P2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2008, Problem 2

(a) Prove that x^2 / (x-1)^2 + y^2 / (y-1)^2 + z^2 / (z-1)^2 ≥ 1 for all real numbers x,y, z, each different from 1, and satisfying xyz = 1.

(b) Prove that equality holds above for infinitely many triples of rational numbers x, y, z, each different from 1, and satisfying xyz = 1.

Imports (7)
Imported by 1 file
  1. theorem Imo2008P2.subst_abc line 51 source

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

    Statement uses: Real, Eq, HMul.hMul, OfNat.ofNat, Exists, And, Ne, HDiv.hDiv

    Proof uses: Exists.intro, Eq.rec, one_ne_zero, Eq.symm, id, Eq.mp, Not, Eq.trans, Or, congrArg, congrFun', Eq.mpr, congr, Lean.Data.AC.Context.eq_of_norm, Lean.Data.AC.Context.mk, Option.some, PLift, Std.Commutative, PLift.up, Option.none and 54 more

    79 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  2. problem Imo2008P2.imo2008_p2a line 62 source

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

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

    Proof uses: Exists, And, Imo2008P2.subst_abc, Exists.intro, of_eq_true, Eq.trans, True, congr, congrArg, sub_sub_cancel, eq_self, congrFun', and_self, Mathlib.Tactic.Contrapose.contrapose₄, Eq.mpr, id, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk and 129 more

    133 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

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

  3. def Imo2008P2.rationalSolutions line 74 source

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

    Statement uses: Set, Prod, Rat

    Proof uses: Set.ofPred, Exists, And, Eq, Prod.mk, Ne, OfNat.ofNat, HMul.hMul, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Nat, HSub.hSub

    14 instances, coercions and auxiliary constants left out.

  4. problem Imo2008P2.imo2008_p2b line 78 source

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

    Statement uses: Set.Infinite, Prod, Rat, Imo2008P2.rationalSolutions

    Proof uses: Set, Set.ofPred, Exists, And, Eq, Prod.mk, GT.gt, OfNat.ofNat, HDiv.hDiv, Neg.neg, HAdd.hAdd, HPow.hPow, Nat, HMul.hMul, LE.le, Membership.mem, Eq.mpr, Ne, HSub.hSub, id and 157 more

    137 instances, coercions and auxiliary constants left out.

    Tactic trace: 83 steps

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