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

40 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1992, Problem 6

For each positive integer $n$, $S(n)$ is defined to be the greatest integer such that, for every positive integer $k \le S(n)$, $n^{2}$ can be written as the sum of $k$ positive squares.

(a) Prove that $S(n) \le n^{2}-14$ for each $n \ge 4$.

(b) Find an integer $n$ such that $S(n)=n^{2}-14$.

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo1992P6.is_sum_of_pos_squares $z$ can be written as the sum of $k$ positive squares line 34 source
Source documentation
$z$ can be written as the sum of $k$ positive squares.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, Fin, And, Eq, Finset.sum, Finset.univ, HPow.hPow, OfNat.ofNat, LT.lt
8 instances, coercions and auxiliary constants left out.
```
def is_sum_of_pos_squares (z k : ℕ) : Prop := ∃ s : (Fin k → ℕ), z = ∑ i, (s i)^2 ∧ ∀ i, 0 < s i
```
def Imo1992P6.S_set Auxiliary definition: S(n) will be defined as the greatest integer of the set S_set(n) line 40 source
Source documentation
Auxiliary definition: S(n) will be defined as the greatest integer of the set S_set(n).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Set
Proof uses: Set.ofPred, LE.le, Imo1992P6.is_sum_of_pos_squares, HPow.hPow, Nat, OfNat.ofNat
13 instances, coercions and auxiliary constants left out.
```
def S_set (n : ℕ+) := { z : ℕ+ | ∀ k, k ≤ z → is_sum_of_pos_squares (n^2) k }
```
Mentions: Imo1992P6.is_sum_of_pos_squares
lemma Imo1992P6.S_set_Nonempty line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Set.Nonempty, Imo1992P6.S_set
Proof uses: Set.nonempty_of_mem, OfNat.ofNat, Nat, id, Membership.mem, Set, Set.ofPred, LE.le, Imo1992P6.is_sum_of_pos_squares, HPow.hPow, Exists.intro, Fin, And, Eq, Finset.sum, Finset.univ, LT.lt, of_eq_true, Eq.trans, True and 18 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo1992P6.S_set_bounded line 53 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Membership.mem, Set, Imo1992P6.S_set, LE.le, HPow.hPow, Nat, OfNat.ofNat
Proof uses: id, Set.ofPred, Imo1992P6.is_sum_of_pos_squares, Exists, Fin, And, Eq, Finset.sum, Finset.univ, LT.lt, Eq.mp, Eq.trans, True, implies_congr, Eq.refl, Eq.mpr, congrArg, Eq.symm, propext, PNat.coe_le_coe and 12 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo1992P6.S_set_Finite line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Set.Finite, Imo1992P6.S_set
Proof uses: Set.Finite.of_finite_image, Subtype, Nat, LT.lt, OfNat.ofNat, Iff.mpr, Set.image, BddAbove, Set.finite_iff_bddAbove, Exists, Membership.mem, Set, LE.le, bddAbove_def, Exists.intro, HPow.hPow, And, Eq, Subtype.mk, cast and 4 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def Imo1992P6.S line 75 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat
Proof uses: Exists.choose, Maximal, Membership.mem, Set, Imo1992P6.S_set
9 instances, coercions and auxiliary constants left out.
theorem Imo1992P6.Multiset.map_sub_of_injective line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Function.Injective, Multiset, Eq, Multiset.map, HSub.hSub
Proof uses: Multiset.induction, of_eq_true, OfNat.ofNat, Eq.trans, True, forall_congr, congr, congrArg, Multiset.map_congr, Multiset.sub_zero, Membership.mem, Eq.refl, eq_self, implies_true, Eq.mpr, Multiset.cons, Multiset.erase, id, Multiset.sub_cons, Multiset.map_cons and 3 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.Multiset.sum_sub line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, AddCommMonoid, Multiset, LE.le, Eq, HAdd.hAdd, Multiset.sum, HSub.hSub
Proof uses: Multiset.induction, of_eq_true, OfNat.ofNat, Eq.trans, True, forall_congr, implies_congr, congrFun', congrArg, Multiset.sub_zero, add_zero, eq_self, implies_true, Multiset.cons, Eq.mpr, Multiset.erase, id, congr, Multiset.sub_cons, Multiset.sum_cons and 15 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.Nat.sub_mod line 119 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, Eq, HMod.hMod, HSub.hSub
Proof uses: Eq.mpr, HMul.hMul, HDiv.hDiv, id, congrArg, Nat.mod_eq_sub_div_mul, HAdd.hAdd, Nat.sub_sub_right, Nat.div_mul_le_self, Nat.sub_add_comm, Eq.symm, Nat.add_mul_mod_self_right
16 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.Nat.sub_mod_eq_add_mod line 126 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, Ne, OfNat.ofNat, Eq, HMod.hMod, HSub.hSub, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Nat.add_sub_assoc, le_of_lt, Nat.mod_lt, Nat.zero_lt_of_ne_zero, Nat.sub_add_comm, Trans.simple, Nat.mod_le, Nat.add_mod_right, Imo1992P6.Nat.sub_mod
18 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Imo1992P6.S_spec line 139 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Maximal, LE.le, Imo1992P6.is_sum_of_pos_squares, HPow.hPow, Nat, OfNat.ofNat, Imo1992P6.S
Proof uses: Exists.choose_spec, Membership.mem, Set, Imo1992P6.S_set
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.imo1992_p6_a line 143 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, GE.ge, OfNat.ofNat, Nat, LE.le, Imo1992P6.S, HSub.hSub, HPow.hPow
Proof uses: Classical.byContradiction, Not, And, LT.lt, Exists, False, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, pow_le_pow_left', Eq.mpr, id, Eq, Eq.symm, propext, PNat.coe_lt_coe, Nat.lt_of_add_one_le, HAdd.hAdd and 138 more
202 instances, coercions and auxiliary constants left out.

Tactic trace: 132 steps
Open to load the checked before-and-after goal states.
def Imo1992P6.complete line 282 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat
Proof uses: Eq, Imo1992P6.S, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat
10 instances, coercions and auxiliary constants left out.
theorem Imo1992P6.complete_iff_sos line 284 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, LE.le, OfNat.ofNat, Nat, Iff, Imo1992P6.complete, HSub.hSub, HPow.hPow, Imo1992P6.is_sum_of_pos_squares
Proof uses: Iff.intro, Imo1992P6.S, Maximal.prop, Imo1992P6.S_spec, Eq.mp, congrArg, GE.ge, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, LT.lt, Exists, And, id, Eq, implies_congr, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, funext, Maximal.not_prop_of_gt and 4 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
def Imo1992P6.msos.sq_sum line 298 source
standard axioms: Quot.sound, propext what this means
Statement uses: Multiset, PNat, Nat
Proof uses: Multiset.sum, Multiset.map, HPow.hPow, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
def Imo1992P6.msos.mk line 300 source
standard axioms: Quot.sound what this means
Statement uses: List, Prod, Nat, PNat, Multiset
Proof uses: List.foldr, HAdd.hAdd, EmptyCollection.emptyCollection, List.map, Imo1992P6.msos.mk.match_1, Multiset.replicate
3 instances, coercions and auxiliary constants left out.
theorem Imo1992P6.msos.is_sum_of_pos_squares line 302 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Multiset, PNat, Imo1992P6.is_sum_of_pos_squares, Imo1992P6.msos.sq_sum, Multiset.card
Proof uses: Multiset.induction, id, OfNat.ofNat, Exists.intro, Fin, Nat, And, Eq, Multiset.sum, Multiset.map, HPow.hPow, Finset.sum, Finset.univ, LT.lt, of_eq_true, Eq.trans, True, congr, congrArg, funext and 68 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
def Imo1992P6.msos.shift line 354 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Multiset, PNat, Nat
Proof uses: HAdd.hAdd, HSub.hSub, Multiset.replicate, HMul.hMul, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.
theorem Imo1992P6.msos.card_shift line 358 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Multiset, PNat, Nat, LE.le, HMul.hMul, OfNat.ofNat, Multiset.count, Eq, HAdd.hAdd, Multiset.card, Imo1992P6.msos.shift
Proof uses: id, Eq.mpr, HSub.hSub, Multiset.replicate, congrFun', congrArg, Eq.trans, Multiset.card_add, Multiset.card_replicate, Multiset.card_sub, Iff.mp, Multiset.le_count_iff_replicate_le, Int, Nat.cast_add, congr, Nat.cast_mul, Nat.cast_sub, Trans.simple, Multiset.count_le_card
49 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.msos.sq_sum_shift line 371 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Multiset, PNat, Nat, LE.le, HMul.hMul, OfNat.ofNat, Multiset.count, Eq, Imo1992P6.msos.sq_sum, Imo1992P6.msos.shift
Proof uses: id, Multiset.sum, Multiset.map, HPow.hPow, Eq.mpr, HAdd.hAdd, HSub.hSub, Multiset.replicate, congrArg, Multiset.map_add, Multiset.map_replicate, Imo1992P6.Multiset.map_sub_of_injective, of_eq_true, Eq.trans, True, congrFun', Eq.mp, Not, False, not_false_eq_true and 14 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
def Imo1992P6.msos.repeat_shift line 392 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Multiset, PNat
Proof uses: WellFounded.Nat.fix, Multiset.card, InvImage, Nat, LT.lt, Multiset.filter, LE.le, OfNat.ofNat, Multiset.count, dite, Eq, EmptyCollection.emptyCollection, Not, Finset.min', Multiset.toFinset, HDiv.hDiv, Imo1992P6.msos.shift
12 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.msos.repeat_shift.forall line 413 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Multiset, PNat, Nat, LE.le, HDiv.hDiv, HSub.hSub, Multiset.card, Imo1992P6.msos.repeat_shift, OfNat.ofNat, Exists, And, Eq, Imo1992P6.msos.sq_sum, HAdd.hAdd, HMul.hMul
Proof uses: Imo1992P6.msos.repeat_shift.induct_unfolding, Multiset.filter, Multiset.count, EmptyCollection.emptyCollection, Exists.intro, of_eq_true, Eq.trans, True, congr, congrArg, eq_self, congrFun', Eq.mp, tsub_self, Nat.zero_div, MulZeroClass.mul_zero, add_zero, and_self, Not, Finset.min' and 12 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.msos.card_repeat_shift_le_card line 441 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Multiset, PNat, LE.le, Nat, Multiset.card, Imo1992P6.msos.repeat_shift
Proof uses: Imo1992P6.msos.repeat_shift.induct_unfolding, Multiset.filter, OfNat.ofNat, Multiset.count, Eq, EmptyCollection.emptyCollection, le_refl, Not, Finset.min', Multiset.toFinset, HDiv.hDiv, Imo1992P6.msos.shift, le_trans, HAdd.hAdd, HMul.hMul, Nat.le_add_right_of_le, le_of_eq, Imo1992P6.msos.card_shift, Nat.mul_div_le
15 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.msos.card_repeat_shift_le line 450 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Multiset, PNat, LE.le, Nat, Multiset.card, Imo1992P6.msos.repeat_shift, HSub.hSub, HMul.hMul, HDiv.hDiv, Multiset.count, OfNat.ofNat
Proof uses: Imo1992P6.msos.repeat_shift.fun_cases_unfolding, Multiset.filter, Eq, EmptyCollection.emptyCollection, Eq.mpr, Or, LT.lt, id, congrArg, propext, Nat.div_eq_zero_iff, Or.inr, dite, Membership.mem, Eq.mp, Eq.trans, Not, forall_congr, implies_congr, Eq.refl and 36 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.is_sum_of_pos_squares_by_repeat_shift line 493 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Multiset, PNat, Nat, Membership.mem, Finset, Finset.Icc, Multiset.card, Imo1992P6.msos.repeat_shift, Eq, HMod.hMod, OfNat.ofNat, Imo1992P6.is_sum_of_pos_squares, Imo1992P6.msos.sq_sum
Proof uses: HDiv.hDiv, HSub.hSub, And, HAdd.hAdd, HMul.hMul, Exists, Imo1992P6.msos.repeat_shift.forall, id, LE.le, Nat.div_le_div_right, And.left, Iff.mp, Finset.mem_Icc, Eq.mp, Int, congrArg, Nat.cast_sub, And.right, Eq.trans, congrFun' and 6 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.msos.card_mk line 516 source
standard axioms: Quot.sound, propext what this means
Statement uses: List, Prod, Nat, PNat, Eq, Multiset.card, Imo1992P6.msos.mk, List.sum, List.map, Prod.fst
Proof uses: List.rec, id, List.nil, of_eq_true, List.foldr, Multiset, HAdd.hAdd, EmptyCollection.emptyCollection, Imo1992P6.msos.mk.match_1, Multiset.replicate, Eq.trans, OfNat.ofNat, True, congr, congrArg, List.map_nil, Prod.snd, eq_self, List.cons, Eq.mpr and 5 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.msos.sq_sum_mk line 530 source
standard axioms: Quot.sound, propext what this means
Statement uses: List, Prod, Nat, PNat, Eq, Imo1992P6.msos.sq_sum, Imo1992P6.msos.mk, List.sum, List.map, Imo1992P6.msos.mk.match_1, HMul.hMul, HPow.hPow, OfNat.ofNat
Proof uses: List.rec, id, List.nil, List.foldr, Multiset, HAdd.hAdd, EmptyCollection.emptyCollection, Multiset.replicate, of_eq_true, Multiset.sum, Multiset.map, Eq.trans, True, congr, congrArg, List.map_nil, Prod.fst, Prod.snd, eq_self, List.cons and 8 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.msos.count_mk line 544 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Nat, PNat, Eq, Multiset.count, Imo1992P6.msos.mk, List.sum, List.map, Prod.fst, List.filter, BEq.beq, Prod.snd
Proof uses: List.rec, id, List.nil, of_eq_true, List.foldr, Multiset, HAdd.hAdd, EmptyCollection.emptyCollection, Imo1992P6.msos.mk.match_1, Multiset.replicate, Eq.trans, OfNat.ofNat, True, congr, congrArg, Multiset.count.congr_simp, Eq.refl, List.map_nil, Multiset.count_eq_zero_of_notMem, Not and 28 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.sos_13_0mod3 line 567 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, LE.le, HSub.hSub, HPow.hPow, Eq, HMod.hMod, Imo1992P6.is_sum_of_pos_squares
Proof uses: dite, Multiset, PNat, Imo1992P6.msos.mk, List.cons, Prod, Prod.mk, List.nil, Imo1992P6.msos.sq_sum, Eq.mpr, id, congrArg, Eq.symm, Imo1992P6.is_sum_of_pos_squares_by_repeat_shift, Membership.mem, Finset, Finset.Icc, Multiset.card, Imo1992P6.msos.repeat_shift, And and 21 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.sos_13_1mod3 line 601 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HSub.hSub, HPow.hPow, OfNat.ofNat, Eq, HMod.hMod, Imo1992P6.is_sum_of_pos_squares
Proof uses: dite, Multiset, PNat, Imo1992P6.msos.mk, List.cons, Prod, Prod.mk, List.nil, Imo1992P6.msos.sq_sum, Eq.mpr, id, congrArg, Eq.symm, Imo1992P6.is_sum_of_pos_squares_by_repeat_shift, Membership.mem, Finset, Finset.Icc, Multiset.card, Imo1992P6.msos.repeat_shift, And and 21 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.sos_13_2mod3 line 635 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HSub.hSub, HPow.hPow, OfNat.ofNat, Eq, HMod.hMod, Imo1992P6.is_sum_of_pos_squares
Proof uses: dite, Multiset, PNat, Imo1992P6.msos.mk, List.cons, Prod, Prod.mk, List.nil, Imo1992P6.msos.sq_sum, Eq.mpr, id, congrArg, Eq.symm, Imo1992P6.is_sum_of_pos_squares_by_repeat_shift, Membership.mem, Finset, Finset.Icc, Multiset.card, Imo1992P6.msos.repeat_shift, And and 19 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.complete_13 line 660 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo1992P6.complete, OfNat.ofNat, PNat, Nat
Proof uses: Eq.mpr, LE.le, HSub.hSub, HPow.hPow, Imo1992P6.is_sum_of_pos_squares, id, Eq, congrArg, propext, Imo1992P6.complete_iff_sos, of_eq_true, Eq.trans, True, eq_true_of_decide, Eq.refl, Bool, Bool.true, Or, HMod.hMod, Or.elim3 and 4 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.sos_mul_const line 670 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1992P6.is_sum_of_pos_squares, HMul.hMul, HPow.hPow
Proof uses: Fin, Eq, Finset.sum, Finset.univ, Exists.intro, And, And.intro, Eq.mpr, id, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, mul_pow, Eq.symm, Finset.mul_sum, mul_comm, of_eq_true, Eq.trans and 2 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.sos_add line 679 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1992P6.is_sum_of_pos_squares, HAdd.hAdd
Proof uses: Fin, Eq, Finset.sum, Finset.univ, HPow.hPow, OfNat.ofNat, LT.lt, Exists.intro, And, dite, Fin.mk, Not, HSub.hSub, And.intro, Eq.mpr, Subtype, Membership.mem, Finset, Finset.filter, id and 35 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.sos_mul line 699 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo1992P6.is_sum_of_pos_squares, HMul.hMul
Proof uses: Fin, Eq, Finset.sum, Finset.univ, HPow.hPow, OfNat.ofNat, LT.lt, Equiv, Prod, Equiv.symm, finProdFinEquiv, Exists.intro, And, Function.uncurry, And.intro, Eq.mpr, id, congrArg, Finset.sum_mul_sum, Eq.symm and 38 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.sos_split line 733 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Imo1992P6.is_sum_of_pos_squares, Exists, And, LT.lt, HPow.hPow, HSub.hSub
Proof uses: Fin, Eq, Finset.sum, Finset.univ, Exists.intro, Fin.mk, And.intro, Eq.mpr, id, congrArg, Finset.single_le_sum_of_canonicallyOrdered, of_eq_true, Membership.mem, Finset, Fin.castLT, Finset.sum_congr, Eq.refl, HAdd.hAdd, propext, Nat.sub_eq_iff_eq_add and 24 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
theorem Imo1992P6.complete_mul line 762 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, LE.le, OfNat.ofNat, Nat, Imo1992P6.complete, HMul.hMul
Proof uses: HSub.hSub, HPow.hPow, mul_le_mul', Eq.mpr, Imo1992P6.is_sum_of_pos_squares, id, Eq, congrArg, propext, Imo1992P6.complete_iff_sos, Trans.simple, Iff.mp, Min.min, right_eq_inf, rfl, dite, Eq.symm, Eq.refl, PNat.mul_coe, Nat.pow_le_pow_left and 218 more
283 instances, coercions and auxiliary constants left out.

Tactic trace: 327 steps (first 200 of 327)
Open to load the checked before-and-after goal states.
theorem Imo1992P6.imo1992_p6_c line 1016 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.Infinite, PNat, Set.ofPred, Eq, Imo1992P6.S, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat
Proof uses: GT.gt, Imo1992P6.complete, Nat.le_induction, Nat.succ, LE.le, of_eq_true, Eq.trans, True, congrArg, zero_add, pow_one, Eq.mpr, HAdd.hAdd, HMul.hMul, id, pow_add, Imo1992P6.complete_mul, Eq.symm, pow_right_monotone, Nat.one_le_of_lt and 11 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
determine Imo1992P6.imo1992_p6_b line 1046 source
standard axioms: propext what this means
Statement uses: PNat
Proof uses: OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
problem Imo1992P6.imo1992_p6 line 1048 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, PNat, GE.ge, OfNat.ofNat, Nat, LE.le, Imo1992P6.S, HSub.hSub, HPow.hPow, Eq, Imo1992P6.imo1992_p6_b, Set.Infinite, Set.ofPred
Proof uses: And.intro, Imo1992P6.imo1992_p6_a, Imo1992P6.complete_13, Imo1992P6.imo1992_p6_c
34 instances, coercions and auxiliary constants left out.

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