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

25 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1970, Problem 6

In a plane there are 100 points, no three of which are collinear. Consider all possible triangles having these points as vertices. Prove that no more that 70% of these triangles are acute.

Imports (2)

Imported by 1 file

Compfiles.lean

abbrev Imo1970P6.Pt line 30 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
def Imo1970P6.NC Abbreviation for the noncollinearity hypothesis on a triple of points line 52 source
Source documentation
Abbreviation for the noncollinearity hypothesis on a triple of points.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt
Proof uses: Not, Collinear, Real, OfNat.ofNat, ENNReal, Fin, Nat, Insert.insert, Set, Singleton.singleton
30 instances, coercions and auxiliary constants left out.
```
def NC (x y z : Pt) : Prop := ¬ Collinear ℝ ({x, y, z} : Set Pt)
```
Mentions: Imo1970P6.Pt
lemma Imo1970P6.NC.swap₁₂ line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Imo1970P6.NC
Proof uses: id, Eq.mpr, Not, Collinear, Real, OfNat.ofNat, ENNReal, Fin, Nat, Insert.insert, Set, Singleton.singleton, Eq, congrArg, Set.insert_comm
30 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1970P6.NC.swap₂₃ line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Imo1970P6.NC
Proof uses: id, Eq.mpr, Not, Collinear, Real, OfNat.ofNat, ENNReal, Fin, Nat, Insert.insert, Set, Singleton.singleton, Eq, congrArg, Set.pair_comm
30 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1970P6.NC.ne₁₂ line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Imo1970P6.NC, Ne
Proof uses: Eq, False, Eq.mp, Not, Collinear, Real, OfNat.ofNat, ENNReal, Fin, Nat, Insert.insert, Set, Singleton.singleton, congrArg, Set.insert_idem, Imo1970P6.NC.eq_1, collinear_pair
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1970P6.NC.ne₂₃ line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Imo1970P6.NC, Ne
Proof uses: Imo1970P6.NC.ne₁₂, Imo1970P6.NC.swap₂₃, Imo1970P6.NC.swap₁₂
lemma Imo1970P6.NC.ne₁₃ line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Imo1970P6.NC, Ne
Proof uses: Imo1970P6.NC.ne₁₂, Imo1970P6.NC.swap₂₃
def Imo1970P6.Bad The triple of points X, Y, Z has an angle of at least π / 2 (at X, at Y, or at Z respectively) line 73 source
Source documentation
The triple of points X, Y, Z has an angle of at least π / 2 (at X, at Y, or at Z respectively).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt
Proof uses: Or, LE.le, Real, HDiv.hDiv, Real.pi, OfNat.ofNat, EuclideanGeometry.angle, ENNReal, Fin, Nat
28 instances, coercions and auxiliary constants left out.
```
def Bad (X Y Z : Pt) : Prop :=
…
```
Mentions: Imo1970P6.Pt
lemma Imo1970P6.Bad.swap₁₂ line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Imo1970P6.Bad
Proof uses: id, LE.le, Real, HDiv.hDiv, Real.pi, OfNat.ofNat, EuclideanGeometry.angle, ENNReal, Fin, Nat, Or, Eq.mp, congrArg, EuclideanGeometry.angle_comm, Iff.mpr, Not, Classical.or_iff_not_imp_left, False.elim
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1970P6.Bad.swap₂₃ line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Imo1970P6.Bad
Proof uses: id, LE.le, Real, HDiv.hDiv, Real.pi, OfNat.ofNat, EuclideanGeometry.angle, ENNReal, Fin, Nat, Or, Eq.mp, congrArg, EuclideanGeometry.angle_comm, Iff.mpr, Not, Classical.or_iff_not_imp_left, False.elim
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1970P6.inner_pos_of_angle_lt line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Ne, OfNat.ofNat, ENNReal, Fin, Nat, Real, LT.lt, InnerProductGeometry.angle, HDiv.hDiv, Real.pi, Inner.inner
Proof uses: Real.cos, Real.cos_pos_of_mem_Ioo, And.intro, Neg.neg, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast and 76 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo1970P6.hull_case If A is a combination of B, C, D with positive weights (an interior point of the triangle B C D), then the angles ∠ B A C and ∠ B A D cannot both be acute line 96 source
Source documentation
If A is a combination of B, C, D with positive weights (an interior point of the triangle B C D), then the angles ∠ B A C and ∠ B A D cannot both be acute.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Ne, Real, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, ENNReal, Fin, Nat, HSMul.hSMul, HSub.hSub, Or, LE.le, HDiv.hDiv, Real.pi, EuclideanGeometry.angle
Proof uses: Decidable.byContradiction, Not, And, False, Eq.mp, Eq.trans, congr, congrArg, Iff.mpr, sub_ne_zero, Ne.symm, Inner.inner, Imo1970P6.inner_pos_of_angle_lt, Eq.mpr, id, inner_zero_right, Eq.refl, real_inner_self_pos, False.elim, Mathlib.Tactic.Linarith.lt_irrefl and 51 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma hull_case {A B C D : Pt} (hAB : A ≠ B) (hAC : A ≠ C) (hAD : A ≠ D)
    {wb wc wd : ℝ} (hwb : 0 < wb) (hwc : 0 < wc) (hwd : 0 < wd)
    (hvec : wb • (B - A) + wc • (C - A) + wd • (D - A) = 0) :
    π / 2 ≤ ∠ B A C ∨ π / 2 ≤ ∠ B A D := by
…
```
Mentions: Imo1970P6.Pt
lemma Imo1970P6.quad_case Documented declaration: quad_case line 120 source
Source documentation
If the segments A C and B D cross, then one of the angles of the quadrilateral A B C D is at least π / 2; each of those four angles is an angle of one of the four triangles on the points A, B, C, D.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Sbtw, Real, OfNat.ofNat, ENNReal, Fin, Nat, Ne, Or, LE.le, HDiv.hDiv, Real.pi, EuclideanGeometry.angle
Proof uses: Decidable.byContradiction, Not, LT.lt, And, False, Eq.mp, Eq.trans, congr, congrArg, Eq, HAdd.hAdd, Eq.symm, EuclideanGeometry.angle_add_angle_eq_of_sbtw, Sbtw.angle_eq_right, Sbtw.angle_eq_left, Sbtw.symm, Eq.mpr, id, EuclideanGeometry.angle_comm, EuclideanGeometry.angle_add_angle_add_angle_eq_pi and 79 more
153 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma quad_case {A B C D Q : Pt} (hAC : Sbtw ℝ A Q C) (hBD : Sbtw ℝ B Q D)
    (hBA : B ≠ A) (hDC : D ≠ C) :
    π / 2 ≤ ∠ B A D ∨ π / 2 ≤ ∠ A B C ∨ π / 2 ≤ ∠ B C D ∨ π / 2 ≤ ∠ C D A := by
…
```
Mentions: Imo1970P6.Pt
lemma Imo1970P6.crossing_lemma From an affine dependence with two positive and two negative weights, produce the crossing point of the two segments line 142 source
Source documentation
From an affine dependence with two positive and two negative weights, produce the crossing point of the two segments.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Real, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, ENNReal, Fin, Nat, HSMul.hSMul, Ne, Exists, And, Sbtw
Proof uses: rfl, add_pos', Exists.intro, AffineMap, AffineMap.lineMap, HDiv.hDiv, And.intro, Eq.mpr, Membership.mem, Set, Set.Ioo, id, congrArg, propext, sbtw_lineMap_iff, div_pos, Iff.mpr, div_lt_one, lt_of_not_ge, LE.le and 101 more
225 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma crossing_lemma {X Y Z W : Pt} {a b c d : ℝ} (ha : 0 < a) (hb : 0 < b)
    (hc : c < 0) (hd : d < 0) (hsum : a + b + c + d = 0)
    (hvec : a • X + b • Y + c • Z + d • W = 0) (hXY : X ≠ Y) (hZW : Z ≠ W) :
    ∃ Q, Sbtw ℝ X Q Y ∧ Sbtw ℝ Z Q W := by
…
```
Mentions: Imo1970P6.Pt
lemma Imo1970P6.collinear_of_dependent An affine dependence between three points means they are collinear line 172 source
Source documentation
An affine dependence between three points means they are collinear.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Real, Eq, HAdd.hAdd, OfNat.ofNat, ENNReal, Fin, Nat, HSMul.hSMul, Not, And, Collinear, Insert.insert, Set, Singleton.singleton
Proof uses: Classical.byContradiction, AffineIndependent, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Iff.mpr, affineIndependent_iff_not_collinear_set, Finset.sum, Finset.univ, Eq.mpr, id, congrArg, Fin.sum_univ_three, Eq.mp, LinearMap, RingHom.id, Finset.weightedVSub, propext, affineIndependent_iff_of_fintype, Finset.weightedVSub_eq_linear_combination and 1 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma collinear_of_dependent {X Y Z : Pt} {a b c : ℝ}
    (hvec : a • X + b • Y + c • Z = 0) (hsum : a + b + c = 0)
    (hne : ¬ (a = 0 ∧ b = 0 ∧ c = 0)) : Collinear ℝ ({X, Y, Z} : Set Pt) := by
…
```
Mentions: Imo1970P6.Pt
lemma Imo1970P6.four_point_aux The core sign-analysis: given an affine dependence with all weights nonzero and the first one positive, some triple of the four points is Bad line 188 source
Source documentation
The core sign-analysis: given an affine dependence with all weights nonzero and the first one positive, some triple of the four points is Bad.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Imo1970P6.NC, Fin, OfNat.ofNat, Nat, Real, Eq, HAdd.hAdd, ENNReal, HSMul.hSMul, Ne, LT.lt, Or, Imo1970P6.Bad
Proof uses: Eq.mpr, id, congrArg, Eq.refl, lt_or_gt_of_ne, Neg.neg, HSub.hSub, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.add_eq_eq, Eq.symm, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval, Mathlib.Tactic.Module.NF.cons, Prod.mk, HMul.hMul, RingHom, Int, Algebra.algebraMap, List.nil, Prod and 103 more
188 instances, coercions and auxiliary constants left out.

Tactic trace: 99 steps
Open to load the checked before-and-after goal states.
```
lemma four_point_aux {A B C D : Pt} (h₁ : NC A B C) (h₂ : NC A B D)
    (h₃ : NC A C D) (w : Fin 4 → ℝ)
    (hw0 : w 0 + w 1 + w 2 + w 3 = 0)
    (hvec : w 0 • A + w 1 • B + w 2 • C + w 3 • D = 0)
    (hall : ∀ j, w j ≠ 0) (hpos : 0 < w 0) :
    Bad A B C ∨ Bad A B D ∨ Bad A C D ∨ Bad B C D := by
…
```
Mentions: Imo1970P6.Pt, Imo1970P6.NC, Imo1970P6.Bad
lemma Imo1970P6.four_point Among four points in the plane, no three of which are collinear, some triple forms a triangle with an angle of at least π / 2 line 261 source
Source documentation
Among four points in the plane, no three of which are collinear, some triple forms a triangle with an angle of at least π / 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1970P6.Pt, Imo1970P6.NC, Or, Imo1970P6.Bad
Proof uses: Not, AffineIndependent, Real, OfNat.ofNat, ENNReal, Fin, Nat, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LE.le, Fintype.card, HAdd.hAdd, Module.finrank, Subtype, Membership.mem, Submodule, vectorSpan, Set.range, AffineIndependent.card_le_finrank_succ and 146 more
172 instances, coercions and auxiliary constants left out.

Tactic trace: 81 steps
Open to load the checked before-and-after goal states.
```
lemma four_point {A B C D : Pt} (h₁ : NC A B C) (h₂ : NC A B D)
    (h₃ : NC A C D) (h₄ : NC B C D) :
    Bad A B C ∨ Bad A B D ∨ Bad A C D ∨ Bad B C D := by
…
```
Mentions: Imo1970P6.Pt, Imo1970P6.NC, Imo1970P6.Bad
def Imo1970P6.AcuteSet The predicate from the problem statement: the 3-element subset w of indices spans an acute-angled triangle line 332 source
Source documentation
The predicate from the problem statement: the 3-element subset w of indices spans an acute-angled triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo1970P6.Pt, Finset
Proof uses: Exists, And, Eq, Insert.insert, Singleton.singleton, Affine.Triangle, Real, ENNReal, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Affine.Simplex.points, Affine.Simplex.AcuteAngled
37 instances, coercions and auxiliary constants left out.
```
def AcuteSet (P : Fin 100 → Pt) (w : Finset (Fin 100)) : Prop :=
…
```
Mentions: P, Imo1970P6.Pt
lemma Imo1970P6.triple_perm line 336 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, Eq, Finset, Insert.insert, Singleton.singleton, Or, And
Proof uses: Iff, Eq.mp, Eq.trans, Membership.mem, forall_congr, congr, congrArg
14 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo1970P6.not_acuteSet_of_bad line 346 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo1970P6.Pt, Ne, Imo1970P6.Bad, Not, Imo1970P6.AcuteSet, Insert.insert, Finset, Singleton.singleton
Proof uses: Exists, And, Eq, Affine.Triangle, Real, ENNReal, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, Affine.Simplex.points, Affine.Simplex.AcuteAngled, False, Or, Imo1970P6.triple_perm, Imo1970P6.Bad.swap₂₃, Imo1970P6.Bad.swap₁₂, LE.le, HDiv.hDiv, Real.pi, EuclideanGeometry.angle and 85 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
lemma Imo1970P6.exists_nonacute_triple Among any four of the points, some three of them form a non-acute triangle line 370 source
Source documentation
Among any four of the points, some three of them form a non-acute triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo1970P6.Pt, List.Nodup, List.cons, List.nil, Not, Collinear, Real, ENNReal, Insert.insert, Set, Singleton.singleton, Finset, Eq, Finset.card, Exists, And, LE.le and 1 more
Proof uses: Ne, Iff.mp, Finset.card_eq_four, Imo1970P6.NC, of_eq_true, Eq.trans, Membership.mem, List, True, congr, congrArg, False, Or, eq_false, or_self, not_false_eq_true, and_self, Imo1970P6.Bad, Imo1970P6.four_point, Exists.intro and 9 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma exists_nonacute_triple {P : Fin 100 → Pt}
    (hP : ∀ a b c : Fin 100, List.Nodup [a, b, c] → ¬ Collinear ℝ {P a, P b, P c})
    {s : Finset (Fin 100)} (hs : s.card = 4) :
    ∃ w : Finset (Fin 100), w ⊆ s ∧ w.card = 3 ∧ ¬ AcuteSet P w := by
…
```
Mentions: P, Imo1970P6.Pt, Imo1970P6.AcuteSet
lemma Imo1970P6.card_supersets The number of (w.card + k)-element subsets of s containing a fixed w ⊆ s is (s.card - w.card).choose k line 395 source
Source documentation
The number of (w.card + k)-element subsets of s containing a fixed w ⊆ s is (s.card - w.card).choose k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Fin, OfNat.ofNat, Nat, LE.le, Eq, Finset.card, Finset.filter, Finset.powersetCard, HAdd.hAdd, Nat.choose, HSub.hSub
Proof uses: Eq.mpr, SDiff.sdiff, id, congrArg, Eq.symm, Finset.card_sdiff_of_subset, Finset.card_powersetCard, Finset.card_bij', Membership.mem, Union.union, And, propext, Finset.mem_powersetCard, And.intro, Finset.sdiff_subset_sdiff, And.left, Eq.mp, Finset.mem_filter, Finset.Subset.refl, And.right and 12 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma card_supersets {w s : Finset (Fin 100)} (hws : w ⊆ s) (k : ℕ) :
    ((s.powersetCard (w.card + k)).filter (fun u => w ⊆ u)).card =
      (s.card - w.card).choose k := by
…
```
lemma Imo1970P6.five_point_bound Among any five of the points, at least three of the ten 3-element subsets form a non-acute triangle line 424 source
Source documentation
Among any five of the points, at least three of the ten 3-element subsets form a non-acute triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo1970P6.Pt, List.Nodup, List.cons, List.nil, Not, Collinear, Real, ENNReal, Insert.insert, Set, Singleton.singleton, Finset, Eq, Finset.card, LE.le, Finset.filter, Imo1970P6.AcuteSet and 2 more
Proof uses: Exists, And, dite, Imo1970P6.exists_nonacute_triple, Exists.intro, And.intro, EmptyCollection.emptyCollection, absurd, Finset.image, Membership.mem, Iff.mp, Finset.mem_image, And.right, Eq.mp, congrArg, propext, Finset.mem_powersetCard, Eq.mpr, id, Finset.mem_filter and 19 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma five_point_bound {P : Fin 100 → Pt}
    (hP : ∀ a b c : Fin 100, List.Nodup [a, b, c] → ¬ Collinear ℝ {P a, P b, P c})
    {s : Finset (Fin 100)} (hs : s.card = 5) :
    3 ≤ ((s.powersetCard 3).filter (fun w => ¬ AcuteSet P w)).card := by
…
```
Mentions: P, Imo1970P6.Pt, Imo1970P6.AcuteSet
lemma Imo1970P6.global_bound Globally, at least 3 * (100.choose 5) / (97.choose 2) = 48510 of the 3-element subsets form a non-acute triangle line 473 source
Source documentation
Globally, at least 3 * (100.choose 5) / (97.choose 2) = 48510 of the 3-element subsets form a non-acute triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo1970P6.Pt, List.Nodup, List.cons, List.nil, Not, Collinear, Real, ENNReal, Insert.insert, Set, Singleton.singleton, LE.le, Finset.card, Finset, Finset.filter, Imo1970P6.AcuteSet, Classical.propDecidable and 2 more
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, Finset.sum, Finset.bipartiteAbove, Finset.bipartiteBelow, Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow, Membership.mem, And, Eq.mp, propext, Finset.mem_powersetCard, Finset.mem_filter, HAdd.hAdd, Eq.refl, Nat.choose, HSub.hSub, Imo1970P6.card_supersets and 32 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
lemma global_bound {P : Fin 100 → Pt}
    (hP : ∀ a b c : Fin 100, List.Nodup [a, b, c] → ¬ Collinear ℝ {P a, P b, P c}) :
    48510 ≤ (((univ : Finset (Fin 100)).powersetCard 3).filter
      (fun w => ¬ AcuteSet P w)).card := by
…
```
Mentions: P, Imo1970P6.Pt, Imo1970P6.AcuteSet
problem Imo1970P6.imo1970_p6 line 532 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo1970P6.Pt, List.Nodup, List.cons, List.nil, Not, Collinear, Real, ENNReal, Insert.insert, Set, Singleton.singleton, Nat.card, Finset, Set.ofPred, Eq, Finset.card, And and 10 more
Proof uses: Finset.powersetCard, Finset.univ, Eq.mpr, Nat.choose, id, congrArg, Finset.card_powersetCard, Finset.card_fin, Nat.descFactorial, Nat.factorial, Nat.choose_eq_descFactorial_div_factorial, Eq.refl, Nat.subtype_card, Membership.mem, of_eq_true, Iff, Eq.trans, True, congrFun', true_and and 28 more
151 instances, coercions and auxiliary constants left out.

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