Compfiles/Imo2000P2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2000, Problem 2

Let a, b, c be positive real numbers such that abc = 1. Show that

(a - 1 + 1/b)(b - 1 + 1/c)(c - 1 + 1/a) ≤ 1.

Imports (2)
Imported by 1 file
  1. lemma Imo2000P2.schur line 29 source

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

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

    Proof uses: Not, Or, Classical.em, Eq, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm and 62 more

    95 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

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

  2. lemma Imo2000P2.lemma1 line 55 source

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

    Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, HAdd.hAdd, Neg.neg, HSub.hSub

    Proof uses: le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HPow.hPow, Nat, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, Eq and 53 more

    71 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. lemma Imo2000P2.lemma2 line 59 source

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

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

    Proof uses: Exists.intro, And.intro, zero_lt_one, Iff.mpr, one_div_pos, Eq.symm, div_one, one_div_one_div, Eq.mpr, inferInstance, CommGroupWithZero, id, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, Neg.neg, List.nil, Prod and 80 more

    105 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  4. problem Imo2000P2.imo2000_p2 line 71 source

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

    Statement uses: Real, LT.lt, OfNat.ofNat, Eq, HMul.hMul, LE.le, HAdd.hAdd, HSub.hSub, HDiv.hDiv

    Proof uses: Exists, And, Imo2000P2.lemma2, Neg.neg, Imo2000P2.lemma1, mul_pos, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne and 87 more

    104 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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