`Compfiles/Imo2001P5.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

32 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2001, Problem 5

Let ABC be a triangle. Let AP bisect ∠BAC and let BQ bisect ∠ABC, with P on BC and Q on AC. If AB + BP = AQ + QB and ∠BAC = 60°, what are the angles of the triangle?

Imports (2)

Imported by 1 file

Compfiles.lean

structure Imo2001P5.Setup The problem's configuration line 41 source
Source documentation
The problem's configuration.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor
3 instances, coercions and auxiliary constants left out.
```
structure Setup where
…
```
lemma Imo2001P5.Setup.A_ne_B line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Ne, Imo2001P5.Setup.A, Imo2001P5.Setup.B
Proof uses: id, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.C, HDiv.hDiv, Real.pi, OfNat.ofNat, Nat, Imo2001P5.Setup.BAC_eq, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, HSub.hSub, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo and 69 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.A_ne_C line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Ne, Imo2001P5.Setup.A, Imo2001P5.Setup.C
Proof uses: id, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.B, HDiv.hDiv, Real.pi, OfNat.ofNat, Nat, Imo2001P5.Setup.BAC_eq, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, HSub.hSub, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo and 69 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.B_ne_C line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Ne, Imo2001P5.Setup.B, Imo2001P5.Setup.C
Proof uses: id, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.A, HDiv.hDiv, Real.pi, OfNat.ofNat, Nat, Imo2001P5.Setup.BAC_eq, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, Neg.neg, HSub.hSub, HMul.hMul, inferInstance, AddMonoidWithOne and 72 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.not_collinear_BAC line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Not, Collinear, Insert.insert, Set, Imo2001P5.Setup.B, Imo2001P5.Setup.A, Singleton.singleton, Imo2001P5.Setup.C
Proof uses: Eq.mpr, Or, Eq, Real.sin, EuclideanGeometry.angle, OfNat.ofNat, id, congrArg, And, Eq.trans, False, congrFun', eq_false, Ne.symm, Imo2001P5.Setup.A_ne_B, Imo2001P5.Setup.A_ne_C, HDiv.hDiv, Real.pi, Nat, Imo2001P5.Setup.BAC_eq and 9 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.BAP_eq line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.B, Imo2001P5.Setup.A, Imo2001P5.Setup.P, HDiv.hDiv, Real.pi, OfNat.ofNat, Nat
Proof uses: HAdd.hAdd, Imo2001P5.Setup.C, EuclideanGeometry.angle_add_of_ne_of_ne, Imo2001P5.Setup.A_ne_B, Imo2001P5.Setup.A_ne_C, Imo2001P5.Setup.P_on_BC, Eq.mp, HMul.hMul, congrArg, Imo2001P5.Setup.BAC_eq, Eq.symm, two_mul, Imo2001P5.Setup.AP_bisect_BAC
35 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.PAC_eq line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.P, Imo2001P5.Setup.A, Imo2001P5.Setup.C, HDiv.hDiv, Real.pi, OfNat.ofNat, Nat
Proof uses: HAdd.hAdd, Imo2001P5.Setup.B, EuclideanGeometry.angle_add_of_ne_of_ne, Imo2001P5.Setup.A_ne_B, Imo2001P5.Setup.A_ne_C, Imo2001P5.Setup.P_on_BC, Eq.mp, HMul.hMul, congrArg, Imo2001P5.Setup.BAC_eq, Eq.symm, two_mul, Imo2001P5.Setup.AP_bisect_BAC
35 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.P_ne_B line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Ne, Imo2001P5.Setup.P, Imo2001P5.Setup.B
Proof uses: id, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.A, HDiv.hDiv, Real.pi, OfNat.ofNat, Nat, Imo2001P5.Setup.BAP_eq, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, Neg.neg, HSub.hSub, HMul.hMul, inferInstance, AddMonoidWithOne and 72 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.P_ne_C line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Ne, Imo2001P5.Setup.P, Imo2001P5.Setup.C
Proof uses: id, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.A, HDiv.hDiv, Real.pi, OfNat.ofNat, Nat, Imo2001P5.Setup.PAC_eq, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, Neg.neg, HSub.hSub, HMul.hMul, inferInstance, AddMonoidWithOne and 72 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.sbtw_BPC line 103 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Sbtw, Imo2001P5.Setup.B, Imo2001P5.Setup.P, Imo2001P5.Setup.C
Proof uses: And.intro, Wbtw, And, Ne, Imo2001P5.Setup.P_on_BC, Imo2001P5.Setup.P_ne_B, Imo2001P5.Setup.P_ne_C
20 instances, coercions and auxiliary constants left out.
lemma Imo2001P5.Setup.BPC_eq line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.B, Imo2001P5.Setup.P, Imo2001P5.Setup.C, Real.pi
Proof uses: Eq.mpr, Sbtw, id, congrArg, propext, EuclideanGeometry.angle_eq_pi_iff_sbtw, Imo2001P5.Setup.sbtw_BPC
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2001P5.Setup.x x = ∠ABQ = ∠QBC line 109 source
Source documentation
x = ∠ABQ = ∠QBC. This is the main angle in the solution and it suffices to show this is 2 * π / 9.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup
Proof uses: EuclideanGeometry.angle, Imo2001P5.Setup.A, Imo2001P5.Setup.B, Imo2001P5.Setup.Q
6 instances, coercions and auxiliary constants left out.
```
def x : ℝ := ∠ s.A s.B s.Q
```
lemma Imo2001P5.Setup.ABQ_eq line 111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.A, Imo2001P5.Setup.B, Imo2001P5.Setup.Q, Imo2001P5.Setup.x
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma Imo2001P5.Setup.QBC_eq line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.Q, Imo2001P5.Setup.B, Imo2001P5.Setup.C, Imo2001P5.Setup.x
Proof uses: Eq.mpr, Imo2001P5.Setup.A, id, congrArg, Eq.symm, Imo2001P5.Setup.BQ_bisect_ABC, Imo2001P5.Setup.ABQ_eq, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.ABC_eq line 115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.A, Imo2001P5.Setup.B, Imo2001P5.Setup.C, HMul.hMul, OfNat.ofNat, Nat, Imo2001P5.Setup.x
Proof uses: HAdd.hAdd, Imo2001P5.Setup.Q, EuclideanGeometry.angle_add_of_ne_of_ne, Ne.symm, Imo2001P5.Setup.A_ne_B, Imo2001P5.Setup.B_ne_C, Imo2001P5.Setup.Q_on_AC, Eq.mp, congrArg, Imo2001P5.Setup.QBC_eq, Imo2001P5.Setup.ABQ_eq
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.x_pos line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, LT.lt, OfNat.ofNat, Imo2001P5.Setup.x
Proof uses: Decidable.byContradiction, Not, Eq, le_antisymm, Eq.mp, LE.le, EuclideanGeometry.angle_nonneg, Imo2001P5.Setup.A, Imo2001P5.Setup.B, Imo2001P5.Setup.Q, EuclideanGeometry.angle, Imo2001P5.Setup.C, HMul.hMul, Nat, Imo2001P5.Setup.ABC_eq, Collinear, Insert.insert, Set, Singleton.singleton, EuclideanGeometry.collinear_of_sin_eq_zero and 16 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.Q_ne_A line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Ne, Imo2001P5.Setup.Q, Imo2001P5.Setup.A
Proof uses: id, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.B, Imo2001P5.Setup.x, Imo2001P5.Setup.ABQ_eq, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, LT.lt, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow and 42 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.Q_ne_C line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Ne, Imo2001P5.Setup.Q, Imo2001P5.Setup.C
Proof uses: id, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.B, Imo2001P5.Setup.x, Imo2001P5.Setup.QBC_eq, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, LT.lt, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow and 43 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.sbtw_AQC line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Sbtw, Imo2001P5.Setup.A, Imo2001P5.Setup.Q, Imo2001P5.Setup.C
Proof uses: And.intro, Wbtw, And, Ne, Imo2001P5.Setup.Q_on_AC, Imo2001P5.Setup.Q_ne_A, Imo2001P5.Setup.Q_ne_C
20 instances, coercions and auxiliary constants left out.
lemma Imo2001P5.Setup.AQC_eq line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.A, Imo2001P5.Setup.Q, Imo2001P5.Setup.C, Real.pi
Proof uses: Eq.mpr, Sbtw, id, congrArg, propext, EuclideanGeometry.angle_eq_pi_iff_sbtw, Imo2001P5.Setup.sbtw_AQC
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.ACB_eq line 139 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.A, Imo2001P5.Setup.C, Imo2001P5.Setup.B, HSub.hSub, HDiv.hDiv, HMul.hMul, OfNat.ofNat, Nat, Real.pi, Imo2001P5.Setup.x
Proof uses: HAdd.hAdd, EuclideanGeometry.angle_add_angle_add_angle_eq_pi, Imo2001P5.Setup.B_ne_C, Eq.mp, congrArg, Imo2001P5.Setup.BAC_eq, Imo2001P5.Setup.ABC_eq, EuclideanGeometry.angle_comm
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.x_lt_pi_div_three line 143 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, LT.lt, Imo2001P5.Setup.x, HDiv.hDiv, Real.pi, OfNat.ofNat, Nat
Proof uses: Decidable.byContradiction, Not, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.A, Imo2001P5.Setup.C, Imo2001P5.Setup.B, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Int.rawCast and 90 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.APB_eq line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.A, Imo2001P5.Setup.P, Imo2001P5.Setup.B, HSub.hSub, HDiv.hDiv, HMul.hMul, OfNat.ofNat, Nat, Real.pi, Imo2001P5.Setup.x
Proof uses: HAdd.hAdd, EuclideanGeometry.angle_add_angle_add_angle_eq_pi, Imo2001P5.Setup.A_ne_B, Eq.mp, Imo2001P5.Setup.C, congrArg, Imo2001P5.Setup.ABC_eq, EuclideanGeometry.angle_eq_angle_of_angle_eq_pi, Imo2001P5.Setup.BPC_eq, EuclideanGeometry.angle_comm, Imo2001P5.Setup.BAP_eq
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.AQB_eq line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.A, Imo2001P5.Setup.Q, Imo2001P5.Setup.B, HSub.hSub, HDiv.hDiv, HMul.hMul, OfNat.ofNat, Nat, Real.pi, Imo2001P5.Setup.x
Proof uses: HAdd.hAdd, EuclideanGeometry.angle_add_angle_add_angle_eq_pi, Imo2001P5.Setup.A_ne_B, Eq.mp, congrArg, Imo2001P5.Setup.ABQ_eq, EuclideanGeometry.angle_comm, Imo2001P5.Setup.C, Imo2001P5.Setup.BAC_eq, EuclideanGeometry.angle_eq_angle_of_angle_eq_pi, Imo2001P5.Setup.AQC_eq
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2001P5.Setup.BP_by_AB dist B P in terms of dist A B line 166 source
Source documentation
dist B P in terms of dist A B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, Dist.dist, Imo2001P5.Setup.B, Imo2001P5.Setup.P, HMul.hMul, HDiv.hDiv, Real.sin, Real.pi, OfNat.ofNat, Nat, HSub.hSub, Imo2001P5.Setup.x, Imo2001P5.Setup.A
Proof uses: Eq.mpr, id, congrArg, div_mul_eq_mul_div₀, eq_div_of_mul_eq, LT.lt.ne', Real.sin_pos_of_pos_of_lt_pi, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast and 75 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma BP_by_AB :
    dist s.B s.P = Real.sin (π / 6) / Real.sin (5 * π / 6 - 2 * s.x) * dist s.A s.B := by
…
```
lemma Imo2001P5.Setup.AQ_by_AB dist A Q in terms of dist A B line 174 source
Source documentation
dist A Q in terms of dist A B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, Dist.dist, Imo2001P5.Setup.A, Imo2001P5.Setup.Q, HMul.hMul, HDiv.hDiv, Real.sin, Imo2001P5.Setup.x, HSub.hSub, OfNat.ofNat, Nat, Real.pi, Imo2001P5.Setup.B
Proof uses: Eq.mpr, id, congrArg, div_mul_eq_mul_div₀, eq_div_of_mul_eq, LT.lt.ne', Real.sin_pos_of_pos_of_lt_pi, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast and 76 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma AQ_by_AB :
    dist s.A s.Q = Real.sin s.x / Real.sin (2 * π / 3 - s.x) * dist s.A s.B := by
…
```
lemma Imo2001P5.Setup.QB_by_AB dist Q B in terms of dist A B line 182 source
Source documentation
dist Q B in terms of dist A B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, Dist.dist, Imo2001P5.Setup.Q, Imo2001P5.Setup.B, HMul.hMul, HDiv.hDiv, Real.sin, Real.pi, OfNat.ofNat, Nat, HSub.hSub, Imo2001P5.Setup.x, Imo2001P5.Setup.A
Proof uses: Eq.mpr, id, congrArg, div_mul_eq_mul_div₀, eq_div_of_mul_eq, LT.lt.ne', Real.sin_pos_of_pos_of_lt_pi, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast and 78 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma QB_by_AB :
    dist s.Q s.B = Real.sin (π / 3) / Real.sin (2 * π / 3 - s.x) * dist s.A s.B := by
…
```
lemma Imo2001P5.Setup.key_x_equation The key trigonometric equation for x line 190 source
Source documentation
The key trigonometric equation for x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, HAdd.hAdd, OfNat.ofNat, HDiv.hDiv, Real.sin, Real.pi, Nat, HSub.hSub, HMul.hMul, Imo2001P5.Setup.x
Proof uses: Dist.dist, Imo2001P5.Setup.A, Imo2001P5.Setup.B, Imo2001P5.Setup.P, Imo2001P5.Setup.Q, Imo2001P5.Setup.dist_sum, mul_right_cancel₀, Iff.mpr, Ne, dist_ne_zero, Imo2001P5.Setup.A_ne_B, Eq.mp, congrArg, Eq.symm, add_div, add_mul, Imo2001P5.Setup.QB_by_AB, Imo2001P5.Setup.AQ_by_AB, one_add_mul, Imo2001P5.Setup.BP_by_AB
59 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma key_x_equation :
    1 + Real.sin (π / 6) / Real.sin (5 * π / 6 - 2 * s.x) =
    (Real.sin s.x + Real.sin (π / 3)) / Real.sin (2 * π / 3 - s.x) := by
…
```
lemma Imo2001P5.Setup.x_eq line 199 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, Eq, Imo2001P5.Setup.x, HDiv.hDiv, HMul.hMul, OfNat.ofNat, Nat, Real.pi
Proof uses: HAdd.hAdd, Real.sin, HSub.hSub, Imo2001P5.Setup.key_x_equation, Eq.mpr, id, congrArg, mul_div_assoc, mul_comm, Eq.symm, propext, div_eq_iff, two_ne_zero, rfl, Real.cos, Real.cos_add_cos, Ne, mul_div_cancel₀, LT.lt.ne, Imo2001P5.Setup.x_lt_pi_div_three and 146 more
155 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
determine Imo2001P5.solution_ABC line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HDiv.hDiv, HMul.hMul, OfNat.ofNat, Real.pi
9 instances, coercions and auxiliary constants left out.
determine Imo2001P5.solution_ACB line 236 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HDiv.hDiv, HMul.hMul, OfNat.ofNat, Real.pi
9 instances, coercions and auxiliary constants left out.
problem Imo2001P5.imo2001_p5 line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Imo2001P5.Setup, And, Eq, EuclideanGeometry.angle, Imo2001P5.Setup.A, Imo2001P5.Setup.B, Imo2001P5.Setup.C, Imo2001P5.solution_ABC, Imo2001P5.solution_ACB
Proof uses: Eq.mpr, HMul.hMul, OfNat.ofNat, Nat, Imo2001P5.Setup.x, id, congrArg, Imo2001P5.Setup.ABC_eq, HSub.hSub, HDiv.hDiv, Real.pi, Imo2001P5.Setup.ACB_eq, Imo2001P5.Setup.x_eq, And.intro, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast, NNRat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr and 50 more
68 instances, coercions and auxiliary constants left out.

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