`Compfiles/Imo1991P5.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

9 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1991, Problem 5

Let ABC be a triangle and P be an interior point of ABC. Show that at least one of the angles ∠PAB, ∠PBC, ∠PCA is less than or equal to 30°.

Imports (2)

Imported by 1 file

Compfiles.lean

lemma Imo1991P5.mul3_le_add3_div_three_pow_three line 34 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow, Nat, HDiv.hDiv, HAdd.hAdd
Proof uses: Real.geom_mean_le_arith_mean3_weighted, Mathlib.Meta.NormNum.isRat_le_true, Int.ofNat, Mathlib.Meta.NormNum.IsNNRat.to_isRat, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.instAddMonoidWithOne', Mathlib.Meta.NormNum.IsNNRat.to_isNat and 20 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P5.map_mean3_le_mean3_map_of_concaveOn line 48 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real, ConcaveOn, Membership.mem, LE.le, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, Nat
Proof uses: Fin, Eq, rfl, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Finset, Finset.univ, Eq.mpr, id, congrArg, Mathlib.Meta.NormNum.isRat_le_true, Int.ofNat, Mathlib.Meta.NormNum.IsNNRat.to_isRat, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul and 39 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P5.one_div_two_lt_sin line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, HDiv.hDiv, Real.pi, OfNat.ofNat, Nat, HMul.hMul, Real.sin
Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, Real.sin_pi_div_six, dite, Real.sin_lt_sin_of_lt_of_le_pi_div_two, le_of_not_gt, Neg.neg, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow and 74 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem Imo1991P5.analytic_version line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, Eq, HAdd.hAdd, Real.pi, HMul.hMul, Real.sin, Or, HDiv.hDiv, Nat
Proof uses: Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, And, LT.lt, Ne, id, implies_congr, Eq.trans, congr, congrArg, Eq.refl, ne_of_gt, Trans.simple, HPow.hPow, Real.sin_nonneg_of_nonneg_of_le_pi, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub and 107 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
theorem Imo1991P5.trigonometric_ceva Trigonometric Form of Ceva's Theorem line 122 source
Source comment
Trigonometric Form of Ceva's Theorem

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, HMul.hMul, Real.sin, EuclideanGeometry.angle
Proof uses: Ne, Function.Injective.ne, AffineIndependent.injective, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, dite, Or, Eq.mpr, congrArg, EuclideanGeometry.angle_self_of_ne, Ne.symm, Real.sin_zero, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.mul_congr, HAdd.hAdd, HPow.hPow and 71 more
133 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
theorem trigonometric_ceva
    (A B C P : EuclideanSpace ℝ (Fin 2))
    (hABC : AffineIndependent ℝ ![A, B, C])
    : Real.sin (∠ P A B) * Real.sin (∠ P B C) * Real.sin (∠ P C A)
      = Real.sin (∠ A B P) * Real.sin (∠ B C P) * Real.sin (∠ C A P) := by
…
```
Mentions: P
lemma Imo1991P5.angle_eq_angle_add_angle_of_mem_interior line 158 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, Membership.mem, Set, interior, ClosureOperator, convexHull, Insert.insert, Singleton.singleton, Eq, EuclideanGeometry.angle, HAdd.hAdd
Proof uses: AffineSubspace, affineSpan, Set.range, Top.top, Eq.mpr, Submodule, vectorSpan, id, congrArg, propext, AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial, AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one, Fintype.card, Module.finrank, finrank_euclideanSpace, of_eq_true, Eq.trans, True, congr, Fintype.card_congr' and 109 more
246 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P5.affineIndependent_rotate line 207 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
Proof uses: Eq.mpr, Not, Collinear, Insert.insert, Set, Singleton.singleton, id, Eq, congrArg, propext, affineIndependent_iff_not_collinear_set, Set.pair_comm, Set.insert_comm, Eq.mp
56 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P5.sum_angle line 214 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, Membership.mem, Set, interior, ClosureOperator, convexHull, Insert.insert, Singleton.singleton, Eq, HAdd.hAdd, EuclideanGeometry.angle and 1 more
Proof uses: Eq.mpr, id, congrArg, Eq.symm, EuclideanGeometry.angle_add_angle_add_angle_eq_pi, Function.Injective.ne, AffineIndependent.injective, of_decide_eq_true, Ne, Bool, Decidable.decide, Bool.true, Eq.refl, Imo1991P5.angle_eq_angle_add_angle_of_mem_interior, Imo1991P5.affineIndependent_rotate, Eq.mp, Set.pair_comm, Set.insert_comm, Mathlib.Tactic.Ring.of_eq, HMul.hMul and 9 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
problem Imo1991P5.imo1991_p5 line 232 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, Membership.mem, Set, interior, ClosureOperator, convexHull, Insert.insert, Singleton.singleton, Or, LE.le, EuclideanGeometry.angle and 2 more
Proof uses: Eq, HAdd.hAdd, Imo1991P5.sum_angle, HMul.hMul, Real.sin, Imo1991P5.trigonometric_ceva, Imo1991P5.analytic_version, EuclideanGeometry.angle_nonneg
113 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.