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

39 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1994, Problem 3

For any positive integer k, let f(k) be the number of elements in the set {k+1, k+2, ... , 2k} which have exactly three 1s when written in base 2. Prove that for each positive integer m, there is at least one k with f(k) = m, and determine all m for which there is exactly one k.

Imports (9)

Imported by 1 file

Compfiles.lean

def Imo1994P3.ones The number of 1s in the binary representation of n line 35 source
Source documentation
The number of 1s in the binary representation of n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: List.sum, Nat.digits, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def ones (n : ℕ) : ℕ := (Nat.digits 2 n).sum
```
def Imo1994P3.f The function f of the problem: the number of elements of {k+1, ..., 2k} whose binary representation has exactly three 1s line 39 source
Source documentation
The function f of the problem: the number of elements of {k+1, ..., 2k} whose binary representation has exactly three 1s.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.card, Finset.filter, Eq, Imo1994P3.ones, OfNat.ofNat, Finset.Icc, HAdd.hAdd, HMul.hMul
8 instances, coercions and auxiliary constants left out.
```
def f (k : ℕ) : ℕ := ((Finset.Icc (k + 1) (2 * k)).filter fun n => ones n = 3).card
```
Mentions: Imo1994P3.ones
determine Imo1994P3.answer line 41 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, Exists, And, LE.le, OfNat.ofNat, Eq, HAdd.hAdd, Nat.choose
4 instances, coercions and auxiliary constants left out.
lemma Imo1994P3.ones_zero line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Imo1994P3.ones, OfNat.ofNat
Proof uses: Eq.mpr, List.sum, Nat.digits, id, congrArg, Imo1994P3.ones.eq_1, List.nil, List, Nat.digits_zero, List.sum_nil, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_mul line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.ones, HMul.hMul, OfNat.ofNat
Proof uses: GT.gt, Or, Nat.eq_zero_or_pos, Eq.refl, Eq.symm, List, Nat.digits, HAdd.hAdd, List.cons, Nat.digits_add, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Bool, Bool.false, Or.inr, Ne, LT.lt.ne', id, Eq.mpr, List.sum and 4 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_mul_add_one line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.ones, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: List, Nat.digits, List.cons, Nat.digits_add, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Or.inl, Ne, one_ne_zero, id, Eq.mpr, List.sum, congrArg, List.sum_cons
22 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_one line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Imo1994P3.ones, OfNat.ofNat
Proof uses: id, Eq.mpr, HAdd.hAdd, HMul.hMul, congrArg, Imo1994P3.ones_two_mul_add_one, Imo1994P3.ones_zero, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Imo1994P3.ones, OfNat.ofNat
Proof uses: id, Eq.mpr, HMul.hMul, congrArg, Imo1994P3.ones_two_mul, Imo1994P3.ones_one, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_mul_pow line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.ones, HMul.hMul, HPow.hPow, OfNat.ofNat
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, pow_zero, one_mul, Eq.refl, HAdd.hAdd, pow_succ', mul_assoc, Imo1994P3.ones_two_mul
24 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_pow line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.ones, HPow.hPow, OfNat.ofNat
Proof uses: Nat.recAux, Imo1994P3.ones_one, Eq.mpr, HAdd.hAdd, HMul.hMul, id, congrArg, pow_succ', Imo1994P3.ones_two_mul, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_pow_add_one line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.ones, HAdd.hAdd, HPow.hPow, OfNat.ofNat
Proof uses: Eq.mpr, HMul.hMul, id, congrArg, pow_succ', Imo1994P3.ones_two_mul_add_one, Imo1994P3.ones_two_pow, Eq.refl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_pow_add_two line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.ones, HAdd.hAdd, HPow.hPow, OfNat.ofNat
Proof uses: HMul.hMul, Eq.mpr, id, congrArg, pow_succ', Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.pow_one_cast_of_isNat and 17 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_pow_add_three line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.ones, HAdd.hAdd, HPow.hPow, OfNat.ofNat
Proof uses: HMul.hMul, Eq.mpr, id, congrArg, pow_succ', Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.pow_one_cast_of_isNat and 19 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_pow_add_four line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.ones, HAdd.hAdd, HPow.hPow, OfNat.ofNat
Proof uses: HMul.hMul, Eq.mpr, id, congrArg, pow_succ', Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.single_pow and 21 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_pow_add_five line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.ones, HAdd.hAdd, HPow.hPow, OfNat.ofNat
Proof uses: HMul.hMul, Eq.mpr, id, congrArg, pow_succ', Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.single_pow and 23 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_pow_add_one' Versions of the above with a hypothesis on the exponent line 103 source
Source documentation
Versions of the above with a hypothesis on the exponent.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Imo1994P3.ones, HAdd.hAdd, HPow.hPow
Proof uses: Exists, Exists.intro, HSub.hSub, Imo1994P3.ones_two_pow_add_one, Eq.symm
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma ones_two_pow_add_one' {n : ℕ} (hn : 1 ≤ n) : ones (2 ^ n + 1) = 2 := by
…
```
Mentions: Imo1994P3.ones
lemma Imo1994P3.ones_two_pow_add_two' line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Imo1994P3.ones, HAdd.hAdd, HPow.hPow
Proof uses: Exists, Exists.intro, HSub.hSub, Imo1994P3.ones_two_pow_add_two, Eq.symm
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_pow_add_three' line 111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Imo1994P3.ones, HAdd.hAdd, HPow.hPow
Proof uses: Exists, Exists.intro, HSub.hSub, Imo1994P3.ones_two_pow_add_three, Eq.symm
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_pow_add_four' line 115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Imo1994P3.ones, HAdd.hAdd, HPow.hPow
Proof uses: Exists, Exists.intro, HSub.hSub, Imo1994P3.ones_two_pow_add_four, Eq.symm
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_two_pow_add_five' line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Imo1994P3.ones, HAdd.hAdd, HPow.hPow
Proof uses: Exists, Exists.intro, HSub.hSub, Imo1994P3.ones_two_pow_add_five, Eq.symm
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_eq_zero line 123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.ones, OfNat.ofNat
Proof uses: Nat.strong_induction_on, LT.lt, GT.gt, Or, Nat.eq_zero_or_pos, Eq.refl, Eq.symm, Even, Odd, Nat.even_or_odd, HMul.hMul, HDiv.hDiv, Nat.two_mul_div_two_of_even, Nat.div_lt_self, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Bool, Bool.false, Eq.mpr, id and 6 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_eq_one line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.ones, OfNat.ofNat, Exists, HPow.hPow
Proof uses: Nat.strong_induction_on, LT.lt, GT.gt, Or, Nat.eq_zero_or_pos, Eq.mp, congrArg, Imo1994P3.ones_zero, Eq.symm, Even, Odd, Nat.even_or_odd, HMul.hMul, HDiv.hDiv, Nat.two_mul_div_two_of_even, Nat.div_lt_self, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool and 11 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.ones_eq_two line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.ones, OfNat.ofNat, Exists, And, LT.lt, HAdd.hAdd, HPow.hPow
Proof uses: Nat.strong_induction_on, GT.gt, Or, Nat.eq_zero_or_pos, Eq.mp, congrArg, Imo1994P3.ones_zero, Eq.symm, Even, Odd, Nat.even_or_odd, HMul.hMul, HDiv.hDiv, Nat.two_mul_div_two_of_even, Nat.div_lt_self, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false and 34 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.add_two_pow_injective line 172 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Function.Injective, HAdd.hAdd, HPow.hPow, OfNat.ofNat
Proof uses: Eq, Nat.pow_right_injective, le_refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Imo1994P3.g Cumulative count: the number of elements of {1, ..., n} with exactly three 1s line 181 source
Source documentation
Cumulative count: the number of elements of {1, ..., n} with exactly three 1s.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.card, Finset.filter, Eq, Imo1994P3.ones, OfNat.ofNat, Finset.Icc
4 instances, coercions and auxiliary constants left out.
```
def g (n : ℕ) : ℕ := ((Finset.Icc 1 n).filter fun m => ones m = 3).card
```
Mentions: Imo1994P3.ones
lemma Imo1994P3.g_succ line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.g, HAdd.hAdd, OfNat.ofNat, ite, Imo1994P3.ones
Proof uses: Finset, Finset.Icc, Insert.insert, Finset.ext, Eq.mpr, Iff, Membership.mem, And, LE.le, Or, id, congr, congrArg, Eq.trans, Finset.card, Finset.filter, Finset.filter_insert, dite, ite_eq_left, Finset.card_insert_of_notMem and 5 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.g_mono line 194 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monotone, Nat, Imo1994P3.g
Proof uses: monotone_nat_of_le_succ, Eq.mpr, LE.le, HAdd.hAdd, OfNat.ofNat, ite, Eq, Imo1994P3.ones, id, congrArg, Imo1994P3.g_succ, Nat.le_add_right
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.f_eq line 197 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.f, HSub.hSub, Imo1994P3.g, HMul.hMul, OfNat.ofNat
Proof uses: Finset, Finset.Icc, Union.union, HAdd.hAdd, Finset.ext, Eq.mpr, Iff, Membership.mem, And, LE.le, Or, id, congr, congrArg, Eq.trans, Disjoint, Not, propext, Finset.disjoint_left, Eq.mp and 8 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.step line 214 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo1994P3.f, HAdd.hAdd, OfNat.ofNat, ite, Imo1994P3.ones, HMul.hMul
Proof uses: Imo1994P3.g, Imo1994P3.g_succ, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq and 27 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.f_mono line 229 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monotone, Nat, Imo1994P3.f
Proof uses: monotone_nat_of_le_succ, Eq.mpr, LE.le, HAdd.hAdd, OfNat.ofNat, ite, Eq, Imo1994P3.ones, HMul.hMul, id, congrArg, Imo1994P3.step, Nat.le_add_right
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.f_zero line 232 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Imo1994P3.f, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.f_ge line 236 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Imo1994P3.f, HAdd.hAdd, HPow.hPow
Proof uses: Finset, Finset.image, HMul.hMul, Finset.range, Finset.filter, Eq, Imo1994P3.ones, Finset.Icc, Membership.mem, And, Exists, Eq.mp, Eq.trans, congrArg, funext, congrFun', Eq.mpr, id, pow_pos, Mathlib.Meta.NormNum.isNat_lt_true and 50 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.card_two_Ico line 266 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Finset.filter, Imo1994P3.ones, OfNat.ofNat, Finset.Ico, HPow.hPow, HAdd.hAdd
Proof uses: Finset, Finset.image, Finset.range, Finset.ext, Eq.mpr, Iff, Membership.mem, And, LE.le, LT.lt, Exists, id, congr, congrArg, Eq.trans, congrFun', funext, Iff.intro, Imo1994P3.ones_eq_two, Decidable.byContradiction and 63 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.card_three_Ioc_succ line 311 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Finset.filter, Imo1994P3.ones, OfNat.ofNat, Finset.Ioc, HPow.hPow, HAdd.hAdd, Finset.Ico
Proof uses: HMul.hMul, pow_succ', Finset, Union.union, Finset.image, Finset.ext, Eq.mpr, Iff, Membership.mem, And, LT.lt, LE.le, Or, Exists, id, congr, congrArg, Eq.trans, congrFun', funext and 23 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.choose_two_succ line 353 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Nat.choose, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, HDiv.hDiv, HMul.hMul, HSub.hSub, id, congrArg, Nat.choose_two_right, Nat.add_sub_cancel, Nat.casesAuxOn, Eq.refl, Eq.symm, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 17 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.card_three line 361 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Finset.filter, Imo1994P3.ones, OfNat.ofNat, Finset.Ioc, HPow.hPow, HAdd.hAdd, Nat.choose
Proof uses: Nat.recAux, Eq.mpr, id, congrFun', congrArg, Finset, Finset.filter.congr_simp, Eq.refl, pow_zero, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Finset.Ico, Imo1994P3.card_three_Ioc_succ, Imo1994P3.card_two_Ico, Imo1994P3.choose_two_succ
24 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo1994P3.f_two_pow_add_two line 370 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Imo1994P3.f, HAdd.hAdd, HPow.hPow, Nat.choose
Proof uses: HMul.hMul, pow_succ', Imo1994P3.ones, Imo1994P3.ones_two_pow_add_one', Imo1994P3.ones_two_pow_add_two', Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.pow_add and 50 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
problem Imo1994P3.imo1994_p3a line 420 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, And, Eq, Imo1994P3.f
Proof uses: LE.le, Exists.intro, HAdd.hAdd, HPow.hPow, Imo1994P3.f_ge, Not, Nat.find, And.intro, Nat.find_spec, Nat.find_min, Ne, False, Eq.mp, congrArg, Imo1994P3.f_zero, Eq.symm, Nat.succ, Nat.exists_eq_succ_of_ne_zero, Nat.lt_succ_self, ite and 10 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
problem Imo1994P3.imo1994_p3b line 441 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Set, Nat, Set.ofPred, And, LT.lt, OfNat.ofNat, ExistsUnique, Imo1994P3.f, Imo1994P3.answer
Proof uses: Set.ext, Iff.intro, Membership.mem, HSub.hSub, LE.le, Imo1994P3.f_mono, Or, lt_or_eq_of_le, Eq.mp, congrArg, Decidable.byContradiction, Not, Imo1994P3.f_zero, rfl, And.intro, HAdd.hAdd, ite, Imo1994P3.ones, HMul.hMul, Imo1994P3.step and 66 more
106 instances, coercions and auxiliary constants left out.

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