Compfiles/Imo1961P1.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1961, Problem 1.

Given constants a and b, solve the system of equations

x + y + z = a x² + y² + z² = b² xy = z²

for x,y,z. Give the conditions that a and b must satisfy so that the solutions x,y,z are distinct positive numbers.

Imports (2)
Imported by 1 file
  1. abbrev Imo1961P1.IsSolution line 32 source

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

    Statement uses: Real

    Proof uses: And, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul

    9 instances, coercions and auxiliary constants left out.

  2. determine Imo1961P1.xyz_of_ab line 37 source

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

    Statement uses: Real, Set, Prod

    Proof uses: Set.ofPred, Imo1961P1.xyz_of_ab.match_1, Or, And, Ne, OfNat.ofNat, Eq, HDiv.hDiv, HSub.hSub, HPow.hPow, Nat, HMul.hMul, HAdd.hAdd

    19 instances, coercions and auxiliary constants left out.

  3. determine Imo1961P1.ab_that_make_xyz_positive_distinct line 44 source

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

    Statement uses: Set, Prod, Real

    Proof uses: Set.ofPred, Imo1961P1.ab_that_make_xyz_positive_distinct.match_1, And, LT.lt, OfNat.ofNat, HPow.hPow, Nat, HMul.hMul

    13 instances, coercions and auxiliary constants left out.

  4. lemma Imo1961P1.aux_1 line 50 source

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

    Statement uses: Real, And, LT.lt, OfNat.ofNat, List.Nodup, List.cons, List.nil, Eq, HAdd.hAdd, HPow.hPow, Nat, HMul.hMul

    Proof uses: lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 191 more

    185 instances, coercions and auxiliary constants left out.

    Tactic trace: 117 steps

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

  5. problem Imo1961P1.imo1961_p1a line 155 source

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

    Statement uses: Real, Iff, Membership.mem, Prod, Set, Imo1961P1.xyz_of_ab, Prod.mk, Imo1961P1.IsSolution

    Proof uses: id, Iff.intro, Or, And, Not, Eq, OfNat.ofNat, HDiv.hDiv, HSub.hSub, HPow.hPow, Nat, HMul.hMul, HAdd.hAdd, Eq.mpr, congrArg, add_sq, mul_assoc, Eq.symm, Mathlib.Tactic.Ring.of_eq, Nat.rawCast and 90 more

    108 instances, coercions and auxiliary constants left out.

    Tactic trace: 39 steps

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

  6. problem Imo1961P1.imo1961_p1b line 192 source

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

    Statement uses: Real, Imo1961P1.IsSolution, Iff, Membership.mem, Prod, Set, Imo1961P1.ab_that_make_xyz_positive_distinct, Prod.mk, And, LT.lt, OfNat.ofNat, List.Nodup, List.cons, List.nil

    Proof uses: Eq, HAdd.hAdd, HPow.hPow, Nat, HMul.hMul, Iff.intro, Eq.mpr, Not, id, Eq.trans, implies_congr, Eq.refl, congrArg, List, congr, Or, False, or_false, True, not_false_eq_true and 117 more

    144 instances, coercions and auxiliary constants left out.

    Tactic trace: 68 steps

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