Compfiles/Imo1974P5.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1974, Problem 5

What are the possible values of

a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)

as a,b,c,d range over the positive real numbers?

Imports (2)
Imported by 1 file
  1. determine Imo1974P5.solution_set line 29 source

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

    Statement uses: Set, Real

    Proof uses: Set.Ioo, OfNat.ofNat

    6 instances, coercions and auxiliary constants left out.

  2. lemma Imo1974P5.condition_implies_solution_set line 33 source

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

    Statement uses: Real, Exists, And, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HDiv.hDiv, Membership.mem, Set, Imo1974P5.solution_set

    Proof uses: Eq.mpr, id, congrArg, Set.Ioo, propext, Set.mem_Ioo, And.intro, div_lt_div_of_pos_left, add_pos', lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat, Nat.rawCast and 96 more

    129 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

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

  3. def Imo1974P5.S line 69 source

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

    Statement uses: Real

    Proof uses: HAdd.hAdd, HDiv.hDiv

    5 instances, coercions and auxiliary constants left out.

  4. def Imo1974P5.T line 73 source

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

    Statement uses: Real

    Proof uses: Imo1974P5.S, OfNat.ofNat, HSub.hSub, HMul.hMul

    6 instances, coercions and auxiliary constants left out.

  5. theorem Imo1974P5.T_continuous line 75 source

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

    Statement uses: ContinuousOn, Real, Imo1974P5.T, Set.Icc, OfNat.ofNat

    Proof uses: id, Imo1974P5.S, HSub.hSub, HMul.hMul, ContinuousOn.fun_add, HAdd.hAdd, HDiv.hDiv, ContinuousOn.div₀, continuousOn_const, ContinuousOn.const_add, ContinuousOn.fun_sub, continuousOn_id', ContinuousOn.fun_mul, Membership.mem, Set, LE.le, Ne, Not.intro, Eq, Mathlib.Tactic.Linarith.lt_irrefl and 71 more

    121 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  6. lemma Imo1974P5.T0 line 79 source

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

    Statement uses: Eq, Real, Imo1974P5.T, OfNat.ofNat

    Proof uses: of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAddMonoidWithOne', congrFun', congrArg, Mathlib.Meta.NormNum.IsNat.to_eq, HAdd.hAdd, HDiv.hDiv, HSub.hSub, HMul.hMul, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.IsNNRat.to_isNat, Mathlib.Meta.NormNum.isNNRat_add, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat and 15 more

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  7. lemma Imo1974P5.T1 line 80 source

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

    Statement uses: Eq, Real, Imo1974P5.T, OfNat.ofNat, Nat

    Proof uses: of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAddMonoidWithOne', Mathlib.Meta.NormNum.instAtLeastTwo, congrFun', congrArg, Mathlib.Meta.NormNum.IsNat.to_eq, HAdd.hAdd, HDiv.hDiv, HSub.hSub, HMul.hMul, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.IsNNRat.to_isNat, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Inv.inv, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_ofNat and 13 more

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  8. problem Imo1974P5.imo1974_p5 line 84 source

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

    Statement uses: Real, Iff, Membership.mem, Set, Imo1974P5.solution_set, Exists, And, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HDiv.hDiv

    Proof uses: Iff.intro, LE.le, Set.Ioo, Imo1974P5.T, Set.image, intermediate_value_Ioo, zero_le_one, Imo1974P5.T_continuous, Eq.mp, Nat, congrArg, Imo1974P5.T1, Imo1974P5.T0, propext, Set.mem_image, Set.mem_Ioo, Exists.intro, HSub.hSub, HMul.hMul, And.intro and 63 more

    126 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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