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

28 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2010, Problem 2

There are $n$ students standing in a circle, one behind the other. The students have heights $h_1 < h_2 < \dots < h_n$. If a student with height $h_k$ is standing directly behind a student with height $h_{k-2}$ or less, the two students are permitted to switch places. Prove that it is not possible to make more than $\binom{n}{3}$ such switches before reaching a position in which no further switches are possible.

Imports (4)

Imported by 1 file

Compfiles.lean

def Usa2010P2.Legal A sequence of permitted switches starting from configuration e line 55 source

Source documentation

A sequence of permitted switches starting from configuration e.

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

Statement uses: Nat, Equiv, Fin, ZMod, List

2 instances, coercions and auxiliary constants left out.

def Legal {n : ℕ} : (Fin n ≃ ZMod n) → List (ZMod n) → Prop
  | _, [] => True
  | e, p :: ps =>
      (e.symm p).val + 2 ≤ (e.symm (p + 1)).val ∧
      Legal (e.trans (Equiv.swap p (p + 1))) ps

/-- The sequence of pairs of students that switch places: each entry is
`(student in front, student behind)`, with front rank `<` behind rank. -/

def Usa2010P2.evPairs The sequence of pairs of students that switch places: each entry is (student in front, student behind), with front rank < behind rank line 63 source
Source documentation
The sequence of pairs of students that switch places: each entry is (student in front, student behind), with front rank < behind rank.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Fin, ZMod, List, Prod
2 instances, coercions and auxiliary constants left out.
```
def evPairs {n : ℕ} : (Fin n ≃ ZMod n) → List (ZMod n) → List (Fin n × Fin n)
  | _, [] => []
  | e, p :: ps =>
      (e.symm p, e.symm (p + 1)) :: evPairs (e.trans (Equiv.swap p (p + 1))) ps

/-- The cyclic-order state of a triple of students: going backwards from `a`
we meet `b` before meeting `c`. -/
```
def Usa2010P2.StateA The cyclic-order state of a triple of students: going backwards from a we meet b before meeting c line 70 source
Source documentation
The cyclic-order state of a triple of students: going backwards from a we meet b before meeting c.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Equiv, Fin, ZMod
Proof uses: LT.lt, ZMod.val, HSub.hSub
11 instances, coercions and auxiliary constants left out.
```
def StateA {n : ℕ} (e : Fin n ≃ ZMod n) (a b c : Fin n) : Prop :=
…
```
instance Usa2010P2.(instance at line 73) line 73 source
lemma Usa2010P2.val_one' line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, ZMod.val, ZMod
Proof uses: NeZero, NeZero.mk, Eq.mpr, id, congrArg, Eq.symm, Nat.cast_one, ZMod.val_natCast_of_lt
22 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P2.val_neg_one' line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, ZMod.val, Neg.neg, ZMod, HSub.hSub
Proof uses: NeZero, NeZero.mk, Eq.mpr, id, congrArg, Nat.cast_sub, Nat.cast_one, ZMod.natCast_self, zero_sub, Eq.refl, ZMod.val_natCast_of_lt
50 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P2.val_add_one' line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, ZMod, Ne, Neg.neg, Eq, ZMod.val, HAdd.hAdd
Proof uses: NeZero, NeZero.mk, LT.lt, ZMod.val_lt, HSub.hSub, ZMod.val_injective, Eq.mpr, id, congrArg, Usa2010P2.val_neg_one', HMod.hMod, ZMod.val_add, Usa2010P2.val_one', Nat.mod_eq_of_lt, Eq.refl
51 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P2.val_sub_one' line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, ZMod, Ne, Eq, ZMod.val, HSub.hSub
Proof uses: NeZero, NeZero.mk, Iff.mp, ZMod.val_eq_zero, LT.lt, ZMod.val_lt, Eq.mpr, HAdd.hAdd, Neg.neg, id, congrArg, sub_eq_add_neg, HMod.hMod, ZMod.val_add, Usa2010P2.val_neg_one', Nat.add_mod_right, Nat.mod_eq_of_lt, Eq.refl
58 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P2.val_sub_ne_of_ne line 110 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, Ne, ZMod.val, HSub.hSub
Proof uses: Eq, Iff.mp, sub_left_inj, ZMod.val_injective
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P2.val_sub_pos_of_ne line 115 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, NeZero, ZMod, Ne, LE.le, OfNat.ofNat, ZMod.val, HSub.hSub
Proof uses: sub_ne_zero_of_ne, Eq, Iff.mp, ZMod.val_eq_zero, Iff.mpr, Nat.one_le_iff_ne_zero
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P2.eq_of_sub_eq_neg_one line 121 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, ZMod, Eq, HSub.hSub, Neg.neg, OfNat.ofNat, HAdd.hAdd
Proof uses: Iff.mp, sub_eq_iff_eq_add, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Meta.NormNum.IsInt.to_raw_eq and 17 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P2.stateA_of_pair L1: if b is directly behind a, then going backwards from a we meet b before any third student c line 130 source
Source documentation
L1: if b is directly behind a, then going backwards from a we meet b before any third student c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Equiv, ZMod, Eq, HAdd.hAdd, Ne, Usa2010P2.StateA
Proof uses: NeZero, NeZero.mk, ZMod.val, HSub.hSub, Eq.mpr, id, congrArg, add_sub_cancel_left, Usa2010P2.val_one', Usa2010P2.val_sub_pos_of_ne, Eq.symm, Equiv.injective, ZMod.val_injective, Iff.mp, sub_eq_iff_eq_add, add_comm, Eq.refl, LT.lt
51 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma stateA_of_pair {n : ℕ} (hn : 2 ≤ n) {a b c : Fin n} {e : Fin n ≃ ZMod n} {p : ZMod n}
    (hea : e a = p) (heb : e b = p + 1) (hac : a ≠ c) (hbc : b ≠ c) :
    StateA e a b c := by
…
```
Mentions: Usa2010P2.StateA
lemma Usa2010P2.not_stateA_of_pair L2: if b is directly behind c, the triple is not in state A line 152 source
Source documentation
L2: if b is directly behind c, the triple is not in state A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Equiv, ZMod, Eq, HAdd.hAdd, Ne, Not, Usa2010P2.StateA
Proof uses: NeZero, NeZero.mk, LT.lt, ZMod.val, HSub.hSub, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HMul.hMul, HPow.hPow, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 28 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma not_stateA_of_pair {n : ℕ} (hn : 2 ≤ n) {a b c : Fin n} {e : Fin n ≃ ZMod n} {p : ZMod n}
    (hec : e c = p) (heb : e b = p + 1) (hab : a ≠ b) :
    ¬ StateA e a b c := by
…
```
Mentions: Usa2010P2.StateA
lemma Usa2010P2.not_stateA_swap L3: after b (behind) and a (front) switch, the triple is not in state A line 169 source
Source documentation
L3: after b (behind) and a (front) switch, the triple is not in state A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Equiv, ZMod, Eq, HAdd.hAdd, Ne, Not, Usa2010P2.StateA, Equiv.trans, Equiv.swap
Proof uses: NeZero, NeZero.mk, Eq.mpr, id, congrArg, Equiv.trans_apply, Equiv.swap_apply_left, Equiv.swap_apply_right, Equiv.injective, Eq.trans, Eq.symm, Equiv.Perm, Equiv.swap_apply_of_ne_of_ne, Eq.refl, HSub.hSub, Neg.neg, Mathlib.Tactic.Ring.of_eq, Int.rawCast, inferInstance, Ring and 38 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma not_stateA_swap {n : ℕ} (hn : 2 ≤ n) {a b c : Fin n} {e : Fin n ≃ ZMod n} {p : ZMod n}
    (hea : e a = p) (heb : e b = p + 1) (hca : c ≠ a) (hcb : c ≠ b) :
    ¬ StateA (e.trans (Equiv.swap p (p + 1))) a b c := by
…
```
Mentions: Usa2010P2.StateA
lemma Usa2010P2.stateA_swap L4: after b (behind) and c (front) switch, the triple is in state A line 198 source
Source documentation
L4: after b (behind) and c (front) switch, the triple is in state A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Equiv, ZMod, Eq, HAdd.hAdd, Ne, Usa2010P2.StateA, Equiv.trans, Equiv.swap
Proof uses: NeZero, NeZero.mk, Eq.mpr, id, congrArg, Equiv.trans_apply, Equiv.swap_apply_left, Equiv.swap_apply_right, Equiv.injective, Eq.trans, Eq.symm, Equiv.Perm, Equiv.swap_apply_of_ne_of_ne, Eq.refl, LT.lt, ZMod.val, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HMul.hMul and 30 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma stateA_swap {n : ℕ} (hn : 2 ≤ n) {a b c : Fin n} {e : Fin n ≃ ZMod n} {p : ZMod n}
    (hec : e c = p) (heb : e b = p + 1) (hac : a ≠ c) (hab : a ≠ b) :
    StateA (e.trans (Equiv.swap p (p + 1))) a b c := by
…
```
Mentions: Usa2010P2.StateA
lemma Usa2010P2.stateA_swap_iff L5: a permitted switch that involves neither the pair (a, b) nor the pair (c, b) preserves the cyclic-order state of the triple {a, c, b} line 224 source
Source documentation
L5: a permitted switch that involves neither the pair (a, b) nor the pair (c, b) preserves the cyclic-order state of the triple {a, c, b}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Equiv, ZMod, Eq, HAdd.hAdd, LT.lt, Equiv.symm, Ne, Prod, Prod.mk, Iff, Usa2010P2.StateA, Equiv.trans, Equiv.swap
Proof uses: NeZero, NeZero.mk, Fin.isLt, Eq.mp, congrArg, lt_irrefl, ZMod.val, HSub.hSub, Usa2010P2.val_sub_ne_of_ne, Eq.symm, Equiv.injective, Usa2010P2.val_sub_pos_of_ne, Eq.mpr, id, rfl, Equiv.apply_symm_apply, dite, And, Prod.mk.injEq, And.intro and 50 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 246 steps (first 200 of 246)
Open to load the checked before-and-after goal states.
```
lemma stateA_swap_iff {n : ℕ} (hn : 2 ≤ n) {a b c : Fin n} {e : Fin n ≃ ZMod n} {p : ZMod n}
    (hc : c.val = a.val + 1) (hab : a.val + 2 ≤ b.val) (hcb : c.val < b.val)
    (hleg : (e.symm p).val + 2 ≤ (e.symm (p + 1)).val)
    (hJ : (e.symm p, e.symm (p + 1)) ≠ (a, b))
    (hM : (e.symm p, e.symm (p + 1)) ≠ (c, b)) :
    StateA (e.trans (Equiv.swap p (p + 1))) a b c ↔ StateA e a b c := by
…
```
Mentions: Usa2010P2.StateA
def Usa2010P2.fsucc The student of rank one higher than a (well-defined when a is not the tallest student) line 424 source
Source documentation
The student of rank one higher than a (well-defined when a is not the tallest student). Defined as a literal so that (fsucc a h).val is definitionally a.val + 1.

no axioms what this means
Statement uses: Nat, Fin, LT.lt, HAdd.hAdd, OfNat.ofNat
Proof uses: Fin.mk
10 instances, coercions and auxiliary constants left out.
```
def fsucc {n : ℕ} (a : Fin n) (h : a.val + 1 < n) : Fin n := ⟨a.val + 1, h⟩
```
Mentions: h
lemma Usa2010P2.evPairs_le Every recorded switch has front rank + 2 ≤ behind rank line 427 source
Source documentation
Every recorded switch has front rank + 2 ≤ behind rank.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Fin, ZMod, List, Usa2010P2.Legal, Prod, Membership.mem, Usa2010P2.evPairs, LE.le, HAdd.hAdd, Prod.fst, OfNat.ofNat, Prod.snd
Proof uses: List.rec, List.nil, False.elim, List.not_mem_nil, List.cons, Equiv.symm, Equiv.trans, Equiv.swap, And, Eq, Prod.mk, Or, Eq.mp, Eq.mpr, id, congrArg
29 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma evPairs_le {n : ℕ} {e : Fin n ≃ ZMod n} {ps : List (ZMod n)} (hL : Legal e ps) :
    ∀ pr ∈ evPairs e ps, pr.1.val + 2 ≤ pr.2.val := by
…
```
Mentions: Usa2010P2.Legal, Usa2010P2.evPairs
lemma Usa2010P2.evPairs_lt Every recorded switch has front rank < behind rank line 442 source
Source documentation
Every recorded switch has front rank < behind rank.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Fin, ZMod, List, Usa2010P2.Legal, Prod, Membership.mem, Usa2010P2.evPairs, LT.lt, Prod.fst, Prod.snd
Proof uses: LE.le, HAdd.hAdd, OfNat.ofNat, Usa2010P2.evPairs_le, Iff.mpr, Fin.lt_def
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma evPairs_lt {n : ℕ} {e : Fin n ≃ ZMod n} {ps : List (ZMod n)} (hL : Legal e ps) :
    ∀ pr ∈ evPairs e ps, pr.1 < pr.2 := by
…
```
Mentions: Usa2010P2.Legal, Usa2010P2.evPairs
lemma Usa2010P2.length_evPairs line 448 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Fin, ZMod, List, Eq, List.length, Prod, Usa2010P2.evPairs
Proof uses: List.rec, Eq.refl, List.nil, of_eq_true, List.cons, HAdd.hAdd, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, Equiv.trans, Equiv.swap, eq_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P2.length_eq_sum_count The length of a list of pairs with fst < snd equals the sum of the counts over all such pairs line 456 source
Source documentation
The length of a list of pairs with fst < snd equals the sum of the counts over all such pairs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Prod, Fin, Membership.mem, LT.lt, Prod.fst, Prod.snd, Eq, List.length, Finset.sum, Finset.filter, Finset.univ, List.count
Proof uses: List.rec, List.nil, of_eq_true, OfNat.ofNat, Eq.trans, True, congrArg, Finset.sum_const_zero, eq_self, List.cons, List.mem_cons_self, List.mem_cons_of_mem, Eq.mpr, HAdd.hAdd, id, List.length_cons, ite, Bool, BEq.beq, Bool.true and 26 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma length_eq_sum_count {n : ℕ} (L : List (Fin n × Fin n))
    (hL : ∀ pr ∈ L, pr.1 < pr.2) :
    L.length = ∑ pr ∈ (Finset.univ.filter (fun pr : Fin n × Fin n => pr.1 < pr.2)),
      L.count pr := by
…
```
lemma Usa2010P2.alternation The key alternation lemma line 499 source
Source documentation
The key alternation lemma. Along any legal sequence of switches, the switches of the pair (a, b) and those of the pair (a+1, b) alternate, and every switch of (a, b) after the first one is preceded by a switch of (a+1, b). Consequently the two displayed inequalities hold (the first conjunct applies when the initial cyclic-order state is A, the second when it is not).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, HAdd.hAdd, LT.lt, Equiv, ZMod, List, Usa2010P2.Legal, And, Usa2010P2.StateA, Usa2010P2.fsucc, List.count, Prod, Prod.mk, Usa2010P2.evPairs, Not
Proof uses: NeZero, NeZero.mk, Fin.isLt, Ne, Eq, congrArg, Ne.symm, id, List.rec, List.nil, And.intro, Nat.zero_le, Nat.le_refl, List.cons, Equiv.symm, Equiv.trans, Equiv.swap, Equiv.apply_symm_apply, of_eq_true, eq_self and 23 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 88 steps
Open to load the checked before-and-after goal states.
```
lemma alternation {n : ℕ} (hn : 2 ≤ n) (a b : Fin n) (hab : a.val + 2 ≤ b.val)
    (ha : a.val + 1 < n) :
    ∀ (e : Fin n ≃ ZMod n) (ps : List (ZMod n)), Legal e ps →
      (StateA e a b (fsucc a ha) →
        (evPairs e ps).count (a, b) ≤ (evPairs e ps).count (fsucc a ha, b) + 1 ∧
        (evPairs e ps).count (fsucc a ha, b) ≤ (evPairs e ps).count (a, b)) ∧
      (¬ StateA e a b (fsucc a ha) →
        (evPairs e ps).count (a, b) ≤ (evPairs e ps).count (fsucc a ha, b) ∧
        (evPairs e ps).count (fsucc a ha, b) ≤ (evPairs e ps).count (a, b) + 1) := by
…
```
Mentions: Usa2010P2.Legal, Usa2010P2.StateA, Usa2010P2.fsucc, Usa2010P2.evPairs
lemma Usa2010P2.count_bound The number of times a fixed pair of students (a, b) can switch is at most b.val - a.val - 1 line 596 source
Source documentation
The number of times a fixed pair of students (a, b) can switch is at most b.val - a.val - 1. Proof by induction on the difference of the ranks, using the alternation lemma.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Equiv, ZMod, List, Usa2010P2.Legal, Eq, HSub.hSub, List.count, Prod, Prod.mk, Usa2010P2.evPairs
Proof uses: Nat.recAux, Eq.mpr, Not, Membership.mem, id, congrArg, propext, List.count_eq_zero, Ord.compare, HAdd.hAdd, Usa2010P2.evPairs_le, le_refl, GT.gt, Or, Nat.eq_zero_or_pos, Eq.symm, Nat.succ, Exists, Nat.exists_eq_succ_of_ne_zero, Nat.ne_of_gt and 12 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma count_bound {n : ℕ} (hn : 2 ≤ n) (d : ℕ) :
    ∀ (a b : Fin n) (e : Fin n ≃ ZMod n) (ps : List (ZMod n)), Legal e ps →
      b.val - a.val = d → (evPairs e ps).count (a, b) ≤ d - 1 := by
…
```
Mentions: Usa2010P2.Legal, Usa2010P2.evPairs
lemma Usa2010P2.sum_range_choose_two line 630 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Finset.range, Nat.choose, OfNat.ofNat
Proof uses: Nat.recAux, Eq.refl, Eq.mpr, HAdd.hAdd, id, congrArg, Finset.sum_range_succ, Nat.choose_succ_succ', add_comm
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P2.inner_sum line 636 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Finset.range, HSub.hSub, OfNat.ofNat, Nat.choose
Proof uses: Finset.sum_congr, rfl, Finset, Membership.mem, Finset.sum_range_reflect, Eq.mpr, id, congrArg, HDiv.hDiv, HMul.hMul, Finset.sum_range_id, Nat.choose_two_right, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P2.sum_Iio_val line 644 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset.sum, Finset.Iio, HSub.hSub, OfNat.ofNat, Nat.choose
Proof uses: Eq.mpr, Finset.range, id, congrArg, Eq.symm, Usa2010P2.inner_sum, Finset, Finset.map, Fin.valEmbedding, Fin.map_valEmbedding_Iio, Nat.Iio_eq_range, Function.Embedding, Finset.sum_map, Finset.sum_congr, rfl, Membership.mem, Eq.refl
24 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P2.pair_sum_choose3 line 654 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Prod, Fin, Finset.filter, LT.lt, Prod.fst, Prod.snd, Finset.univ, HSub.hSub, OfNat.ofNat, Nat.choose
Proof uses: Finset.Iio, Eq.mpr, ite, id, congrArg, Finset.sum_filter, SProd.sprod, Finset, Eq.symm, Finset.univ_product_univ, Prod.mk, Finset.sum_product, Finset.sum_comm, Finset.sum_congr, rfl, Membership.mem, Finset.ext, of_eq_true, Iff, Eq.trans and 11 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
problem Usa2010P2.usa2010_p2 USAMO 2010 Problem 2 line 688 source
Source documentation
USAMO 2010 Problem 2. There are n students standing in a circle, one behind the other, with heights h₁ < h₂ < ⋯ < hₙ. If a student with height hₖ is standing directly behind a student with height hₖ₋₂ or less, the two students are permitted to switch places. Then it is not possible to make more than C(n, 3) such switches.
We model the circle by positions in ZMod n (position p + 1 is directly behind position p), the students by their height ranks in Fin n, and a sequence of switches by the list of positions at which they occur; Legal asserts that every switch is permitted.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Fin, ZMod, List, Usa2010P2.Legal, LE.le, List.length, Nat.choose, OfNat.ofNat
Proof uses: LT.lt, Or, lt_or_ge, Eq, List.nil, Nat.zero_le, Eq.symm, List.cons, False.elim, HAdd.hAdd, Equiv.symm, Equiv.trans, Equiv.swap, And, False, Fin.isLt, Eq.refl, Eq.mpr, Prod, Usa2010P2.evPairs and 24 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
problem usa2010_p2 {n : ℕ} (e : Fin n ≃ ZMod n) (ps : List (ZMod n)) (h : Legal e ps) :
    ps.length ≤ n.choose 3 := by
…
```
Mentions: h, Usa2010P2.Legal