Compfiles/Usa2001P4.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2001, Problem 4

Let ABC be a triangle and P be any point such that PA, PB, PC are the sides of an obtuse triangle, with PA the longest side. Prove that ∠BAC is acute.

Imports (5)
Imported by 1 file
  1. lemma Usa2001P4.lemma1 line 34 source

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

    Statement uses: Real, LE.le, HAdd.hAdd, HMul.hMul, Real.sqrt, HPow.hPow, Nat, OfNat.ofNat

    Proof uses: EuclideanSpace, Fin, WithLp.toLp, ENNReal, Matrix.vecCons, Matrix.vecEmpty, abs, le_abs_self, Inner.inner, Norm.norm, abs_real_inner_le_norm, LE.le.trans, Eq.mp, congrArg, mul_comm, congr, Eq.trans, Finset.sum, Finset.univ, WithLp.ofLp and 22 more

    100 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  2. problem Usa2001P4.usa2001_p4 line 45 source

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

    Statement uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, AffineIndependent, ENNReal, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Eq, Dist.dist, LT.lt, HDiv.hDiv, Real.pi, EuclideanGeometry.angle

    Proof uses: Not, Collinear, Insert.insert, Set, Singleton.singleton, Iff.mp, affineIndependent_iff_not_collinear_set, Iff.mpr, Ne, dist_pos, ne₁₃_of_not_collinear, ne₂₃_of_not_collinear, ne₁₂_of_not_collinear, HAdd.hAdd, HPow.hPow, HMul.hMul, HSub.hSub, Real.cos, EuclideanGeometry.law_cos, sub_pos and 134 more

    215 instances, coercions and auxiliary constants left out.

    Tactic trace: 61 steps

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