Compfiles/Imo1965P4.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1965, Problem 4

Find all sets of four real numbers x₁, x₂, x₃, x₄ such that the sum of any one and the product of the other three is equal to 2.

Imports (2)
Imported by 1 file
  1. determine Imo1965P4.solution line 28 source

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

    Statement uses: Set, Multiset, Real

    Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton, Neg.neg

    10 instances, coercions and auxiliary constants left out.

  2. lemma Imo1965P4.cubic line 32 source

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

    Statement uses: Real, Eq, HSub.hSub, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat

    Proof uses: dite, Not, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, Neg.neg, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Ring, Int.rawCast, Int.negOfNat and 74 more

    114 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  3. lemma Imo1965P4.multiset_erase line 37 source

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

    Statement uses: DecidableEq, Multiset, Membership.mem, Eq, Multiset.erase, Multiset.cons

    3 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. lemma Imo1965P4.multiset_order₁ line 47 source

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

    Statement uses: Eq, Multiset, Real, Insert.insert, OfNat.ofNat, Nat, Neg.neg, Singleton.singleton

    Proof uses: Multiset.ext', dite, Multiset.count, of_eq_true, Eq.trans, True, congr, congrArg, HAdd.hAdd, Multiset.cons, Multiset.count.congr_simp, id, Eq.refl, Multiset.count_cons_self, congrFun', Multiset.count_eq_zero_of_notMem, Not, Membership.mem, False, Or and 24 more

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. lemma Imo1965P4.multiset_order₂ line 48 source

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

    Statement uses: Eq, Multiset, Real, Insert.insert, Neg.neg, OfNat.ofNat, Nat, Singleton.singleton

    Proof uses: Multiset.ext', dite, Multiset.count, of_eq_true, Eq.trans, True, congr, congrArg, Multiset.cons, Multiset.count.congr_simp, id, Eq.refl, Multiset.count_cons_of_ne, Not, False, eq_false, Ne, Mathlib.Meta.NormNum.isInt_eq_false, Int.ofNat, Int.negOfNat and 23 more

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  6. problem Imo1965P4.imo1965_p4 line 52 source

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

    Statement uses: Eq, Set, Multiset, Real, Set.ofPred, And, Nat, Multiset.card, OfNat.ofNat, Membership.mem, HAdd.hAdd, Multiset.prod, Multiset.erase, Imo1965P4.solution

    Proof uses: Set.ext, Iff.intro, Ne, EmptyCollection.emptyCollection, Iff.mp, LT.lt, Multiset.card_pos, lt_of_lt_of_eq, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, Eq.symm, HSub.hSub, HPow.hPow, HMul.hMul, Exists, Multiset.exists_mem_of_ne_zero, dite and 124 more

    157 instances, coercions and auxiliary constants left out.

    Tactic trace: 124 steps

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