Compfiles/Imo1963P1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1963, Problem 1

Find all real roots of the equation

√(x²-p) + 2√(x²-1) = x

where p is a real parameter.

Imports (3)
Imported by 1 file
  1. lemma Imo1963P1.iff_comm line 32 source

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

    Statement uses: Iff

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. determine Imo1963P1.f line 37 source

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

    Statement uses: Real, Set

    Proof uses: ite, And, LE.le, OfNat.ofNat, HDiv.hDiv, Singleton.singleton, HSub.hSub, HMul.hMul, Real.sqrt, EmptyCollection.emptyCollection

    19 instances, coercions and auxiliary constants left out.

  3. problem Imo1963P1.imo1963_p1 line 42 source

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

    Statement uses: Real, GE.ge, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, Iff, Eq, HAdd.hAdd, Real.sqrt, HMul.hMul, Membership.mem, Set, Imo1963P1.f

    Proof uses: Eq.mpr, And, LE.le, HDiv.hDiv, id, congrArg, Eq.trans, ite, Singleton.singleton, EmptyCollection.emptyCollection, Imo1963P1.iff_comm, Eq.symm, add_nonneg, Real.sqrt_nonneg, mul_nonneg, le_of_lt, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo and 238 more

    214 instances, coercions and auxiliary constants left out.

    Tactic trace: 127 steps

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