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

99 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2024, Problem 3

Let a₁, a₂, a₃, ... be an infinite sequence of positive integers, and let N be a positive integer. Suppose that, for each n > N, aₙ is equal to the number of times aₙ₋₁ appears in the list a₁, a₂, ..., aₙ₋₁.

Prove that at least one of the sequences a₁, a₃, a₅, ... and a₂, a₄, a₆, ... is eventually periodic.

Imports (4)

Imported by 1 file

Compfiles.lean

def Imo2024P3.Condition line 38 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: And, LT.lt, OfNat.ofNat, Eq, Finset.card, Finset.filter, HSub.hSub, Finset.range
5 instances, coercions and auxiliary constants left out.
def Imo2024P3.EventuallyPeriodic line 41 source
no axioms what this means
Statement uses: Nat
Proof uses: Exists, And, LT.lt, OfNat.ofNat, LE.le, Eq, HAdd.hAdd
5 instances, coercions and auxiliary constants left out.
def Imo2024P3.M A number greater than any of the initial terms a 0 through a N (otherwise arbitrary) line 50 source
Source documentation
A number greater than any of the initial terms a 0 through a N (otherwise arbitrary).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, Finset.sup, Finset.range, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
```
def M (a : ℕ → ℕ) (N : ℕ) : ℕ := (Finset.range (N + 1)).sup a + 1
```
lemma Imo2024P3.M_pos line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Imo2024P3.M
Proof uses: Nat.add_one_pos, Finset.sup, Finset.range, HAdd.hAdd
8 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.one_le_M line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo2024P3.M
Proof uses: Iff.mp, LT.lt, HAdd.hAdd, Nat.lt_iff_add_one_le, Imo2024P3.M_pos
7 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.apply_lt_M_of_le_N line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, LT.lt, Imo2024P3.M
Proof uses: Iff.mpr, HAdd.hAdd, Finset.sup, Finset.range, OfNat.ofNat, Nat.lt_add_one_iff, Finset.le_sup, Membership.mem, Finset, Nat.succ, Finset.mem_range_succ_iff
12 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.N_lt_of_M_le_apply line 61 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Imo2024P3.M, LT.lt
Proof uses: Decidable.byContradiction, Not, Nat.not_succ_le_self, Finset.sup, Finset.range, HAdd.hAdd, OfNat.ofNat, LE.le.trans, Finset.le_sup, Iff.mpr, Membership.mem, Finset, Nat.succ, Finset.mem_range_succ_iff, Eq.mp
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.ne_zero_of_M_le_apply line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Imo2024P3.M, Ne, OfNat.ofNat
Proof uses: Nat.ne_zero_of_lt, Imo2024P3.N_lt_of_M_le_apply
3 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.apply_lt_of_M_le_apply line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Imo2024P3.M, LT.lt
Proof uses: LT.lt.trans_le, Imo2024P3.apply_lt_M_of_le_N
4 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.apply_ne_of_M_le_apply line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Imo2024P3.M, Ne
Proof uses: LT.lt.ne, Imo2024P3.apply_lt_of_M_le_apply
3 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.toFinset_card_pos line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.Finite, Set.ofPred, Eq, LT.lt, OfNat.ofNat, Finset.card, Set.Finite.toFinset
Proof uses: Iff.mpr, Finset.Nonempty, Finset.card_pos, Set.Nonempty, Set.Finite.toFinset_nonempty, Exists.intro, Membership.mem, Set, rfl
5 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.apply_nth_zero line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Nat.nth, OfNat.ofNat
Proof uses: Nat.nth_mem, Imo2024P3.toFinset_card_pos
2 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.map_add_one_range line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidablePred, Not, OfNat.ofNat, Eq, Finset, Finset.map, Function.Embedding.mk, HAdd.hAdd, add_left_injective, Finset.filter, Finset.range
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, Function.Embedding, id, congrFun', congrArg, Iff.intro, LE.le, Eq.trans, LT.lt, Eq.mp, funext, of_eq_true, True, congr, eq_true and 13 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.pos line 100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, OfNat.ofNat
Proof uses: And.left, Eq, Finset.card, Finset.filter, HSub.hSub, Finset.range
7 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.apply_ne_zero line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Ne, OfNat.ofNat
Proof uses: LT.lt.ne', Imo2024P3.Condition.pos
3 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.one_le_apply line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LE.le, OfNat.ofNat
Proof uses: Iff.mpr, Ne, Nat.one_le_iff_ne_zero, Imo2024P3.Condition.apply_ne_zero
4 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.apply_eq_card line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, Eq, Finset.card, Finset.filter, HSub.hSub, OfNat.ofNat, Finset.range
Proof uses: And.right
10 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.apply_add_one_eq_card line 111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LE.le, Eq, HAdd.hAdd, OfNat.ofNat, Finset.card, Finset.filter, Finset.range
Proof uses: Eq.mpr, HSub.hSub, id, congrArg, Imo2024P3.Condition.apply_eq_card, Nat.lt_add_one_of_le, of_eq_true, Eq.trans, True, congrFun', Finset, Finset.filter_congr, Membership.mem, Iff.of_eq, add_tsub_cancel_right, eq_self
30 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.nth_apply_eq_zero line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Eq, Nat.nth, OfNat.ofNat
Proof uses: Eq.mpr, False, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, funext, propext, of_eq_true, Iff, Eq.trans, True, congrFun', congrArg, eq_false, LT.lt.ne', Imo2024P3.Condition.pos, iff_self, Nat.nth_false
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.nth_apply_add_one_eq line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LE.le, Eq, Nat.nth, HSub.hSub, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, Finset.card, Finset.filter, Finset.range, id, congrArg, Imo2024P3.Condition.apply_add_one_eq_card, Nat.count, Eq.symm, Nat.nth_count, rfl, of_eq_true, Eq.trans, True, congr, congrFun', Insert.insert, Finset, ite, Finset.filter.congr_simp and 15 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.apply_nth_add_one_eq line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Set.Finite, Set.ofPred, Eq, LT.lt, Finset.card, Set.Finite.toFinset, LE.le, Nat.nth, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, Finset.filter, HSub.hSub, Finset.range, id, congrArg, Imo2024P3.Condition.apply_eq_card, Nat.lt_add_one_of_le, add_tsub_cancel_right, Nat.count, Eq.symm, Nat.count_eq_card_filter_range, Nat.nth_mem, Nat.count_nth_succ, Eq.refl
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.apply_nth_add_one_eq_of_infinite line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Set.Infinite, Set.ofPred, Eq, LE.le, Nat.nth, HAdd.hAdd, OfNat.ofNat
Proof uses: Imo2024P3.Condition.apply_nth_add_one_eq, Set.Finite, absurd, LT.lt, Finset.card, Set.Finite.toFinset
6 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.apply_nth_add_one_eq_of_lt line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, Nat.nth, Eq, HAdd.hAdd, OfNat.ofNat
Proof uses: Imo2024P3.Condition.apply_nth_add_one_eq, Classical.byContradiction, Set.Finite, Set.ofPred, Finset.card, Set.Finite.toFinset, Not, Iff.mpr, Or, And, Exists, LE.le, Nat.nth_eq_zero, Or.inr, Eq.mp, Iff.of_eq, Eq.refl, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, propext and 2 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.lt_toFinset_card line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LE.le, Imo2024P3.M, HAdd.hAdd, OfNat.ofNat, Set.Finite, Set.ofPred, Eq, LT.lt, HSub.hSub, Finset.card, Set.Finite.toFinset
Proof uses: Eq.mpr, Nat.succ, id, congrArg, propext, Nat.sub_lt_iff_lt_add', Imo2024P3.M_pos, Nat.lt_one_add_iff, LE.le.trans, Finset.filter, Finset.range, Eq.rec, Imo2024P3.Condition.apply_eq_card, Imo2024P3.N_lt_of_M_le_apply, Finset.card_le_card, of_eq_true, Finset, Eq.trans, Set, True and 12 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.nth_ne_zero_of_M_le_of_lt line 146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LE.le, Imo2024P3.M, LT.lt, HAdd.hAdd, OfNat.ofNat, Ne, Nat.nth, Eq
Proof uses: Nat.nth_ne_zero_anti, Imo2024P3.apply_ne_of_M_le_apply, Nat.zero_le, HSub.hSub, Eq.rec, Imo2024P3.ne_zero_of_M_le_apply, Eq.symm, Imo2024P3.Condition.nth_apply_add_one_eq, LT.lt.le, Imo2024P3.N_lt_of_M_le_apply
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.apply_add_one_lt_of_apply_eq line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LE.le, LT.lt, Eq, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, Finset.card, Finset.filter, Finset.range, id, congrArg, Imo2024P3.Condition.apply_add_one_eq_card, Finset.card_lt_card, Iff.mp, Finset, And, Not, Finset.ssubset_def, And.intro, LE.ofSetLike, Finset.filter_subset_filter, of_eq_true, Eq.trans, True, Function.swap and 14 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.apply_add_one_ne_of_apply_eq line 158 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LE.le, Ne, Eq, HAdd.hAdd, OfNat.ofNat
Proof uses: Or.elim, LT.lt, Ne.lt_or_gt, LT.lt.ne, Imo2024P3.Condition.apply_add_one_lt_of_apply_eq, LT.lt.ne', Eq.symm
13 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.exists_infinite_setOf_apply_eq line 163 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Exists, Set.Infinite, Set.ofPred, Eq
Proof uses: Classical.byContradiction, Not, Set.range, Mathlib.Tactic.Contrapose.contrapose₂, Eq.mpr, Set.Finite, id, implies_congr, Eq.refl, Infinite, Set.preimage, Set.rangeFactorization, Singleton.singleton, Set, Finite.exists_infinite_fiber, Eq.mp, Finite, congrArg, Eq.symm, propext and 40 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.nonempty_setOf_infinite_setOf_apply_eq line 185 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Set.Nonempty, Set.ofPred, Set.Infinite, Eq
Proof uses: Imo2024P3.Condition.exists_infinite_setOf_apply_eq
lemma Imo2024P3.Condition.injOn_setOf_apply_add_one_eq_of_M_le line 188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LE.le, Imo2024P3.M, Set.InjOn, Set.ofPred, Eq, HAdd.hAdd, OfNat.ofNat
Proof uses: Membership.mem, Set, Nat.nth, HSub.hSub, Eq.rec, Imo2024P3.Condition.nth_apply_add_one_eq, Iff.mp, LT.lt, Nat.lt_add_one_iff, Imo2024P3.N_lt_of_M_le_apply, Eq.symm, Eq.mpr, id, congrArg, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.empty_consecutive_apply_ge_M line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Eq, Set, Set.ofPred, And, LE.le, Imo2024P3.M, HAdd.hAdd, OfNat.ofNat, EmptyCollection.emptyCollection
Proof uses: Eq.mpr, Not, Membership.mem, id, congrArg, propext, Set.eq_empty_iff_forall_notMem, Nat.strong_induction_on, LT.lt, False, of_eq_true, Eq.trans, True, forall_congr, implies_congr_ctx, Eq.refl, eq_true, Eq.mp, implies_true, Finset and 40 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.card_lt_M_of_M_le line 242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LE.le, Imo2024P3.M, Exists, Set.Finite, Set.ofPred, Eq, LT.lt, Finset.card, Set.Finite.toFinset
Proof uses: Set, And, HAdd.hAdd, OfNat.ofNat, EmptyCollection.emptyCollection, Imo2024P3.Condition.empty_consecutive_apply_ge_M, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, Set.Nonempty, id, implies_congr, Ne, Eq.trans, binderNameHint, forall_congr, Exists.intro, Membership.mem, Nat.nth, HSub.hSub and 14 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.bddAbove_setOf_infinite_setOf_apply_eq line 253 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, BddAbove, Set.ofPred, Set.Infinite, Eq
Proof uses: Exists.intro, Membership.mem, Set, upperBounds, Imo2024P3.M, Decidable.byContradiction, LE.le, Not, Exists, Imo2024P3.Condition.card_lt_M_of_M_le, LT.lt.le, Iff.mp, LT.lt, not_le
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.infinite_setOf_apply_eq_anti line 258 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, OfNat.ofNat, Set.Infinite, Set.ofPred, Eq, LE.le
Proof uses: HAdd.hAdd, Set.InjOn, Function.Injective.injOn, add_left_injective, Eq.mpr, Set.image, id, congrArg, Eq.symm, propext, Set.infinite_image_iff, SDiff.sdiff, Set, Singleton.singleton, Set.Infinite.sdiff, Set.finite_singleton, eq_of_heq, HEq, Eq.refl, HEq.refl and 36 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
def Imo2024P3.Condition.k The largest number to appear infinitely often line 301 source
Source documentation
The largest number to appear infinitely often.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SupSet.sSup, Set.ofPred, Set.Infinite, Eq
1 instances, coercions and auxiliary constants left out.
```
noncomputable def k : ℕ := sSup {m | {i | a i = m}.Infinite}
```
def Imo2024P3.Condition.Small Small numbers are those that are at most k (that is, those that appear infinitely often) line 304 source
Source documentation
Small numbers are those that are at most k (that is, those that appear infinitely often).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: LE.le, Imo2024P3.Condition.k
1 instances, coercions and auxiliary constants left out.
```
def Small (j : ℕ) : Prop := j ≤ k a
…
```
Mentions: Imo2024P3.Condition.k
lemma Imo2024P3.Condition.infinite_setOf_apply_eq_k line 308 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Set.Infinite, Set.ofPred, Eq, Imo2024P3.Condition.k
Proof uses: Nat.sSup_mem, Imo2024P3.Condition.nonempty_setOf_infinite_setOf_apply_eq, Imo2024P3.Condition.bddAbove_setOf_infinite_setOf_apply_eq
lemma Imo2024P3.Condition.infinite_setOf_apply_eq_iff_small line 311 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, OfNat.ofNat, Iff, Set.Infinite, Set.ofPred, Eq, Imo2024P3.Condition.Small
Proof uses: Iff.intro, le_csSup, Imo2024P3.Condition.bddAbove_setOf_infinite_setOf_apply_eq, Imo2024P3.Condition.infinite_setOf_apply_eq_anti, Imo2024P3.Condition.k, Imo2024P3.Condition.infinite_setOf_apply_eq_k
7 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.finite_setOf_apply_eq_iff_not_small line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, OfNat.ofNat, Iff, Set.Finite, Set.ofPred, Eq, Not, Imo2024P3.Condition.Small
Proof uses: Eq.mp, Set.Infinite, congrFun', congrArg, Iff.not, Imo2024P3.Condition.infinite_setOf_apply_eq_iff_small
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.finite_setOf_apply_eq_k_add_one line 320 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Set.Finite, Set.ofPred, Eq, HAdd.hAdd, Imo2024P3.Condition.k, OfNat.ofNat
Proof uses: Eq.mpr, Not, Imo2024P3.Condition.Small, id, congrArg, propext, Imo2024P3.Condition.finite_setOf_apply_eq_iff_not_small, LE.le, Imo2024P3.Condition.Small.eq_1
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.finite_setOf_k_lt_card There are only finitely many m that appear more than k times line 325 source
Source documentation
There are only finitely many m that appear more than k times.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Set.Finite, Set.ofPred, Eq, LT.lt, Imo2024P3.Condition.k, Finset.card, Set.Finite.toFinset
Proof uses: Eq.mpr, Set.image, HAdd.hAdd, Nat.nth, OfNat.ofNat, id, congrArg, Eq.symm, propext, Set.finite_image_iff, Membership.mem, Set, Eq.mp, Nat.nth_mem, eq_of_heq, HEq, Eq.refl, HEq.refl, Set.Finite.of_sdiff, Set.Iic and 12 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma finite_setOf_k_lt_card : {m | ∀ hf : {i | a i = m}.Finite, k a < #hf.toFinset}.Finite := by
…
```
Mentions: Imo2024P3.Condition.k
lemma Imo2024P3.Condition.bddAbove_setOf_k_lt_card line 337 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, BddAbove, Set.ofPred, Set.Finite, Eq, LT.lt, Imo2024P3.Condition.k, Finset.card, Set.Finite.toFinset
Proof uses: Set.Finite.bddAbove, Imo2024P3.Condition.finite_setOf_k_lt_card
12 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.k_pos line 340 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, OfNat.ofNat, Imo2024P3.Condition.k
Proof uses: Decidable.byContradiction, Not, Eq.rec, Eq, Set.Infinite, Set.ofPred, Imo2024P3.Condition.infinite_setOf_apply_eq_k, Iff.mp, LE.le, nonpos_iff_eq_zero, Eq.mp, Eq.mpr, Set.Finite, EmptyCollection.emptyCollection, Set, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm and 14 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.small_one line 347 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Small, OfNat.ofNat
Proof uses: Classical.byContradiction, Not, False.elim, False, Eq.mp, Eq.trans, LE.le, Imo2024P3.Condition.k, LT.lt, Eq, eq_false, LT.lt.ne', Imo2024P3.Condition.k_pos
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.infinite_setOf_apply_eq_one line 351 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Set.Infinite, Set.ofPred, Eq, OfNat.ofNat
Proof uses: Iff.mpr, Imo2024P3.Condition.Small, Imo2024P3.Condition.infinite_setOf_apply_eq_iff_small, of_decide_eq_true, LT.lt, id, Bool, Decidable.decide, Bool.true, Eq.refl, Imo2024P3.Condition.small_one
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Imo2024P3.Condition.l The largest number to appear more than k times line 357 source
Source documentation
The largest number to appear more than k times.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SupSet.sSup, Set.ofPred, Set.Finite, Eq, LT.lt, Imo2024P3.Condition.k, Finset.card, Set.Finite.toFinset
2 instances, coercions and auxiliary constants left out.
```
noncomputable def l : ℕ := sSup {m | ∀ hf : {i | a i = m}.Finite, k a < #hf.toFinset}
```
Mentions: Imo2024P3.Condition.k
def Imo2024P3.Condition.Medium Medium numbers are those that are more than k but at most l (and include all numbers appearing finitely often but more than k times) line 361 source
Source documentation
Medium numbers are those that are more than k but at most l (and include all numbers appearing finitely often but more than k times).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: And, LT.lt, Imo2024P3.Condition.k, LE.le, Imo2024P3.Condition.l
2 instances, coercions and auxiliary constants left out.
```
def Medium (j : ℕ) : Prop := k a < j ∧ j ≤ l a
```
Mentions: Imo2024P3.Condition.k, Imo2024P3.Condition.l
def Imo2024P3.Condition.Big Big numbers are those greater than l (thus, appear at most k times) line 364 source
Source documentation
Big numbers are those greater than l (thus, appear at most k times).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: LT.lt, Imo2024P3.Condition.l
1 instances, coercions and auxiliary constants left out.
```
def Big (j : ℕ) : Prop := l a < j
…
```
Mentions: Imo2024P3.Condition.l
lemma Imo2024P3.Condition.k_le_l line 368 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LE.le, Imo2024P3.Condition.k, Imo2024P3.Condition.l
Proof uses: le_csSup, Set.ofPred, Set.Finite, Eq, LT.lt, Finset.card, Set.Finite.toFinset, Imo2024P3.Condition.bddAbove_setOf_k_lt_card, absurd, Imo2024P3.Condition.infinite_setOf_apply_eq_k
5 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.k_lt_of_big line 371 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Big, LT.lt, Imo2024P3.Condition.k
Proof uses: LE.le.trans_lt, Imo2024P3.Condition.l, Imo2024P3.Condition.k_le_l
2 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.pos_of_big line 374 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Big, LT.lt, OfNat.ofNat
Proof uses: LE.le.trans_lt, Imo2024P3.Condition.k, Nat.zero_le, Imo2024P3.Condition.k_lt_of_big
4 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.not_small_of_big line 377 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Big, Not, Imo2024P3.Condition.Small
Proof uses: of_eq_true, LE.le, Imo2024P3.Condition.k, Eq.trans, LT.lt, True, eq_true, Imo2024P3.Condition.k_lt_of_big
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.exists_card_le_of_big line 379 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Big, Exists, Set.Finite, Set.ofPred, Eq, LE.le, Finset.card, Set.Finite.toFinset, Imo2024P3.Condition.k
Proof uses: Not, Imo2024P3.Condition.Small, Imo2024P3.Condition.not_small_of_big, Exists.intro, Eq.mp, congrArg, Eq.symm, propext, Imo2024P3.Condition.finite_setOf_apply_eq_iff_not_small, Imo2024P3.Condition.pos_of_big, Decidable.byContradiction, notMem_of_csSup_lt, LT.lt, Imo2024P3.Condition.bddAbove_setOf_k_lt_card
12 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Imo2024P3.Condition.N'aux N'aux is such that, by position N'aux, every medium number has made all its appearances and every small number has appeared more than max(k, N+1) times line 391 source
Source documentation
N'aux is such that, by position N'aux, every medium number has made all its appearances and every small number has appeared more than max(k, N+1) times.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Max.max, SupSet.sSup, Set.ofPred, Imo2024P3.Condition.Medium, Set.image, Nat.nth, Eq, Imo2024P3.Condition.k, HAdd.hAdd, OfNat.ofNat, Set.Iic
6 instances, coercions and auxiliary constants left out.
```
noncomputable def N'aux : ℕ :=
…
```
def Imo2024P3.Condition.N' Documented declaration: N' line 397 source
Source documentation
N' is such that, by position N', every medium number has made all its appearances and every small number has appeared more than max(k, N+1) times; furthermore, a N' is small (which means that every subsequent big number is preceded by a small number).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, Imo2024P3.Condition.N'aux, ite, Imo2024P3.Condition.Small, OfNat.ofNat, Classical.propDecidable
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def N' : ℕ := by
…
```
lemma Imo2024P3.Condition.not_medium_of_N'aux_lt line 403 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, Imo2024P3.Condition.N'aux, Not, Imo2024P3.Condition.Medium
Proof uses: Set, Set.iUnion, Membership.mem, Set.Ioc, Imo2024P3.Condition.k, Imo2024P3.Condition.l, Set.ofPred, Eq, Set.Finite, Set.Finite.biUnion, Set.finite_Ioc, LE.le, Eq.mpr, Imo2024P3.Condition.Small, id, congrArg, propext, Imo2024P3.Condition.finite_setOf_apply_eq_iff_not_small, Imo2024P3.Condition.Small.eq_1, not_le and 21 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.small_or_big_of_N'aux_lt line 412 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, Imo2024P3.Condition.N'aux, Or, Imo2024P3.Condition.Small, Imo2024P3.Condition.Big
Proof uses: Not, Imo2024P3.Condition.Medium, Imo2024P3.Condition.not_medium_of_N'aux_lt, Eq.mpr, LE.le, Imo2024P3.Condition.k, id, Eq, congrArg, Imo2024P3.Condition.Small.eq_1, Imo2024P3.Condition.l, Imo2024P3.Condition.Big.eq_1, Eq.mp, And, Imo2024P3.Condition.Medium.eq_1
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.small_or_big_of_N'_le line 417 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LE.le, Imo2024P3.Condition.N', Or, Imo2024P3.Condition.Small, Imo2024P3.Condition.Big
Proof uses: Imo2024P3.Condition.small_or_big_of_N'aux_lt, Eq.mp, HAdd.hAdd, Imo2024P3.Condition.N'aux, ite, OfNat.ofNat, Classical.propDecidable, congrArg, Imo2024P3.Condition.N'.eq_1
6 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.nth_sup_k_N_add_one_le_N'aux_of_small line 424 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition.Small, LE.le, Nat.nth, Eq, Max.max, Imo2024P3.Condition.k, HAdd.hAdd, OfNat.ofNat, Imo2024P3.Condition.N'aux
Proof uses: Decidable.byContradiction, Not, notMem_of_csSup_lt, Set.image, Set.Iic, LE.le.trans_lt, SupSet.sSup, Set.ofPred, Imo2024P3.Condition.Medium, le_sup_right, Eq.mp, LT.lt, Set.Finite.bddAbove, Set.Finite.image, Set.finite_Iic, Exists.intro, And, Membership.mem, Set, And.intro and 1 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.nth_sup_k_le_N'aux_of_small line 432 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Small, LE.le, Nat.nth, Eq, Imo2024P3.Condition.k, Imo2024P3.Condition.N'aux
Proof uses: OfNat.ofNat, of_eq_true, Eq.trans, True, congrFun', congrArg, Imo2024P3.Condition.nth_apply_eq_zero, HAdd.hAdd, LE.le.trans, Nat.succ, Max.max, Iff.mpr, Nat.nth_le_nth, Set.Infinite, Set.ofPred, Imo2024P3.Condition.infinite_setOf_apply_eq_iff_small, Nat.zero_lt_succ, le_sup_left, Imo2024P3.Condition.nth_sup_k_N_add_one_le_N'aux_of_small
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.nth_sup_N_add_one_le_N'aux_of_small line 439 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Small, LE.le, Nat.nth, Eq, HAdd.hAdd, OfNat.ofNat, Imo2024P3.Condition.N'aux
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Imo2024P3.Condition.nth_apply_eq_zero, LE.le.trans, Nat.succ, Max.max, Imo2024P3.Condition.k, Iff.mpr, Nat.nth_le_nth, Set.Infinite, Set.ofPred, Imo2024P3.Condition.infinite_setOf_apply_eq_iff_small, Nat.zero_lt_succ, le_sup_right, Imo2024P3.Condition.nth_sup_k_N_add_one_le_N'aux_of_small
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.N_lt_N'aux line 446 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, Imo2024P3.Condition.N'aux
Proof uses: Iff.mp, LE.le, HAdd.hAdd, OfNat.ofNat, Nat.add_one_le_iff, LE.le.trans, Nat.nth, Eq, Nat.le_nth, Set.Finite, Set.ofPred, absurd, Finset.card, Set.Finite.toFinset, Imo2024P3.Condition.infinite_setOf_apply_eq_one, Imo2024P3.Condition.nth_sup_N_add_one_le_N'aux_of_small, Imo2024P3.Condition.small_one
7 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.N_lt_N' N is less than N' line 451 source
Source documentation
N is less than N'.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, Imo2024P3.Condition.N'
Proof uses: LT.lt.trans_le, Imo2024P3.Condition.N'aux, Imo2024P3.Condition.N_lt_N'aux, Nat.le_add_right, ite, Imo2024P3.Condition.Small, HAdd.hAdd, OfNat.ofNat, Classical.propDecidable
5 instances, coercions and auxiliary constants left out.
```
lemma N_lt_N' : N < N' a N := hc.N_lt_N'aux.trans_le (Nat.le_add_right _ _)
```
Mentions: Imo2024P3.Condition.N'
lemma Imo2024P3.Condition.lt_card_filter_eq_of_small_nth_lt line 453 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, OfNat.ofNat, Imo2024P3.Condition.Small, Nat.nth, Eq, Finset.card, Finset.filter, Finset.range
Proof uses: Eq.mpr, Nat.count, id, congrArg, Eq.symm, Nat.count_eq_card_filter_range, Iff.mpr, Nat.lt_nth_iff_count_lt, Eq.mp, Set.Infinite, Set.ofPred, propext, Imo2024P3.Condition.infinite_setOf_apply_eq_iff_small
6 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.k_lt_card_filter_eq_of_small_of_N'aux_le line 459 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, OfNat.ofNat, Imo2024P3.Condition.Small, Imo2024P3.Condition.N'aux, Imo2024P3.Condition.k, Finset.card, Finset.filter, Eq, Finset.range
Proof uses: Imo2024P3.Condition.lt_card_filter_eq_of_small_nth_lt, LE.le.trans_lt, Nat.nth, Imo2024P3.Condition.nth_sup_k_le_N'aux_of_small
6 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.N_add_one_lt_card_filter_eq_of_small_of_N'aux_le line 463 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, OfNat.ofNat, Imo2024P3.Condition.Small, Imo2024P3.Condition.N'aux, HAdd.hAdd, Finset.card, Finset.filter, Eq, Finset.range
Proof uses: Imo2024P3.Condition.lt_card_filter_eq_of_small_nth_lt, LE.le.trans_lt, Nat.nth, Imo2024P3.Condition.nth_sup_N_add_one_le_N'aux_of_small
10 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.N_add_one_lt_card_filter_eq_of_small_of_N'_le line 468 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, OfNat.ofNat, Imo2024P3.Condition.Small, Imo2024P3.Condition.N', HAdd.hAdd, Finset.card, Finset.filter, Eq, Finset.range
Proof uses: Imo2024P3.Condition.N_add_one_lt_card_filter_eq_of_small_of_N'aux_le, Nat.lt_of_add_right_lt, Imo2024P3.Condition.N'aux, ite, Classical.propDecidable, Eq.mp, congrArg, Imo2024P3.Condition.N'.eq_1
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.apply_add_one_big_of_apply_small_of_N'aux_le line 474 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Small, LE.le, Imo2024P3.Condition.N'aux, Imo2024P3.Condition.Big, HAdd.hAdd, OfNat.ofNat
Proof uses: LT.lt, Not, Eq.mpr, Finset.card, Finset.filter, Eq, Finset.range, id, congrArg, Imo2024P3.Condition.apply_add_one_eq_card, LE.le.trans, LT.lt.le, Imo2024P3.Condition.N_lt_N'aux, Imo2024P3.Condition.k, Imo2024P3.Condition.Small.eq_1, propext, not_le, Imo2024P3.Condition.k_lt_card_filter_eq_of_small_of_N'aux_le, Imo2024P3.Condition.pos, Eq.mp and 7 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.apply_add_one_big_of_apply_small_of_N'_le line 481 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Small, LE.le, Imo2024P3.Condition.N', Imo2024P3.Condition.Big, HAdd.hAdd, OfNat.ofNat
Proof uses: Imo2024P3.Condition.apply_add_one_big_of_apply_small_of_N'aux_le, LE.le.trans, Imo2024P3.Condition.N'aux, ite, Classical.propDecidable, Nat.le_add_right
9 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.apply_add_one_small_of_apply_big_of_N'aux_le line 485 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Big, LE.le, Imo2024P3.Condition.N'aux, Imo2024P3.Condition.Small, HAdd.hAdd, OfNat.ofNat
Proof uses: Set.Finite, Set.ofPred, Eq, Finset.card, Set.Finite.toFinset, Imo2024P3.Condition.k, Exists, Imo2024P3.Condition.exists_card_le_of_big, Eq.mpr, Finset.filter, Finset.range, id, congrArg, Imo2024P3.Condition.apply_add_one_eq_card, LE.le.trans, LT.lt.le, Imo2024P3.Condition.N_lt_N'aux, Finset.card_le_card, of_eq_true, Finset and 13 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.apply_add_one_small_of_apply_big_of_N'_le line 491 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Big, LE.le, Imo2024P3.Condition.N', Imo2024P3.Condition.Small, HAdd.hAdd, OfNat.ofNat
Proof uses: Imo2024P3.Condition.apply_add_one_small_of_apply_big_of_N'aux_le, LE.le.trans, Imo2024P3.Condition.N'aux, ite, Classical.propDecidable, Nat.le_add_right
9 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.apply_add_two_small_of_apply_small_of_N'_le line 495 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Small, LE.le, Imo2024P3.Condition.N', HAdd.hAdd, OfNat.ofNat
Proof uses: Imo2024P3.Condition.apply_add_one_small_of_apply_big_of_N'_le, Imo2024P3.Condition.apply_add_one_big_of_apply_small_of_N'_le
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.small_apply_N' a (N' a N) is a small number line 501 source
Source documentation
a (N' a N) is a small number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Small, Imo2024P3.Condition.N'
Proof uses: Eq.mpr, HAdd.hAdd, Imo2024P3.Condition.N'aux, ite, OfNat.ofNat, Classical.propDecidable, id, Eq, congrArg, Imo2024P3.Condition.N'.eq_1, dite, ite_eq_left, Not, ite_eq_right, Imo2024P3.Condition.Big, Eq.mp, Or, Eq.trans, False, congrFun' and 5 more
4 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma small_apply_N' : Small a (a (N' a N)) := by
…
```
Mentions: Imo2024P3.Condition.Small, Imo2024P3.Condition.N'
lemma Imo2024P3.Condition.small_apply_N'_add_iff_even line 509 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Iff, Imo2024P3.Condition.Small, HAdd.hAdd, Imo2024P3.Condition.N', Even
Proof uses: Nat.recAux, Eq.mpr, OfNat.ofNat, id, Eq, Eq.trans, True, congr, congrArg, add_zero, iff_true, Imo2024P3.Condition.small_apply_N', dite, Eq.symm, add_assoc, Not, of_eq_true, Odd, False, eq_false and 14 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.small_apply_add_two_mul_iff_small line 521 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LE.le, Imo2024P3.Condition.N', Iff, Imo2024P3.Condition.Small, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, HSub.hSub, id, Eq, congrArg, add_assoc, Even, propext, Imo2024P3.Condition.small_apply_N'_add_iff_even, of_eq_true, Eq.trans, True, congrFun', iff_true, iff_self
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.apply_sub_one_small_of_apply_big_of_N'_le line 527 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Big, LE.le, Imo2024P3.Condition.N', Imo2024P3.Condition.Small, HSub.hSub, OfNat.ofNat
Proof uses: LT.lt, Imo2024P3.Condition.N_lt_N', Decidable.byContradiction, Not, Eq, Imo2024P3.Condition.not_small_of_big, Eq.rec, Imo2024P3.Condition.small_apply_N', Or.elim, Imo2024P3.Condition.small_or_big_of_N'_le, id, False.elim, HAdd.hAdd, Imo2024P3.Condition.apply_add_one_small_of_apply_big_of_N'_le, Nat.sub_add_cancel
14 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.apply_sub_one_big_of_apply_small_of_N'_lt line 540 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Small, LT.lt, Imo2024P3.Condition.N', Imo2024P3.Condition.Big, HSub.hSub, OfNat.ofNat
Proof uses: LE.le, Or.elim, Imo2024P3.Condition.small_or_big_of_N'_le, False.elim, Imo2024P3.Condition.not_small_of_big, Eq.rec, HAdd.hAdd, Eq, Imo2024P3.Condition.apply_add_one_big_of_apply_small_of_N'_le, Nat.sub_add_cancel, id
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.apply_sub_two_small_of_apply_small_of_N'_lt line 547 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Small, LT.lt, Imo2024P3.Condition.N', HSub.hSub, OfNat.ofNat
Proof uses: Eq.mpr, Eq.refl, Imo2024P3.Condition.apply_sub_one_small_of_apply_big_of_N'_le, Imo2024P3.Condition.apply_sub_one_big_of_apply_small_of_N'_lt
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.N_add_one_lt_apply_of_apply_big_of_N'_le line 552 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Big, LE.le, Imo2024P3.Condition.N', LT.lt, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.rec, Finset.card, Finset.filter, Eq, HSub.hSub, Finset.range, Imo2024P3.Condition.N_add_one_lt_card_filter_eq_of_small_of_N'_le, Imo2024P3.Condition.pos, Imo2024P3.Condition.apply_sub_one_small_of_apply_big_of_N'_le, Decidable.byContradiction, Not, Imo2024P3.Condition.not_small_of_big, Imo2024P3.Condition.small_apply_N', Eq.symm, Imo2024P3.Condition.apply_eq_card, LT.lt.trans_le, Imo2024P3.Condition.N_lt_N'
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.setOf_apply_eq_of_apply_big_of_N'_le line 560 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Big, LE.le, Imo2024P3.Condition.N', Eq, Set, Set.ofPred, And, LT.lt, Imo2024P3.Condition.Small, HSub.hSub, OfNat.ofNat, Finset.card, Finset.filter, Finset.range
Proof uses: Membership.mem, Eq.rec, Imo2024P3.Condition.apply_eq_card, Eq.symm, Set.Finite, Set.Finite.toFinset, Imo2024P3.Condition.k, Exists, Imo2024P3.Condition.exists_card_le_of_big, Set.Finite.subset, Finset, Finset.eq_of_subset_of_card_le, Eq.mp, congrArg, propext, Set.Finite.toFinset_subset_toFinset, LE.le.trans, Finset.image, HAdd.hAdd, Nat.nth and 41 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.N_lt_of_apply_eq_of_apply_big_of_N'_le line 599 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Eq, Imo2024P3.Condition.Big, LE.le, Imo2024P3.Condition.N', LT.lt
Proof uses: Membership.mem, Set, Set.ofPred, id, And.left, And, Imo2024P3.Condition.Small, HSub.hSub, OfNat.ofNat, Finset.card, Finset.filter, Finset.range, Eq.rec, Imo2024P3.Condition.setOf_apply_eq_of_apply_big_of_N'_le
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.small_apply_sub_one_of_apply_eq_of_apply_big_of_N'_le line 604 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Eq, Imo2024P3.Condition.Big, LE.le, Imo2024P3.Condition.N', Imo2024P3.Condition.Small, HSub.hSub, OfNat.ofNat
Proof uses: Membership.mem, Set, Set.ofPred, id, And.left, Finset.card, Finset.filter, Finset.range, And.right, LT.lt, And, Eq.rec, Imo2024P3.Condition.setOf_apply_eq_of_apply_big_of_N'_le
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.apply_add_one_eq_card_small_le_card_eq Lemma 1 from the informal solution line 612 source
Source documentation
Lemma 1 from the informal solution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, Imo2024P3.Condition.N', Imo2024P3.Condition.Big, Eq, HAdd.hAdd, OfNat.ofNat, Finset.card, Finset.filter, LE.le, Finset.range, Imo2024P3.Condition.k
Proof uses: Eq.mpr, id, congrArg, Imo2024P3.Condition.apply_add_one_eq_card, LT.lt.le, LT.lt.trans, Imo2024P3.Condition.N_lt_N', Finset.image, Nat.nth, HSub.hSub, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Finset, Eq.rec, Finset.ext, Iff, Membership.mem and 59 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
```
lemma apply_add_one_eq_card_small_le_card_eq {i : ℕ} (hi : N' a N < i) (hib : Big a (a i)) :
    a (i + 1) = #{m ∈ Finset.range (k a + 1) | a i ≤ #{j ∈ Finset.range i | a j = m}} := by
…
```
Mentions: Imo2024P3.Condition.N', Imo2024P3.Condition.Big, Imo2024P3.Condition.k
lemma Imo2024P3.Condition.apply_eq_card_small_le_card_eq_of_small Similar to Lemma 1 from the informal solution, but with a Small hypothesis instead of Big and considering a range one larger (the form needed for Lemma 2) line 663 source
Source documentation
Similar to Lemma 1 from the informal solution, but with a Small hypothesis instead of Big and considering a range one larger (the form needed for Lemma 2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, HAdd.hAdd, Imo2024P3.Condition.N', OfNat.ofNat, Imo2024P3.Condition.Small, Eq, Finset.card, Finset.filter, LE.le, HSub.hSub, Finset.range, Imo2024P3.Condition.k
Proof uses: Imo2024P3.Condition.Big, Imo2024P3.Condition.apply_sub_one_big_of_apply_small_of_N'_lt, Eq.mpr, id, congrArg, Imo2024P3.Condition.apply_add_one_eq_card_small_le_card_eq, Finset, Eq.rec, Eq.refl, Finset.ext, Iff, Membership.mem, Eq.trans, And, congr, congrFun', eq_of_heq, HEq, HEq.refl, Eq.symm and 11 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma apply_eq_card_small_le_card_eq_of_small {i : ℕ} (hi : N' a N + 1 < i)
    (his : Small a (a i)) :
    a i = #{m ∈ Finset.range (k a + 1) | a (i - 1) ≤ #{j ∈ Finset.range i | a j = m}} := by
…
```
Mentions: Imo2024P3.Condition.N', Imo2024P3.Condition.Small, Imo2024P3.Condition.k
lemma Imo2024P3.Condition.exists_apply_sub_two_eq_of_apply_eq Lemma 2 from the informal solution line 684 source
Source documentation
Lemma 2 from the informal solution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, HAdd.hAdd, Imo2024P3.Condition.N', OfNat.ofNat, Imo2024P3.Condition.Small, Eq, LE.le, Finset.card, Finset.filter, Finset.Ico, Exists, And, Membership.mem, Finset, HSub.hSub
Proof uses: Finset.range, Imo2024P3.Condition.k, Imo2024P3.Condition.apply_eq_card_small_le_card_eq_of_small, Eq.rec, Imo2024P3.Condition.N_lt_N', Union.union, Eq.mpr, id, congrArg, Finset.range_eq_Ico, Min.min, Max.max, Finset.Ico_union_Ico', of_eq_true, Eq.trans, True, congrFun', congr, inf_of_le_left, sup_of_le_right and 55 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 110 steps
Open to load the checked before-and-after goal states.
```
lemma exists_apply_sub_two_eq_of_apply_eq {i j : ℕ} (hi : N' a N + 2 < i) (hijlt : i < j)
    (his : Small a (a i)) (hijeq : a i = a j)
    (hij1 : ∀ t, Small a t → #{x ∈ Finset.Ico i j | a x = t} ≤ 1) :
    ∃ t, t ∈ Finset.Ico i j ∧ a (i - 2) = a t := by
…
```
Mentions: Imo2024P3.Condition.N', Imo2024P3.Condition.Small
def Imo2024P3.Condition.pSet The indices, minus n, of small numbers appearing for the second or subsequent time at or after a n line 800 source
Source documentation
The indices, minus n, of small numbers appearing for the second or subsequent time at or after a n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set
Proof uses: Set.ofPred, Exists, And, Membership.mem, Finset, Finset.Ico, HAdd.hAdd, Imo2024P3.Condition.Small, Eq
6 instances, coercions and auxiliary constants left out.
```
def pSet (n : ℕ) : Set ℕ := {t | ∃ i ∈ Finset.Ico n (n + t), Small a (a i) ∧ a (n + t) = a i}
```
Mentions: Imo2024P3.Condition.Small
def Imo2024P3.Condition.p The index, minus n, of the second appearance of the first small number to appear twice at or after a n line 804 source
Source documentation
The index, minus n, of the second appearance of the first small number to appear twice at or after a n. This is only used for small a n with N' a N + 2 < n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: InfSet.sInf, Imo2024P3.Condition.pSet
1 instances, coercions and auxiliary constants left out.
```
noncomputable def p (n : ℕ) : ℕ := sInf (pSet a n)
…
```
Mentions: Imo2024P3.Condition.pSet
lemma Imo2024P3.Condition.nonempty_pSet line 808 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Set.Nonempty, Imo2024P3.Condition.pSet
Proof uses: And, Membership.mem, Set, Set.ofPred, Eq, OfNat.ofNat, LT.lt, Exists, Set.Infinite.exists_gt, Imo2024P3.Condition.infinite_setOf_apply_eq_one, Exists.intro, HSub.hSub, Eq.mpr, LE.le, HAdd.hAdd, Imo2024P3.Condition.Small, id, congrFun', congrArg, Finset and 8 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.exists_mem_Ico_small_and_apply_add_p_eq line 815 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Exists, And, Membership.mem, Finset, Finset.Ico, HAdd.hAdd, Imo2024P3.Condition.p, Imo2024P3.Condition.Small, Eq
Proof uses: csInf_mem, Imo2024P3.Condition.pSet, Imo2024P3.Condition.nonempty_pSet
9 instances, coercions and auxiliary constants left out.
lemma Imo2024P3.Condition.p_pos line 819 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, OfNat.ofNat, Imo2024P3.Condition.p
Proof uses: Decidable.byContradiction, Not, Exists, And, Membership.mem, Finset, Finset.Ico, HAdd.hAdd, Imo2024P3.Condition.Small, Eq, Imo2024P3.Condition.exists_mem_Ico_small_and_apply_add_p_eq, False.elim, False, Eq.mp, Eq.trans, congrArg, funext, congrFun', EmptyCollection.emptyCollection, Finset.Ico_eq_empty_of_le and 5 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.card_filter_apply_eq_Ico_add_p_le_one line 824 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Imo2024P3.Condition.Small, LE.le, Finset.card, Finset.filter, Eq, Finset.Ico, HAdd.hAdd, Imo2024P3.Condition.p, OfNat.ofNat
Proof uses: IsLeast, Imo2024P3.Condition.pSet, isLeast_csInf, Imo2024P3.Condition.nonempty_pSet, Eq.mpr, Membership.mem, Finset, id, congrArg, propext, Finset.card_le_one_iff, LT.lt, Or, lt_trichotomy, HSub.hSub, And.right, Exists, And, Eq.mp, congr and 14 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.apply_add_p_eq line 843 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, HAdd.hAdd, Imo2024P3.Condition.N', OfNat.ofNat, Imo2024P3.Condition.Small, Eq, Imo2024P3.Condition.p
Proof uses: And, Membership.mem, Finset, Finset.Ico, Exists, Imo2024P3.Condition.exists_mem_Ico_small_and_apply_add_p_eq, Decidable.byContradiction, Not, LE.le, Finset.card, Finset.filter, Trans.trans, Finset.card_le_card, Finset.filter_subset_filter, Finset.Ico_subset_Ico, And.left, Eq.mp, le_rfl, Imo2024P3.Condition.card_filter_apply_eq_Ico_add_p_le_one, HSub.hSub and 18 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.even_p line 866 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, HAdd.hAdd, Imo2024P3.Condition.N', OfNat.ofNat, Imo2024P3.Condition.Small, Even, Imo2024P3.Condition.p
Proof uses: Eq, HSub.hSub, Eq.rec, Eq.symm, Imo2024P3.Condition.apply_add_p_eq, Eq.mp, Eq.trans, Iff, True, congrFun', congrArg, eq_true, propext, Imo2024P3.Condition.small_apply_N'_add_iff_even, true_iff, add_assoc
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.p_le_two_mul_k line 874 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, HAdd.hAdd, Imo2024P3.Condition.N', OfNat.ofNat, Imo2024P3.Condition.Small, LE.le, Imo2024P3.Condition.p, HMul.hMul, Imo2024P3.Condition.k
Proof uses: Decidable.byContradiction, Not, And, Membership.mem, Finset, Finset.range, Exists, Ne, Eq, False, Eq.mpr, Eq.refl, Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Finset.Icc, of_eq_true, Finset.card, Eq.trans, True, congr, congrArg and 24 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.p_apply_sub_two_le_p_apply line 892 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, HAdd.hAdd, Imo2024P3.Condition.N', OfNat.ofNat, Imo2024P3.Condition.Small, LE.le, Imo2024P3.Condition.p, HSub.hSub
Proof uses: And, Membership.mem, Finset, Finset.Ico, Eq, Exists, Imo2024P3.Condition.exists_apply_sub_two_eq_of_apply_eq, Iff.mpr, lt_add_iff_pos_right, Imo2024P3.Condition.p_pos, Eq.symm, Imo2024P3.Condition.apply_add_p_eq, Imo2024P3.Condition.card_filter_apply_eq_Ico_add_p_le_one, Decidable.byContradiction, Not, Imo2024P3.Condition.apply_sub_two_small_of_apply_small_of_N'_lt, Even, Imo2024P3.Condition.even_p, Finset.card, Finset.filter and 14 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.p_apply_le_p_apply_add_two line 910 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, LT.lt, HAdd.hAdd, Imo2024P3.Condition.N', OfNat.ofNat, Imo2024P3.Condition.Small, LE.le, Imo2024P3.Condition.p
Proof uses: Imo2024P3.Condition.p_apply_sub_two_le_p_apply, Imo2024P3.Condition.apply_add_two_small_of_apply_small_of_N'_le
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.exists_p_eq line 917 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Exists, LT.lt, Eq, Imo2024P3.Condition.p, HAdd.hAdd, Imo2024P3.Condition.N', HMul.hMul, OfNat.ofNat
Proof uses: SupSet.sSup, Set.range, Membership.mem, Set, upperBounds, Imo2024P3.Condition.k, Eq.mpr, LE.le, id, Eq.trans, forall_congr, implies_congr, Eq.refl, Imo2024P3.Condition.p_le_two_mul_k, Iff.mpr, Imo2024P3.Condition.Small, Even, Imo2024P3.Condition.small_apply_N'_add_iff_even, of_eq_true, le_csSup and 16 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma Imo2024P3.Condition.exists_a_apply_add_eq line 940 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Exists, And, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, Imo2024P3.Condition.N', HMul.hMul
Proof uses: Imo2024P3.Condition.p, Imo2024P3.Condition.exists_p_eq, Imo2024P3.Condition.Small, Iff.mpr, Even, Imo2024P3.Condition.small_apply_N'_add_iff_even, of_eq_true, Exists.intro, HDiv.hDiv, And.intro, Imo2024P3.Condition.p_pos, Imo2024P3.Condition.even_p, Eq.rec, Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam and 12 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
problem Imo2024P3.imo2024_p3 line 959 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2024P3.Condition, Or, Imo2024P3.EventuallyPeriodic, HMul.hMul, OfNat.ofNat, HAdd.hAdd
Proof uses: Exists, And, LT.lt, Eq, Imo2024P3.Condition.N', Imo2024P3.Condition.exists_a_apply_add_eq, Even, Odd, Nat.even_or_odd, Or.inl, Exists.intro, LE.le, HDiv.hDiv, And.intro, Eq.mpr, HSub.hSub, eq_of_heq, HEq, Eq.refl, HEq.refl and 4 more
39 instances, coercions and auxiliary constants left out.

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