Compfiles/Imo2005P3.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2005, Problem 3

Let x, y and z be positive real numbers such that xyz ≥ 1. Prove that: (x^5 - x^2)/(x^5 + y^2 + z^2) + (y^5 - y^2)/(y^5 + z^2 + x^2) + (z^5 - z^2)/(z^5 + x^2 + y^2) ≥ 0

Imports (3)
Imported by 1 file
  1. theorem Imo2005P3.key_insight line 39 source

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

    Statement uses: Real, GT.gt, OfNat.ofNat, GE.ge, HMul.hMul, HDiv.hDiv, HSub.hSub, HPow.hPow, Nat, HAdd.hAdd

    Proof uses: Eq, Eq.mpr, inferInstance, CommGroupWithZero, GroupWithZero, 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, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, rfl, Eq.trans, Mathlib.Tactic.FieldSimp.subst_sub, congr_arg₂, Mathlib.Tactic.FieldSimp.NF.div_eq_eval and 134 more

    145 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  2. problem Imo2005P3.imo2005_p3 line 59 source

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

    Statement uses: Real, GT.gt, OfNat.ofNat, GE.ge, HMul.hMul, HAdd.hAdd, HDiv.hDiv, HSub.hSub, HPow.hPow, Nat

    Proof uses: Trans.trans, Eq, id, add_le_add, LE.le, Imo2005P3.key_insight, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero and 94 more

    125 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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