Compfiles/Imo1985P6.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1985, Problem 6

For every real number x_1, construct the sequence {x_1,x_2, ...} by setting x_{n+1} = x_n * (x_n + 1 / n) for each n >= 1.

Prove that there exists exactly one value of x_1 for which 0 < x_n , x_n < x_{n+1}, and x_{n+1} < 1 for every n.

Imports (3)
Imported by 1 file
  1. lemma Imo1985P6.aux_1 line 37 source

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

    Statement uses: Nat, NNReal, Real, Eq, OfNat.ofNat, LT.lt, HAdd.hAdd, HMul.hMul, HDiv.hDiv, And

    Proof uses: Nat.le_induction, Nat.succ, Eq.mpr, id, congrArg, LE.le, Nat.zero_lt_of_lt, mul_pos, add_pos', div_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, Iff.mpr, Nat.cast_pos', lt_of_lt_of_le, inferInstance and 3 more

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  2. lemma Imo1985P6.aux_2 line 51 source

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

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

    Proof uses: Nat.strong_induction_on, Nat.casesAuxOn, absurd, Nat.lt_irrefl, Eq.symm, Eq.mpr, id, Eq.trans, congr, congrArg, congrFun', zero_add, Nat.succ, Nat.succ_pos, Nat.lt_succ_self, mul_lt_mul, add_le_add, le_of_lt, le_rfl, add_pos_of_nonneg_of_pos and 9 more

    91 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  3. lemma Imo1985P6.aux_3 line 74 source

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

    Statement uses: Nat, NNReal, Real, Eq, OfNat.ofNat, LT.lt, HAdd.hAdd, HMul.hMul, HDiv.hDiv, And, LE.le

    Proof uses: Or, lt_or_eq_of_le, le_of_lt, Nat.zero_lt_of_lt, Eq.mpr, id, congrArg, le_refl, Nat.le_induction, Nat.succ, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.instAddMonoidWithOne' and 24 more

    106 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

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

  4. lemma Imo1985P6.aux_4 line 102 source

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

    Statement uses: Nat, NNReal, Real, LT.lt, OfNat.ofNat, LE.le, Eq, Real.toNNReal, StrictMono

    Proof uses: Eq.mpr, id, congrArg, Iff.mpr, Real.toNNReal_lt_toNNReal_iff_of_nonneg

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  5. lemma Imo1985P6.aux_5 line 113 source

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

    Statement uses: Nat, NNReal, Real, LT.lt, OfNat.ofNat, Function.Injective, StrictMono, Eq, Function.invFun

    Proof uses: congrFun, Eq.mpr, id, congrArg, Eq.symm, StrictMono.injective, Function.comp, Function.invFun_comp, NNReal.eq, Eq.mp, Function.comp_def

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  6. lemma Imo1985P6.aux_6 line 133 source

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

    Statement uses: Nat, NNReal, Real, Eq, OfNat.ofNat, LT.lt, HAdd.hAdd, HMul.hMul, HDiv.hDiv, Real.toNNReal, Continuous

    Proof uses: Eq.mpr, id, congrArg, Continuous.comp, continuous_real_toNNReal, Nat.le_induction, Nat.succ, funext, NNReal.continuous_coe, LE.le, Continuous.comp', Prod, Prod.mk, Prod.fst, Prod.snd, continuous_mul, Continuous.prodMk, Continuous.add_const

    49 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  7. lemma Imo1985P6.aux_7 line 153 source

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

    Statement uses: Nat, NNReal, Real, Eq, OfNat.ofNat, LT.lt, HAdd.hAdd, HMul.hMul, HDiv.hDiv, LE.le, And, Real.toNNReal, StrictMono, Continuous, Function.Surjective

    Proof uses: Continuous.surjective, Monotone.tendsto_atTop_atTop, StrictMono.monotone, Exists.intro, Nat.le_induction, Nat.succ, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, Real.toNNReal_add, congr, Real.toNNReal_coe, Real.toNNReal_one, Iff.mp, Real.le_toNNReal_iff_coe_le, Eq.mp, dite and 40 more

    172 instances, coercions and auxiliary constants left out.

    Tactic trace: 68 steps

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

  8. lemma Imo1985P6.aux_8 line 212 source

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

    Statement uses: Nat, NNReal, Real, Eq, OfNat.ofNat, LT.lt, HAdd.hAdd, HMul.hMul, HDiv.hDiv, StrictMono, Function.Injective, Real.toNNReal, Set, And, Membership.mem, HSub.hSub

    Proof uses: And.right, Eq.refl, Eq.mpr, id, congrArg, Eq.symm, Decidable.byContradiction, Not, LE.le, dite, le_of_lt, Imo1985P6.aux_3, And.intro, Eq.mp, Ne, Eq.trans, Nat.cast_zero, div_self, NNReal.sub_div, div_ne_zero and 79 more

    172 instances, coercions and auxiliary constants left out.

    Tactic trace: 50 steps

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

  9. lemma Imo1985P6.aux_9 line 269 source

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

    Statement uses: Nat, NNReal, Real, Eq, OfNat.ofNat, LT.lt, HAdd.hAdd, HMul.hMul, HDiv.hDiv, Real.toNNReal, StrictMono, Function.RightInverse, Iff, HSub.hSub, Set, Set.Ici, StrictMonoOn

    Proof uses: Eq.mpr, id, congrArg, strictMonoOn_Ici_of_pred_lt, Order.pred, Nat.le_induction, Nat.succ, NNReal.HolderConjugate, NNReal.HolderConjugate.two_two, Inv.inv, Eq.trans, congr, Order.pred_eq_sub_one, Nat.cast_one, div_self, of_eq_true, Not, False, True, not_false_eq_true and 45 more

    194 instances, coercions and auxiliary constants left out.

    Tactic trace: 72 steps

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

  10. lemma Imo1985P6.aux_10 line 342 source

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

    Statement uses: Nat, NNReal, Real, Eq, OfNat.ofNat, LT.lt, HAdd.hAdd, HMul.hMul, HDiv.hDiv, Real.toNNReal, Function.RightInverse, Set, Set.Ici, Membership.mem, HSub.hSub, Set.range, Set.image, IsLUB

    Proof uses: Eq.mpr, id, congrArg, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, Subtype.mk, NNReal.HolderConjugate, NNReal.HolderConjugate.two_two, Inv.inv, Eq.trans, one_div, rfl, congr, Eq.symm, Nat.cast_zero, congrFun', Nat.cast_one and 22 more

    105 instances, coercions and auxiliary constants left out.

    Tactic trace: 52 steps

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

  11. lemma Imo1985P6.aux_11 line 409 source

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

    Statement uses: Set, Nat, NNReal, LT.lt, StrictMono, Membership.mem, StrictAnti, Eq, Set.range, Real, Set.image, IsLUB, IsGLB, LE.le

    Proof uses: Or, lt_or_ge, lt_trans, lt_or_eq_of_le, Eq.mpr, id, congrArg, Decidable.byContradiction, Not, Exists, And, IsLUB.exists_between, Eq.mp, False, IsGLB.exists_between, Real.toNNReal, Iff.mp, Set.mem_image, Eq.symm, Real.toNNReal_coe and 10 more

    43 instances, coercions and auxiliary constants left out.

    Tactic trace: 47 steps

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

  12. lemma Imo1985P6.aux_exists line 473 source

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

    Statement uses: Nat, NNReal, Real, And, LT.lt, OfNat.ofNat, StrictMono, Eq, Set, Set.Ici, Membership.mem, HSub.hSub, HDiv.hDiv, StrictAnti, Set.range, Set.image, HAdd.hAdd, LE.le, Exists

    Proof uses: Or, lt_or_eq_of_le, exists_between, gt_trans, Real.toNNReal, Iff.mpr, Real.toNNReal_pos, Exists.intro, Eq.mpr, id, congrArg, And.intro, Subtype.mk, NNReal.coe_sub, div_le_self, zero_le_one', Nat.one_le_cast, Eq.symm, Real.lt_toNNReal_iff_coe_lt, lt_of_le_of_lt and 21 more

    123 instances, coercions and auxiliary constants left out.

    Tactic trace: 167 steps

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

  13. lemma Imo1985P6.aux_unique_top_ind line 648 source

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

    Statement uses: Nat, NNReal, Real, Set, Eq, Set.Ici, OfNat.ofNat, HSub.hSub, Membership.mem, LT.lt, HAdd.hAdd, LE.le, HMul.hMul, HDiv.hDiv, Subtype.mk, HPow.hPow

    Proof uses: Eq.mpr, id, congrArg, Iff.mp, Set.mem_Ici, Eq.symm, Subtype.property, Nat.le_induction, of_eq_true, Eq.trans, True, congrFun', eq_self, tsub_self, pow_zero, mul_one, forall_congr, GE.ge, implies_congr, Eq.refl and 74 more

    180 instances, coercions and auxiliary constants left out.

    Tactic trace: 46 steps

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

  14. lemma Imo1985P6.aux_unique_top line 701 source

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

    Statement uses: Nat, NNReal, Real, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HMul.hMul, HDiv.hDiv, HSub.hSub, Set, Set.Ici, Membership.mem, And, Filter.Tendsto, Filter.atTop

    Proof uses: Eq.refl, Eq.mpr, id, congrArg, Eq.symm, Iff.mpr, LE.le, Set.mem_Ici, Nat.le_add_right_of_le, Iff.mp, Subtype.property, Subtype.mk, Nat.zero_lt_of_lt, of_eq_true, Eq.trans, Inv.inv, HPow.hPow, True, congr, Nat.rawCast and 124 more

    169 instances, coercions and auxiliary constants left out.

    Tactic trace: 99 steps

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

  15. lemma Imo1985P6.aux_unique_nhds line 801 source

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

    Statement uses: Nat, NNReal, Real, Set, Eq, Set.Ici, OfNat.ofNat, HSub.hSub, Membership.mem, LT.lt, And, HDiv.hDiv, Filter.Tendsto, Filter.atTop, nhds

    Proof uses: Nonempty, Eq.mpr, id, congrArg, Iff.mpr, IsOpen, Exists, LE.le, tendsto_atTop_nhds, Filter, IsOpen.mem_nhds, Set.Ioo, Iff.mp, mem_nhds_iff_exists_Ioo_subset, And.right, Set.mem_Ioo, HAdd.hAdd, Nat.ceil, Set.mem_Ici, Nat.le_add_right and 43 more

    165 instances, coercions and auxiliary constants left out.

    Tactic trace: 58 steps

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

  16. lemma Imo1985P6.aux_unique line 865 source

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

    Statement uses: Nat, NNReal, Real, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HMul.hMul, HDiv.hDiv, StrictMono, HSub.hSub, And

    Proof uses: Set, Set.Ici, Membership.mem, rfl, Eq.mpr, id, congrArg, Iff.mpr, sub_pos, lt_of_lt_of_le, Nat.zero_lt_two, Subtype.property, Filter.Tendsto, Filter.atTop, Imo1985P6.aux_unique_top, nhds, Imo1985P6.aux_unique_nhds, Decidable.byContradiction, Not, dite and 48 more

    132 instances, coercions and auxiliary constants left out.

    Tactic trace: 162 steps

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

  17. lemma Imo1985P6.imo_1985_p6_nnreal line 1014 source

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

    Statement uses: Nat, NNReal, Real, Eq, OfNat.ofNat, LT.lt, HAdd.hAdd, HMul.hMul, HDiv.hDiv, ExistsUnique, And

    Proof uses: Imo1985P6.aux_1, LE.le, Nat.le_induction, Nat.succ, Eq.mpr, id, congrArg, NNReal.zero_le_coe, mul_nonneg, le_of_lt, Right.add_pos_of_nonneg_of_pos, div_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, Iff.mpr, Nat.cast_pos' and 102 more

    194 instances, coercions and auxiliary constants left out.

    Tactic trace: 233 steps (first 200 of 233)

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

  18. problem Imo1985P6.imo1985_p6 line 1209 source

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

    Statement uses: Nat, Real, Eq, OfNat.ofNat, LT.lt, HAdd.hAdd, HMul.hMul, HDiv.hDiv, ExistsUnique, And

    Proof uses: NNReal, LE.le, rfl, Imo1985P6.imo_1985_p6_nnreal, Exists.intro, And.intro, dite, Iff.mp, Real.toNNReal, Real.toNNReal_eq_toNNReal_iff, NNReal.zero_le_coe, Eq.mpr, id, congrArg, Real.toNNReal_coe, zero_le, Real.coe_toNNReal, Not, False.elim, Eq.mp and 13 more

    55 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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