Compfiles/Iran1998P9.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Iranian Mathematical Olympiad 1998, Problem 9

Let x,y,z > 1 and 1/x + 1/y + 1/z = 2. Prove that

√(x + y + z) ≥ √(x - 1) + √(y - 1) + √(z - 1).

Imports (5)
Imported by 1 file
  1. lemma Iran1998P9.compute_norm line 34 source

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

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Eq, Norm.norm, ENNReal, Real.sqrt, Finset.sum, Finset.univ, HPow.hPow, WithLp.ofLp

    Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, EuclideanSpace.norm_eq, Finset.sum_congr, Eq.refl, Finset, Membership.mem, sq_abs, eq_self

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. problem Iran1998P9.iran1998_p9 line 39 source

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

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

    Proof uses: le_of_lt, lt_trans, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, HMul.hMul, HPow.hPow, Int.rawCast, inferInstance, Ring and 116 more

    145 instances, coercions and auxiliary constants left out.

    Tactic trace: 59 steps

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