Compfiles/Imo2001P1.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2001, Problem 1

Let ABC be an acute-angled triangle with O as its circumcenter. Let P on line BC be the foot of the altitude from A. Assume that ∠BCA ≥ ∠ABC + 30°. Prove that ∠CAB + ∠COP < 90°.

Imports (2)
Imported by 1 file
  1. lemma Imo2001P1.aux₀ line 43 source

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

    Statement uses: Real, Exists, Int, Eq, HMul.hMul, LT.lt, abs, OfNat.ofNat

    Proof uses: Eq.mpr, id, congrArg, mul_eq_zero_of_right, Mathlib.Tactic.Contrapose.contrapose₁, Not, Ne, LE.le, implies_congr, Eq.refl, abs_mul, Eq.symm, Int.cast_one, Int.cast_abs, propext, Int.cast_le, Int.one_le_abs, Trans.trans, le_abs_self, mul_one and 2 more

    77 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  2. lemma Imo2001P1.aux₁ line 60 source

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

    Statement uses: Real, LE.le, OfNat.ofNat, LT.lt, abs, HAdd.hAdd

    Proof uses: Eq.mpr, And, Neg.neg, id, Eq, congrArg, propext, abs_lt, And.intro, Trans.trans, rfl, And.left, Iff.mp, Eq.symm, zero_add, add_le_add_left, add_le_add_right, add_zero, And.right

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  3. lemma Imo2001P1.aux₂ line 75 source

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

    Statement uses: Real, Eq, abs, HAdd.hAdd, LT.lt

    Proof uses: Eq.symm, Eq.mpr, id, congrArg, Or, And, LE.le, OfNat.ofNat, propext, abs_add_eq_add_abs_iff, Mathlib.Tactic.Contrapose.contrapose₁, Not, Ne, implies_congr, Eq.trans, congr, Mathlib.Tactic.Push.not_and_eq, Eq.refl, ne_of_lt, dite and 6 more

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

  4. lemma Imo2001P1.aux₃ line 90 source

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

    Statement uses: Real.Angle, Eq, HAdd.hAdd, HSMul.hSMul, Nat, OfNat.ofNat, Real.pi, LT.lt, Real, abs, Real.Angle.toReal, HDiv.hDiv

    Proof uses: Eq.mpr, id, congrArg, rfl, Trans.trans, LE.le, abs_add_le, add_lt_add, Eq.mp, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne', Mathlib.Tactic.Ring.Common.add_congr, NNRat.rawCast, Mathlib.Tactic.Ring.Common.div_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.symm, Eq.refl and 60 more

    168 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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

  5. lemma Imo2001P1.aux₄ line 132 source

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

    Statement uses: Real.Angle, Eq, HSMul.hSMul, Nat, OfNat.ofNat, LT.lt, Real, abs, Real.Angle.toReal, HDiv.hDiv, Real.pi

    Proof uses: HMul.hMul, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Eq.mpr, id, congrArg, rfl, Int, Exists, Eq.mp, propext, Real.Angle.coe_eq_zero_iff, Eq.symm, Real.Angle.coe_nsmul, Real.Angle.coe_toReal, smul_smul, Trans.trans, Mathlib.Tactic.Ring.of_eq and 43 more

    120 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  6. lemma Imo2001P1.aux₅ line 150 source

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

    Statement uses: Real, Exists, Int, Eq, HSub.hSub, HMul.hMul, LT.lt, OfNat.ofNat, LE.le, abs, HDiv.hDiv, Nat

    Proof uses: dite, Eq.mpr, id, congrArg, Eq.mp, propext, sub_eq_zero, MulZeroClass.mul_zero, Int.cast_zero, le_refl, Not, le_trans, Eq.symm, Int.cast_one, Int.cast_abs, Int.cast_le, Int.one_le_abs, HAdd.hAdd, sub_eq_iff_eq_add, Or and 72 more

    136 instances, coercions and auxiliary constants left out.

    Tactic trace: 38 steps

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

  7. lemma Imo2001P1.aux₆ line 186 source

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

    Statement uses: Real.Angle, Eq, HAdd.hAdd, LE.le, Real, abs, Real.Angle.toReal

    Proof uses: Eq.mpr, id, congrArg, rfl, Trans.trans, Imo2001P1.aux₅, HMul.hMul, OfNat.ofNat, Nat, Real.pi, Eq.mp, Exists, Int, HSub.hSub, propext, Real.Angle.angle_eq_iff_two_pi_dvd_sub, Eq.symm, Real.Angle.coe_add, Real.Angle.coe_toReal, Real.two_pi_pos and 11 more

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  8. lemma Imo2001P1.aux₇ line 203 source

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

    Statement uses: Real.Angle, Eq, Real, Real.sin, abs, Real.Angle.toReal, Real.Angle.sin

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, Real.Angle.coe_toReal, Real.Angle.sin_coe, LE.le, Real.pi, Real.Angle.abs_toReal_le_pi, Real.abs_sin_eq_sin_abs_of_abs_le_pi

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  9. structure Imo2001P1.Imo2001q1Cfg line 209 source

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

  10. def Imo2001P1.Imo2001q1Cfg.ABC line 221 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal

    Proof uses: Affine.Simplex.mk, Matrix.vecCons, Imo2001P1.Imo2001q1Cfg.A, Imo2001P1.Imo2001q1Cfg.B, Imo2001P1.Imo2001q1Cfg.C, Matrix.vecEmpty, Imo2001P1.Imo2001q1Cfg.hABC

    52 instances, coercions and auxiliary constants left out.

  11. def Imo2001P1.Imo2001q1Cfg.P line 224 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat

    Proof uses: Affine.Simplex.altitudeFoot, ENNReal, Imo2001P1.Imo2001q1Cfg.ABC, HAdd.hAdd

    28 instances, coercions and auxiliary constants left out.

  12. def Imo2001P1.Imo2001q1Cfg.O line 227 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat

    Proof uses: Affine.Simplex.circumcenter, ENNReal, Imo2001P1.Imo2001q1Cfg.ABC

    23 instances, coercions and auxiliary constants left out.

  13. lemma Imo2001P1.Imo2001q1Cfg.A_ne_B line 230 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2001P1.Imo2001q1Cfg.A, Imo2001P1.Imo2001q1Cfg.B

    Proof uses: Function.Injective.ne, Nat.succ, Matrix.vecCons, Imo2001P1.Imo2001q1Cfg.C, Matrix.vecEmpty, AffineIndependent.injective, ENNReal, Imo2001P1.Imo2001q1Cfg.hABC, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  14. lemma Imo2001P1.Imo2001q1Cfg.A_ne_C line 233 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2001P1.Imo2001q1Cfg.A, Imo2001P1.Imo2001q1Cfg.C

    Proof uses: Function.Injective.ne, Nat.succ, Matrix.vecCons, Imo2001P1.Imo2001q1Cfg.B, Matrix.vecEmpty, AffineIndependent.injective, ENNReal, Imo2001P1.Imo2001q1Cfg.hABC, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  15. lemma Imo2001P1.Imo2001q1Cfg.C_ne_B line 236 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2001P1.Imo2001q1Cfg.C, Imo2001P1.Imo2001q1Cfg.B

    Proof uses: Function.Injective.ne, Nat.succ, Matrix.vecCons, Imo2001P1.Imo2001q1Cfg.A, Matrix.vecEmpty, AffineIndependent.injective, ENNReal, Imo2001P1.Imo2001q1Cfg.hABC, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  16. lemma Imo2001P1.Imo2001q1Cfg.CO_circumradius line 239 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Eq, Real, Dist.dist, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.O, Imo2001P1.Imo2001q1Cfg.C, Affine.Simplex.circumradius, Imo2001P1.Imo2001q1Cfg.ABC

    Proof uses: Affine.Simplex.dist_circumcenter_eq_circumradius', HAdd.hAdd

    52 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  17. lemma Imo2001P1.Imo2001q1Cfg.C_ne_O line 242 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2001P1.Imo2001q1Cfg.O, Imo2001P1.Imo2001q1Cfg.C

    Proof uses: Eq.mpr, LT.lt, Dist.dist, ENNReal, id, Eq, congrArg, Eq.symm, propext, dist_pos, Affine.Simplex.circumradius, Imo2001P1.Imo2001q1Cfg.ABC, Imo2001P1.Imo2001q1Cfg.CO_circumradius, Affine.Simplex.circumradius_pos

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  18. lemma Imo2001P1.Imo2001q1Cfg.A_opposite_BC line 246 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Eq, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Insert.insert, Imo2001P1.Imo2001q1Cfg.B, Singleton.singleton, Imo2001P1.Imo2001q1Cfg.C, Set.range, HAdd.hAdd, HSub.hSub, Affine.Simplex.points, ENNReal, Affine.Simplex.faceOpposite, Imo2001P1.Imo2001q1Cfg.ABC

    Proof uses: Set.eq_of_subset_of_card_le, Membership.mem, Eq.mpr, Exists, And, Not, id, Eq.trans, Compl.compl, Set.image, congrFun', congrArg, Affine.Simplex.range_faceOpposite_points, funext, Or, Eq.mp, Exists.intro, True, False, not_false_eq_true and 27 more

    114 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

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

  19. lemma Imo2001P1.Imo2001q1Cfg.PBC_collinear line 270 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Collinear, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Insert.insert, Set, Imo2001P1.Imo2001q1Cfg.P, Imo2001P1.Imo2001q1Cfg.B, Singleton.singleton, Imo2001P1.Imo2001q1Cfg.C

    Proof uses: collinear_insert_of_mem_affineSpan_pair, Eq.mpr, Membership.mem, AffineSubspace, affineSpan, Set.range, HAdd.hAdd, HSub.hSub, Affine.Simplex.points, Affine.Simplex.faceOpposite, Imo2001P1.Imo2001q1Cfg.ABC, id, Eq, congrArg, Imo2001P1.Imo2001q1Cfg.A_opposite_BC, Affine.Simplex.altitudeFoot_mem_affineSpan_faceOpposite

    76 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  20. lemma Imo2001P1.Imo2001q1Cfg.APx_eq line 275 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Membership.mem, Set, Insert.insert, Imo2001P1.Imo2001q1Cfg.B, Singleton.singleton, Imo2001P1.Imo2001q1Cfg.C, Eq, EuclideanGeometry.angle, ENNReal, Imo2001P1.Imo2001q1Cfg.A, Imo2001P1.Imo2001q1Cfg.P, HDiv.hDiv, Real.pi

    Proof uses: Eq.mpr, InnerProductGeometry.angle, VSub.vsub, id, congrArg, EuclideanGeometry.angle.eq_1, Inner.inner, Eq.symm, propext, InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, Submodule.IsOrtho.inner_eq, vectorSpan, Set.image, HAdd.hAdd, Affine.Simplex.points, Imo2001P1.Imo2001q1Cfg.ABC, Compl.compl, AffineSubspace.direction, Affine.Simplex.altitude and 27 more

    101 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

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

  21. lemma Imo2001P1.Imo2001q1Cfg.APC_eq line 289 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Eq, Real, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.A, Imo2001P1.Imo2001q1Cfg.P, Imo2001P1.Imo2001q1Cfg.C, HDiv.hDiv, Real.pi

    Proof uses: Imo2001P1.Imo2001q1Cfg.APx_eq, of_eq_true, Membership.mem, Set, Insert.insert, Imo2001P1.Imo2001q1Cfg.B, Singleton.singleton, Eq.trans, Or, True, congrArg, eq_self, or_true

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  22. lemma Imo2001P1.Imo2001q1Cfg.APB_eq line 293 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Eq, Real, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.A, Imo2001P1.Imo2001q1Cfg.P, Imo2001P1.Imo2001q1Cfg.B, HDiv.hDiv, Real.pi

    Proof uses: Imo2001P1.Imo2001q1Cfg.APx_eq, of_eq_true, Membership.mem, Set, Insert.insert, Singleton.singleton, Imo2001P1.Imo2001q1Cfg.C, Eq.trans, Or, True, congr, congrArg, eq_self, true_or

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  23. lemma Imo2001P1.Imo2001q1Cfg.PC_eq line 297 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Eq, Real, Dist.dist, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.P, Imo2001P1.Imo2001q1Cfg.C, HMul.hMul, Imo2001P1.Imo2001q1Cfg.A, Real.cos, EuclideanGeometry.angle

    Proof uses: Eq.symm, Eq.mpr, id, congrArg, mul_comm, EuclideanGeometry.angle_comm, dist_comm, EuclideanGeometry.cos_angle_mul_dist_of_angle_eq_pi_div_two, Imo2001P1.Imo2001q1Cfg.APC_eq

    61 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  24. lemma Imo2001P1.Imo2001q1Cfg.non_sbtw_BCP line 302 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Not, Sbtw, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.B, Imo2001P1.Imo2001q1Cfg.C, Imo2001P1.Imo2001q1Cfg.P

    Proof uses: Eq, EuclideanGeometry.angle, Real.pi, Sbtw.angle₁₂₃_eq_pi, Mathlib.Tactic.Contrapose.contrapose₁, False, Eq.mpr, True, Ne, id, implies_congr, not_false_eq_true, Eq.refl, ne_of_lt, Real.Angle, HAdd.hAdd, EuclideanGeometry.oangle, Imo2001P1.planeFiniteDim, Imo2001P1.someOrientation, Imo2001P1.Imo2001q1Cfg.A and 53 more

    127 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  25. lemma Imo2001P1.Imo2001q1Cfg.wbtw_BPC line 317 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Or, Wbtw, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.P, Imo2001P1.Imo2001q1Cfg.B, Imo2001P1.Imo2001q1Cfg.C

    Proof uses: Not, Sbtw, Imo2001P1.Imo2001q1Cfg.non_sbtw_BCP, Collinear.wbtw_or_wbtw_or_wbtw, Imo2001P1.Imo2001q1Cfg.PBC_collinear, Mathlib.Tactic.Contrapose.contrapose₂, Eq.mpr, And, id, Eq, implies_congr, Eq.refl, And.intro, Ne, False.elim, Imo2001P1.Imo2001q1Cfg.C_ne_B, Mathlib.Tactic.Contrapose.contrapose₄, congrArg, wbtw_self_left

    68 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  26. lemma Imo2001P1.Imo2001q1Cfg.P_ne_C line 330 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Ne, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Imo2001P1.Imo2001q1Cfg.P, Imo2001P1.Imo2001q1Cfg.C

    Proof uses: Eq, LT.lt, EuclideanGeometry.angle, ENNReal, Imo2001P1.Imo2001q1Cfg.B, Imo2001P1.Imo2001q1Cfg.A, HDiv.hDiv, Real.pi, Imo2001P1.Imo2001q1Cfg.hAcuteC, Mathlib.Tactic.Contrapose.contrapose₁, False, Eq.mpr, Not, True, LE.le, id, implies_congr, not_false_eq_true, le_of_eq, congrArg and 4 more

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  27. lemma Imo2001P1.Imo2001q1Cfg.oriented_BCO_CAB line 337 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Eq, Real.Angle, HAdd.hAdd, HSMul.hSMul, Nat, OfNat.ofNat, EuclideanGeometry.oangle, EuclideanSpace, Real, Fin, ENNReal, Imo2001P1.planeFiniteDim, Imo2001P1.someOrientation, Imo2001P1.Imo2001q1Cfg.B, Imo2001P1.Imo2001q1Cfg.C, Imo2001P1.Imo2001q1Cfg.O, Imo2001P1.Imo2001q1Cfg.A, Real.pi

    Proof uses: EuclideanGeometry.Sphere.two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi, Affine.Simplex.circumsphere, Imo2001P1.Imo2001q1Cfg.ABC, Affine.Simplex.mem_circumsphere, Imo2001P1.Imo2001q1Cfg.A_ne_C, Imo2001P1.Imo2001q1Cfg.A_ne_B, Imo2001P1.Imo2001q1Cfg.C_ne_B

    63 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

  28. lemma Imo2001P1.Imo2001q1Cfg.acute_BCO line 346 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, LT.lt, Real, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.B, Imo2001P1.Imo2001q1Cfg.C, Imo2001P1.Imo2001q1Cfg.O, HDiv.hDiv, Real.pi

    Proof uses: Eq.mpr, abs, Real.Angle.toReal, EuclideanGeometry.oangle, Imo2001P1.planeFiniteDim, Imo2001P1.someOrientation, id, Eq, congrArg, EuclideanGeometry.angle_eq_abs_oangle_toReal, Ne.symm, Imo2001P1.Imo2001q1Cfg.C_ne_B, Imo2001P1.Imo2001q1Cfg.C_ne_O, EuclideanGeometry.Sphere.abs_oangle_center_right_toReal_lt_pi_div_two, Affine.Simplex.circumsphere, Imo2001P1.Imo2001q1Cfg.ABC, Affine.Simplex.mem_circumsphere, HAdd.hAdd

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  29. lemma Imo2001P1.Imo2001q1Cfg.BCO_CAB line 352 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Eq, Real, HAdd.hAdd, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.B, Imo2001P1.Imo2001q1Cfg.C, Imo2001P1.Imo2001q1Cfg.O, Imo2001P1.Imo2001q1Cfg.A, HDiv.hDiv, Real.pi

    Proof uses: Real.Angle, HSMul.hSMul, EuclideanGeometry.oangle, Imo2001P1.planeFiniteDim, Imo2001P1.someOrientation, Imo2001P1.Imo2001q1Cfg.oriented_BCO_CAB, LT.lt, Imo2001P1.Imo2001q1Cfg.acute_BCO, Imo2001P1.Imo2001q1Cfg.hAcuteA, Eq.mpr, abs, Real.Angle.toReal, id, congrArg, EuclideanGeometry.angle_eq_abs_oangle_toReal, Ne.symm, Imo2001P1.Imo2001q1Cfg.C_ne_B, Imo2001P1.Imo2001q1Cfg.C_ne_O, Imo2001P1.Imo2001q1Cfg.A_ne_C, Imo2001P1.Imo2001q1Cfg.A_ne_B and 2 more

    76 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  30. lemma Imo2001P1.Imo2001q1Cfg.xCP_eq_xCB line 360 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Ne, Imo2001P1.Imo2001q1Cfg.C, Eq, EuclideanGeometry.angle, ENNReal, Imo2001P1.Imo2001q1Cfg.P, Imo2001P1.Imo2001q1Cfg.B

    Proof uses: Real.Angle, EuclideanGeometry.oangle, Imo2001P1.planeFiniteDim, Imo2001P1.someOrientation, eq_of_sub_eq_zero, Eq.mpr, HSub.hSub, id, congrArg, EuclideanGeometry.oangle_sub_left, Ne.symm, Imo2001P1.Imo2001q1Cfg.C_ne_B, Imo2001P1.Imo2001q1Cfg.P_ne_C, Or, Wbtw, propext, EuclideanGeometry.oangle_eq_zero_iff_wbtw, wbtw_comm, Imo2001P1.Imo2001q1Cfg.wbtw_BPC, abs and 3 more

    72 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  31. lemma Imo2001P1.Imo2001q1Cfg.OCP_eq_OCB line 371 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Eq, Real, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.O, Imo2001P1.Imo2001q1Cfg.C, Imo2001P1.Imo2001q1Cfg.P, Imo2001P1.Imo2001q1Cfg.B

    Proof uses: Imo2001P1.Imo2001q1Cfg.xCP_eq_xCB, Imo2001P1.Imo2001q1Cfg.C_ne_O

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  32. lemma Imo2001P1.Imo2001q1Cfg.CAB_OCP line 374 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Eq, Real, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.C, Imo2001P1.Imo2001q1Cfg.A, Imo2001P1.Imo2001q1Cfg.B, HSub.hSub, HDiv.hDiv, Real.pi, Imo2001P1.Imo2001q1Cfg.O, Imo2001P1.Imo2001q1Cfg.P

    Proof uses: Eq.mpr, HAdd.hAdd, id, congrArg, Eq.symm, Imo2001P1.Imo2001q1Cfg.BCO_CAB, Imo2001P1.Imo2001q1Cfg.OCP_eq_OCB, EuclideanGeometry.angle_comm, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.refl, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.sub_pf and 21 more

    86 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  33. lemma Imo2001P1.Imo2001q1Cfg.oriented_BOC_BAC line 378 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Eq, Real.Angle, EuclideanGeometry.oangle, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.planeFiniteDim, Imo2001P1.someOrientation, Imo2001P1.Imo2001q1Cfg.B, Imo2001P1.Imo2001q1Cfg.O, Imo2001P1.Imo2001q1Cfg.C, HSMul.hSMul, Imo2001P1.Imo2001q1Cfg.A

    Proof uses: EuclideanGeometry.Sphere.oangle_center_eq_two_zsmul_oangle, Affine.Simplex.circumsphere, Imo2001P1.Imo2001q1Cfg.ABC, Affine.Simplex.mem_circumsphere, HAdd.hAdd, Imo2001P1.Imo2001q1Cfg.A_ne_B, Imo2001P1.Imo2001q1Cfg.A_ne_C

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  34. lemma Imo2001P1.Imo2001q1Cfg.angle_in_ABC_pos line 386 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Fin, OfNat.ofNat, Nat, Function.Injective, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Ne, Real, EuclideanGeometry.angle, EuclideanSpace, ENNReal, Affine.Simplex.points, Imo2001P1.Imo2001q1Cfg.ABC

    Proof uses: Eq, Function.comp, funext, Fin.ext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, of_eq_true, eq_self and 25 more

    98 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

  35. lemma Imo2001P1.Imo2001q1Cfg.BOC_non_collinear line 406 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Not, Collinear, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Insert.insert, Set, Imo2001P1.Imo2001q1Cfg.B, Imo2001P1.Imo2001q1Cfg.O, Singleton.singleton, Imo2001P1.Imo2001q1Cfg.C

    Proof uses: LT.lt, EuclideanGeometry.angle, Imo2001P1.Imo2001q1Cfg.A, HDiv.hDiv, Real.pi, Imo2001P1.Imo2001q1Cfg.hAcuteA, Eq, abs, Real.Angle.toReal, EuclideanGeometry.oangle, Imo2001P1.planeFiniteDim, Imo2001P1.someOrientation, Imo2001P1.aux₄, Iff.mpr, Real.Angle, HSMul.hSMul, Int, Or, Real.Angle.two_zsmul_eq_zero_iff, Eq.mp and 21 more

    103 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  36. lemma Imo2001P1.Imo2001q1Cfg.OCP_non_collinear line 419 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Not, Collinear, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Insert.insert, Set, Imo2001P1.Imo2001q1Cfg.P, Imo2001P1.Imo2001q1Cfg.C, Singleton.singleton, Imo2001P1.Imo2001q1Cfg.O

    Proof uses: Imo2001P1.Imo2001q1Cfg.BOC_non_collinear, Membership.mem, AffineSubspace, affineSpan, Collinear.mem_affineSpan_of_mem_of_ne, of_eq_true, Eq.trans, Or, Eq, True, congr, congrArg, eq_self, true_or, or_true, Imo2001P1.Imo2001q1Cfg.P_ne_C, Imo2001P1.Imo2001q1Cfg.B, Imo2001P1.Imo2001q1Cfg.PBC_collinear, collinear_insert_insert_of_mem_affineSpan_pair, Collinear.subset

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  37. lemma Imo2001P1.Imo2001q1Cfg.ACP_eq_ACB line 429 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Eq, Real, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.A, Imo2001P1.Imo2001q1Cfg.C, Imo2001P1.Imo2001q1Cfg.P, Imo2001P1.Imo2001q1Cfg.B

    Proof uses: Imo2001P1.Imo2001q1Cfg.xCP_eq_xCB, Imo2001P1.Imo2001q1Cfg.A_ne_C

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  38. lemma Imo2001P1.Imo2001q1Cfg.CA_eq line 432 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, Eq, Real, Dist.dist, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.C, Imo2001P1.Imo2001q1Cfg.A, HMul.hMul, Affine.Simplex.circumradius, Imo2001P1.Imo2001q1Cfg.ABC, Real.sin, EuclideanGeometry.angle, Imo2001P1.Imo2001q1Cfg.B

    Proof uses: Eq.mpr, abs, Real.Angle.toReal, EuclideanGeometry.oangle, Imo2001P1.planeFiniteDim, Imo2001P1.someOrientation, id, congrArg, EuclideanGeometry.angle_eq_abs_oangle_toReal, Imo2001P1.Imo2001q1Cfg.A_ne_B, Imo2001P1.Imo2001q1Cfg.C_ne_B, Real.Angle.sin, Imo2001P1.aux₇, Ne, propext, abs_ne_zero, And, Real.Angle, Real.pi, Real.Angle.sin_ne_zero_iff and 34 more

    108 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

  39. lemma Imo2001P1.Imo2001q1Cfg.four_sin_B_cos_A_le_one line 455 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, LE.le, Real, HMul.hMul, OfNat.ofNat, Nat, Real.sin, EuclideanGeometry.angle, EuclideanSpace, Fin, ENNReal, Imo2001P1.Imo2001q1Cfg.A, Imo2001P1.Imo2001q1Cfg.B, Imo2001P1.Imo2001q1Cfg.C, Real.cos

    Proof uses: HAdd.hAdd, HDiv.hDiv, Real.pi, Real.cos_le_cos_of_nonneg_of_le_pi, add_nonneg, EuclideanGeometry.angle_nonneg, le_of_lt, div_pos, Real.pi_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, EuclideanGeometry.angle_le_pi, Eq.mpr, id, Eq, congrArg and 121 more

    165 instances, coercions and auxiliary constants left out.

    Tactic trace: 38 steps

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

  40. lemma Imo2001P1.Imo2001q1Cfg.two_mul_PC_le_circumradius line 489 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, LE.le, Real, HMul.hMul, OfNat.ofNat, Nat, Dist.dist, EuclideanSpace, Fin, ENNReal, Imo2001P1.Imo2001q1Cfg.P, Imo2001P1.Imo2001q1Cfg.C, Affine.Simplex.circumradius, Imo2001P1.Imo2001q1Cfg.ABC

    Proof uses: Eq.mpr, Imo2001P1.Imo2001q1Cfg.A, Real.cos, EuclideanGeometry.angle, id, Eq, congrArg, Imo2001P1.Imo2001q1Cfg.PC_eq, Imo2001P1.Imo2001q1Cfg.B, Imo2001P1.Imo2001q1Cfg.ACP_eq_ACB, Real.sin, Imo2001P1.Imo2001q1Cfg.CA_eq, Trans.trans, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 20 more

    97 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  41. lemma Imo2001P1.Imo2001q1Cfg.PC_lt_PO line 498 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, LT.lt, Real, Dist.dist, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.P, Imo2001P1.Imo2001q1Cfg.C, Imo2001P1.Imo2001q1Cfg.O

    Proof uses: HAdd.hAdd, Eq.mpr, Not, Wbtw, id, Eq, congrArg, propext, dist_lt_dist_add_dist_iff, Imo2001P1.Imo2001q1Cfg.OCP_non_collinear, Collinear.subset, Insert.insert, Set, Singleton.singleton, Wbtw.collinear, Trans.trans, HSub.hSub, LE.le, Affine.Simplex.circumradius, Imo2001P1.Imo2001q1Cfg.ABC and 52 more

    129 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  42. lemma Imo2001P1.Imo2001q1Cfg.COP_le_OCP line 512 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, LT.lt, Real, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.C, Imo2001P1.Imo2001q1Cfg.O, Imo2001P1.Imo2001q1Cfg.P

    Proof uses: Eq.mpr, id, Eq, congrArg, EuclideanGeometry.angle_comm, Dist.dist, propext, EuclideanGeometry.angle_lt_iff_dist_lt, Imo2001P1.Imo2001q1Cfg.OCP_non_collinear, Imo2001P1.Imo2001q1Cfg.PC_lt_PO

    48 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  43. theorem Imo2001P1.Imo2001q1Cfg.result line 517 source

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

    Statement uses: Imo2001P1.Imo2001q1Cfg, LT.lt, Real, HAdd.hAdd, EuclideanGeometry.angle, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Imo2001P1.Imo2001q1Cfg.C, Imo2001P1.Imo2001q1Cfg.A, Imo2001P1.Imo2001q1Cfg.B, Affine.Simplex.circumcenter, Imo2001P1.Imo2001q1Cfg.ABC, Imo2001P1.Imo2001q1Cfg.P, HDiv.hDiv, Real.pi

    Proof uses: Eq.mpr, HSub.hSub, Imo2001P1.Imo2001q1Cfg.O, id, Eq, congrArg, Imo2001P1.Imo2001q1Cfg.CAB_OCP, Trans.trans, add_lt_add_right, Imo2001P1.Imo2001q1Cfg.COP_le_OCP, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, NNRat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat and 43 more

    117 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  44. problem Imo2001P1.imo2001_p1 line 527 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, LT.lt, EuclideanGeometry.angle, HDiv.hDiv, Real.pi, LE.le, HAdd.hAdd, Affine.Triangle, Affine.Simplex.mk, Affine.Simplex.altitudeFoot, Affine.Simplex.circumcenter

    Proof uses: Imo2001P1.Imo2001q1Cfg, Imo2001P1.Imo2001q1Cfg.mk, Imo2001P1.Imo2001q1Cfg.result

    89 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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