Compfiles/Imo1959P2.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1959, Problem 2

For what real values of x is

√(x+√(2x-1)) + √(x-√(2x-1)) = A,

given: (a) A = √2 (b) A = 1 (c) A = 2, where only non-negative real numbers are admitted for square roots?

Imports (2)
Imported by 1 file
  1. def Imo1959P2.IsGood line 38 source

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

    Statement uses: Real

    Proof uses: And, Eq, HAdd.hAdd, Real.sqrt, HSub.hSub, HMul.hMul, OfNat.ofNat, LE.le

    14 instances, coercions and auxiliary constants left out.

  2. theorem Imo1959P2.isGood_iff line 54 source

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

    Statement uses: Real, Iff, Imo1959P2.IsGood, And, Eq, HAdd.hAdd, Real.sqrt, HSub.hSub, HMul.hMul, OfNat.ofNat, Nat, abs, LE.le, HDiv.hDiv

    Proof uses: LT.lt, Or, le_or_gt, Or.inl, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, HPow.hPow, Int.rawCast, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr and 140 more

    144 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

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

  3. theorem Imo1959P2.IsGood.one_half_le line 71 source

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

    Statement uses: Real, Imo1959P2.IsGood, LE.le, HDiv.hDiv, OfNat.ofNat, Nat

    Proof uses: And.right, Eq, HAdd.hAdd, Real.sqrt, HSub.hSub, HMul.hMul, abs, Iff.mp, And, Imo1959P2.isGood_iff

    30 instances, coercions and auxiliary constants left out.

  4. theorem Imo1959P2.sqrt_two_mul_sub_one_le_one line 73 source

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

    Statement uses: Real, Iff, LE.le, Real.sqrt, HSub.hSub, HMul.hMul, OfNat.ofNat, Nat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, And, HPow.hPow, congr, HAdd.hAdd, one_pow, mul_one, LT.lt, true_and, iff_self

    73 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. theorem Imo1959P2.isGood_iff_eq_sqrt_two line 76 source

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

    Statement uses: Real, Membership.mem, Set, Set.Icc, HDiv.hDiv, OfNat.ofNat, Nat, Iff, Imo1959P2.IsGood, Eq, Real.sqrt

    Proof uses: LE.le, HSub.hSub, HMul.hMul, Iff.mpr, Imo1959P2.sqrt_two_mul_sub_one_le_one, And.right, Eq.mpr, HAdd.hAdd, id, congrFun', congrArg, Eq.trans, And, abs, True, congr, abs_sub_comm, abs_of_nonneg, sub_nonneg, eq_true and 56 more

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  6. theorem Imo1959P2.isGood_iff_eq_sqrt line 83 source

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

    Statement uses: Real, LT.lt, OfNat.ofNat, Iff, Imo1959P2.IsGood, Eq, Real.sqrt, HSub.hSub, HMul.hMul, Nat

    Proof uses: Eq.mpr, Not, LE.le, id, Eq.trans, congrArg, Eq.mp, HDiv.hDiv, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, HAdd.hAdd, Neg.neg, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Ring and 97 more

    138 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  7. theorem Imo1959P2.IsGood.sqrt_two_lt_of_one_lt line 91 source

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

    Statement uses: Real, Imo1959P2.IsGood, LT.lt, OfNat.ofNat, Real.sqrt, Nat

    Proof uses: Eq.mpr, HSub.hSub, HMul.hMul, id, Eq, congrArg, Iff.mp, Imo1959P2.isGood_iff_eq_sqrt, Real.sqrt_lt_sqrt, zero_le_two, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, HPow.hPow, Int.rawCast and 51 more

    76 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  8. theorem Imo1959P2.IsGood.eq_sqrt_two_iff_le_one line 96 source

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

    Statement uses: Real, Imo1959P2.IsGood, Iff, Eq, Real.sqrt, OfNat.ofNat, Nat, LE.le

    Proof uses: Iff.intro, Iff.mp, Not, LT.lt, not_lt, LT.lt.ne', Imo1959P2.IsGood.sqrt_two_lt_of_one_lt, Imo1959P2.isGood_iff_eq_sqrt_two, And.intro, HDiv.hDiv, Imo1959P2.IsGood.one_half_le

    25 instances, coercions and auxiliary constants left out.

  9. theorem Imo1959P2.IsGood.sqrt_two_lt_iff_one_lt line 100 source

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

    Statement uses: Real, Imo1959P2.IsGood, Iff, LT.lt, Real.sqrt, OfNat.ofNat, Nat

    Proof uses: Iff.intro, Iff.mp, Not, LE.le, not_le, LT.lt.ne', Iff.mpr, Eq, Imo1959P2.IsGood.eq_sqrt_two_iff_le_one, Imo1959P2.IsGood.sqrt_two_lt_of_one_lt

    23 instances, coercions and auxiliary constants left out.

  10. theorem Imo1959P2.IsGood.sqrt_two_le line 103 source

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

    Statement uses: Real, Imo1959P2.IsGood, LE.le, Real.sqrt, OfNat.ofNat, Nat

    Proof uses: Or.elim, LT.lt, le_or_gt, Eq.ge, Iff.mpr, Eq, Imo1959P2.IsGood.eq_sqrt_two_iff_le_one, LT.lt.le, Imo1959P2.IsGood.sqrt_two_lt_of_one_lt

    20 instances, coercions and auxiliary constants left out.

  11. theorem Imo1959P2.isGood_iff_of_sqrt_two_lt line 107 source

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

    Statement uses: Real, LT.lt, Real.sqrt, OfNat.ofNat, Nat, Iff, Imo1959P2.IsGood, Eq, HAdd.hAdd, HPow.hPow, HDiv.hDiv

    Proof uses: lt_trans, of_eq_true, Eq.trans, True, Iff.intro, Eq.mp, congrArg, propext, Imo1959P2.IsGood.sqrt_two_lt_iff_one_lt, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Neg.neg, HSub.hSub, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 115 more

    118 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

  12. determine Imo1959P2.solution_set_sqrt2 line 121 source

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

    Statement uses: Set, Real

    Proof uses: Set.Icc, HDiv.hDiv, OfNat.ofNat

    9 instances, coercions and auxiliary constants left out.

  13. problem Imo1959P2.imo1959_p2a line 123 source

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

    Statement uses: Real, Iff, Imo1959P2.IsGood, Real.sqrt, OfNat.ofNat, Nat, Membership.mem, Set, Imo1959P2.solution_set_sqrt2

    Proof uses: Iff.intro, And.intro, LE.le, HDiv.hDiv, Imo1959P2.IsGood.one_half_le, Iff.mp, Not, LT.lt, not_lt, LT.lt.false, Imo1959P2.IsGood.sqrt_two_lt_of_one_lt, Iff.mpr, Eq, Imo1959P2.isGood_iff_eq_sqrt_two, rfl

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  14. determine Imo1959P2.solution_set_one line 127 source

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

    Statement uses: Set, Real

    Proof uses: EmptyCollection.emptyCollection

    1 instances, coercions and auxiliary constants left out.

  15. problem Imo1959P2.imo1959_p2b line 129 source

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

    Statement uses: Real, Iff, Imo1959P2.IsGood, OfNat.ofNat, Membership.mem, Set, Imo1959P2.solution_set_one

    Proof uses: Not, LE.le.not_gt, Real.sqrt, Nat, Imo1959P2.IsGood.sqrt_two_le, Iff.mpr, LT.lt, HPow.hPow, Real.lt_sqrt, zero_le_one, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.one_natPow, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, iff_of_false

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  16. determine Imo1959P2.solution_set_two line 134 source

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

    Statement uses: Set, Real

    Proof uses: Singleton.singleton, HDiv.hDiv, OfNat.ofNat

    8 instances, coercions and auxiliary constants left out.

  17. problem Imo1959P2.imo1959_p2c line 136 source

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

    Statement uses: Real, Iff, Imo1959P2.IsGood, OfNat.ofNat, Nat, Membership.mem, Set, Imo1959P2.solution_set_two

    Proof uses: Eq.mpr, Eq, HDiv.hDiv, id, congrArg, Singleton.singleton, propext, Set.mem_singleton_iff, Iff.trans, HAdd.hAdd, HPow.hPow, Imo1959P2.isGood_iff_of_sqrt_two_lt, Iff.mpr, LT.lt, Real.sqrt, Real.sqrt_lt', two_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 25 more

    63 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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