Compfiles/Usa2003P5.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2003, Problem 5

Prove that for a,b,c > 0: (2a+b+c)² / (2a²+(b+c)²) + (2b+c+a)² / (2b²+(c+a)²) + (2c+a+b)² / (2c²+(a+b)²) ≤ 8

Imports (3)
Imported by 1 file
  1. lemma Usa2003P5.bound line 36 source

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

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

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

    131 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  2. problem Usa2003P5.usa2003_p5 line 44 source

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

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

    Proof uses: Usa2003P5.bound, add_le_add, Eq.mpr, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, 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 and 82 more

    107 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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