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

41 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1997, Problem 4

An $n \times n$ matrix whose entries come from the set $S = \{1, 2, \ldots, 2n - 1\}$ is called a silver matrix if, for each $i = 1, \ldots, n$, the $i$-th row and the $i$-th column together contain all elements of $S$. Show that:

(a) there is no silver matrix for $n = 1997$;

(b) silver matrices exist for infinitely many values of $n$.

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo1997P4.SilverMatrix An n × n matrix M is a silver matrix if its entries come from S = {1, …, 2n - 1} and, for each i, the i-th row and the i-th column together contain all of S line 35 source
Source documentation
An n × n matrix M is a silver matrix if its entries come from S = {1, …, 2n - 1} and, for each i, the i-th row and the i-th column together contain all of S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin
Proof uses: And, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, HSub.hSub, HMul.hMul, Eq, Union.union, Finset.image, Finset.univ
12 instances, coercions and auxiliary constants left out.
```
def SilverMatrix (n : ℕ) (M : Fin n → Fin n → ℕ) : Prop :=
…
```
def Imo1997P4.row line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, Prod
Proof uses: SProd.sprod, Singleton.singleton, Finset.univ
3 instances, coercions and auxiliary constants left out.
def Imo1997P4.col line 48 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, Prod
Proof uses: SProd.sprod, Finset.univ, Singleton.singleton
3 instances, coercions and auxiliary constants left out.
def Imo1997P4.cross line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, Prod
Proof uses: Union.union, Imo1997P4.row, Imo1997P4.col
3 instances, coercions and auxiliary constants left out.
lemma Imo1997P4.card_row line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset.card, Prod, Imo1997P4.row
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.univ, Finset.map, Function.Embedding.sectR, Finset, Finset.singleton_product, Finset.card_map, Fintype.card_fin, eq_self
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.card_col line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset.card, Prod, Imo1997P4.col
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.univ, Finset.map, Function.Embedding.sectL, Finset, Finset.product_singleton, Finset.card_map, Fintype.card_fin, eq_self
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.row_mem line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Membership.mem, Prod, Finset, Imo1997P4.row, Prod.mk
Proof uses: Finset.mk_mem_product, Singleton.singleton, Finset.univ, Finset.mem_singleton_self, Finset.mem_univ
4 instances, coercions and auxiliary constants left out.
lemma Imo1997P4.col_mem line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Membership.mem, Prod, Finset, Imo1997P4.col, Prod.mk
Proof uses: Finset.mk_mem_product, Finset.univ, Singleton.singleton, Finset.mem_univ, Finset.mem_singleton_self
4 instances, coercions and auxiliary constants left out.
lemma Imo1997P4.cross_mem_left line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Membership.mem, Prod, Finset, Imo1997P4.cross, Prod.mk
Proof uses: Finset.mem_union_left, Imo1997P4.row, Imo1997P4.col, Imo1997P4.row_mem
4 instances, coercions and auxiliary constants left out.
lemma Imo1997P4.row_union line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Prod, Fin, Finset.biUnion, Finset.univ, Imo1997P4.row
Proof uses: Iff.mpr, Membership.mem, Finset.eq_univ_iff_forall, Prod.mk, Exists, And, Finset.mem_biUnion, Exists.intro, And.intro, Finset.mem_univ, Imo1997P4.row_mem
11 instances, coercions and auxiliary constants left out.
lemma Imo1997P4.col_union line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Prod, Fin, Finset.biUnion, Finset.univ, Imo1997P4.col
Proof uses: Iff.mpr, Membership.mem, Finset.eq_univ_iff_forall, Prod.mk, Exists, And, Finset.mem_biUnion, Exists.intro, And.intro, Finset.mem_univ, Imo1997P4.col_mem
11 instances, coercions and auxiliary constants left out.
lemma Imo1997P4.row_disjoint line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.PairwiseDisjoint, Finset, Prod, Fin, Set.univ, Imo1997P4.row
Proof uses: Membership.mem, Set, Ne, Iff.mpr, Disjoint, SProd.sprod, Singleton.singleton, Finset.univ, Or, Finset.disjoint_product, Or.inl, Finset.disjoint_singleton
8 instances, coercions and auxiliary constants left out.
lemma Imo1997P4.col_disjoint line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.PairwiseDisjoint, Finset, Prod, Fin, Set.univ, Imo1997P4.col
Proof uses: Membership.mem, Set, Ne, Iff.mpr, Disjoint, SProd.sprod, Finset.univ, Singleton.singleton, Or, Finset.disjoint_product, Or.inr, Finset.disjoint_singleton
8 instances, coercions and auxiliary constants left out.
lemma Imo1997P4.row_inter_col line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Prod, Inter.inter, Imo1997P4.row, Imo1997P4.col, Singleton.singleton, Prod.mk
Proof uses: Eq.mpr, SProd.sprod, Finset.univ, id, congrArg, Imo1997P4.row.eq_1, Imo1997P4.col.eq_1, Finset.product_inter_product, of_eq_true, Eq.trans, True, congrFun', Finset.map, Function.Embedding.sectL, congr, Finset.inter_univ, Finset.inter_singleton_of_mem, Membership.mem, Finset.product_singleton, Function.Embedding and 3 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.card_cross line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset.card, Prod, Imo1997P4.cross, HSub.hSub, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, Union.union, Finset, Imo1997P4.row, Imo1997P4.col, id, congrArg, Imo1997P4.cross.eq_1, HAdd.hAdd, Inter.inter, Finset.card_union, Imo1997P4.card_row, Imo1997P4.card_col, Singleton.singleton, Prod.mk, Imo1997P4.row_inter_col, Finset.card_singleton, Nat.two_mul, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.image_row line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Finset.image, Finset.univ, Prod, Function.HasUncurry.uncurry, Imo1997P4.row
Proof uses: Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Exists, True, congr, congrArg, And, funext, congrFun', true_and, Finset.map, Function.Embedding.sectR, Prod.fst, Prod.snd, Prod.mk, Finset.singleton_product, Function.Embedding and 2 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.image_col line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Finset.image, Finset.univ, Prod, Function.HasUncurry.uncurry, Imo1997P4.col
Proof uses: Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Exists, True, congr, congrArg, And, funext, congrFun', true_and, Finset.map, Function.Embedding.sectL, Prod.fst, Prod.snd, Prod.mk, Finset.product_singleton, Function.Embedding and 2 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.image_cross line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo1997P4.SilverMatrix, Eq, Finset, Finset.image, Prod, Function.HasUncurry.uncurry, Imo1997P4.cross, Finset.Icc, OfNat.ofNat, HSub.hSub, HMul.hMul
Proof uses: Eq.mpr, Union.union, Imo1997P4.row, Imo1997P4.col, id, congrArg, Imo1997P4.cross.eq_1, Finset.image_union, Finset.univ, Eq.symm, Imo1997P4.image_row, Imo1997P4.image_col, And.right, Membership.mem
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.silver_iff_cross line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Iff, Imo1997P4.SilverMatrix, Eq, Finset, Finset.image, Prod, Function.HasUncurry.uncurry, Imo1997P4.cross, Finset.Icc, OfNat.ofNat, HSub.hSub, HMul.hMul
Proof uses: Iff.intro, Imo1997P4.image_cross, And.intro, Membership.mem, Union.union, Finset.univ, Eq.mpr, id, congrArg, Eq.symm, Iff.mpr, Exists, And, Finset.mem_image, Exists.intro, Prod.mk, Imo1997P4.cross_mem_left, rfl, Imo1997P4.row, Imo1997P4.image_row and 5 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.val_map_cross line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo1997P4.SilverMatrix, Eq, Multiset, Multiset.map, Prod, Function.HasUncurry.uncurry, Finset.val, Imo1997P4.cross, Multiset.Icc, OfNat.ofNat, HSub.hSub, HMul.hMul
Proof uses: Eq.mpr, Finset.image, id, congrArg, Eq.symm, Finset.image_val_of_injOn, Finset.injOn_of_card_image_eq, of_eq_true, Finset.card, Eq.trans, True, congr, HAdd.hAdd, Finset.Icc, Finset, Imo1997P4.image_cross, Nat.card_Icc, add_tsub_cancel_right, Imo1997P4.card_cross, eq_self and 1 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.multiset_row_col line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo1997P4.SilverMatrix, Eq, Multiset, HAdd.hAdd, Multiset.map, Prod, Function.HasUncurry.uncurry, Finset.val, Imo1997P4.row, Imo1997P4.col, Multiset.cons, Multiset.Icc, OfNat.ofNat, HSub.hSub, HMul.hMul
Proof uses: Eq.mpr, Imo1997P4.cross, id, congrArg, Eq.symm, Imo1997P4.val_map_cross, Multiset.map_add, Union.union, Inter.inter, Multiset.union_add_inter, Finset, Finset.union_val, Finset.inter_val, Singleton.singleton, Prod.mk, Imo1997P4.row_inter_col, Finset.singleton_val, Multiset.map_singleton, Multiset.singleton_add, add_comm and 1 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.sum_row_val line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Multiset, Prod, Fin, Finset.sum, Finset.univ, Finset.val, Imo1997P4.row
Proof uses: Eq.mpr, Finset.biUnion, id, congrArg, Finset, Eq.symm, Imo1997P4.row_union, Finset.disjiUnion, Set.PairwiseDisjoint, Set.univ, congrFun', Set, Finset.coe_univ, Imo1997P4.row_disjoint, Finset.disjiUnion_eq_biUnion, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.sum_col_val line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Multiset, Prod, Fin, Finset.sum, Finset.univ, Finset.val, Imo1997P4.col
Proof uses: Eq.mpr, Finset.biUnion, id, congrArg, Finset, Eq.symm, Imo1997P4.col_union, Finset.disjiUnion, Set.PairwiseDisjoint, Set.univ, congrFun', Set, Finset.coe_univ, Imo1997P4.col_disjoint, Finset.disjiUnion_eq_biUnion, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.sum_row_col_val line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Multiset, Finset.sum, Finset.univ, HAdd.hAdd, Multiset.map, Prod, Function.HasUncurry.uncurry, Finset.val, Imo1997P4.row, Imo1997P4.col, HSMul.hSMul, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, AddMonoidHom, Multiset.mapAddMonoidHom, True, congr, congrArg, Finset.sum_add_distrib, Imo1997P4.sum_row_val, Imo1997P4.sum_col_val, two_nsmul, eq_self
33 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.sum_row_col_val_silver line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Imo1997P4.SilverMatrix, Eq, Multiset, Finset.sum, Finset.univ, HAdd.hAdd, Multiset.map, Prod, Function.HasUncurry.uncurry, Finset.val, Imo1997P4.row, Imo1997P4.col, HSMul.hSMul, Multiset.Icc, OfNat.ofNat, HSub.hSub, HMul.hMul
Proof uses: Eq.mpr, Multiset.cons, id, congrFun', congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Imo1997P4.multiset_row_col, Singleton.singleton, Finset.sum_add_distrib, Finset.card, Finset.sum_const, Fintype.card, Fintype.card_fin, Multiset.map_congr, AddMonoidHom, Multiset.mapAddMonoidHom, map_sum
47 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.exists_diag_count_zero line 139 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, Exists, And, Membership.mem, Multiset, Multiset.Icc, HSub.hSub, HMul.hMul, Eq, Multiset.count, Multiset.map, Finset.val, Finset.univ
Proof uses: Eq.mpr, id, congrArg, rfl, Finset.card, Multiset.toFinset, Finset.Icc, LE.le, List.toFinset, List.ofFn, congrFun', Finset, Eq.trans, Fin.univ_val_map, Eq.mp, Multiset.card, congr, List.length_ofFn, Multiset.toFinset_card_le, HAdd.hAdd and 5 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.no_odd_SilverMatrix line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Odd, Not, Exists, Fin, Imo1997P4.SilverMatrix
Proof uses: False, And, Membership.mem, Multiset, Multiset.Icc, HSub.hSub, HMul.hMul, Eq, Multiset.count, Multiset.map, Finset.val, Finset.univ, Imo1997P4.exists_diag_count_zero, Even, Finset.sum, HAdd.hAdd, Prod, Function.HasUncurry.uncurry, Imo1997P4.row, Imo1997P4.col and 15 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def Imo1997P4.blockMatrix line 164 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd
Proof uses: Matrix.fromBlocks, Equiv, Sum, Equiv.symm, finSumFinEquiv
7 instances, coercions and auxiliary constants left out.
lemma Imo1997P4.blockMatrix_row_left line 167 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Finset.image, Prod, HAdd.hAdd, Function.HasUncurry.uncurry, Imo1997P4.blockMatrix, Imo1997P4.row, Equiv, Sum, finSumFinEquiv, Sum.inl, Union.union
Proof uses: Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Or, Exists, True, congr, congrArg, And, Finset.univ, Sum.elim, Equiv.symm, Sum.inr, congrFun', Fin.castAdd, funext, Matrix, Matrix.of and 6 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.blockMatrix_row_right line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Finset.image, Prod, HAdd.hAdd, Function.HasUncurry.uncurry, Imo1997P4.blockMatrix, Imo1997P4.row, Equiv, Sum, finSumFinEquiv, Sum.inr, Union.union
Proof uses: Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Or, Exists, True, congr, congrArg, And, Finset.univ, Sum.elim, Equiv.symm, Sum.inl, congrFun', funext, Matrix, Matrix.of, Equiv.symm_apply_apply and 4 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.blockMatrix_col_left line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Finset.image, Prod, HAdd.hAdd, Function.HasUncurry.uncurry, Imo1997P4.blockMatrix, Imo1997P4.col, Equiv, Sum, finSumFinEquiv, Sum.inl, Union.union
Proof uses: Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Or, Exists, True, congr, congrArg, And, Finset.univ, Sum.elim, Equiv.symm, Sum.inr, congrFun', Fin.castAdd, funext, Matrix, Matrix.of and 6 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.blockMatrix_col_right line 188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Finset.image, Prod, HAdd.hAdd, Function.HasUncurry.uncurry, Imo1997P4.blockMatrix, Imo1997P4.col, Equiv, Sum, finSumFinEquiv, Sum.inr, Union.union
Proof uses: Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Or, Exists, True, congr, congrArg, And, Finset.univ, Sum.elim, Equiv.symm, Sum.inl, congrFun', funext, Matrix, Matrix.of, Equiv.symm_apply_apply and 4 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.blockMatrix_cross_left line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Finset.image, Prod, HAdd.hAdd, Function.HasUncurry.uncurry, Imo1997P4.blockMatrix, Imo1997P4.cross, Equiv, Sum, finSumFinEquiv, Sum.inl, Union.union, Imo1997P4.row, Imo1997P4.col
Proof uses: Eq.mpr, id, congrArg, Imo1997P4.cross.eq_1, Finset.image_union, Imo1997P4.blockMatrix_row_left, Imo1997P4.blockMatrix_col_left, congr, Lean.Data.AC.Context.eq_of_norm, Lean.Data.AC.Context.mk, Option.some, PLift, Std.Commutative, PLift.up, Std.IdempotentOp, List.cons, Lean.Data.AC.Variable, Lean.Data.AC.Variable.mk, Option.none, Std.LawfulIdentity and 7 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.blockMatrix_cross_right line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Finset.image, Prod, HAdd.hAdd, Function.HasUncurry.uncurry, Imo1997P4.blockMatrix, Imo1997P4.cross, Equiv, Sum, finSumFinEquiv, Sum.inr, Union.union, Imo1997P4.row, Imo1997P4.col
Proof uses: Eq.mpr, id, congrArg, Imo1997P4.cross.eq_1, Finset.image_union, Imo1997P4.blockMatrix_row_right, Imo1997P4.blockMatrix_col_right, congr, Lean.Data.AC.Context.eq_of_norm, Lean.Data.AC.Context.mk, Option.some, PLift, Std.Commutative, PLift.up, Std.IdempotentOp, List.cons, Lean.Data.AC.Variable, Lean.Data.AC.Variable.mk, Option.none, Std.LawfulIdentity and 7 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo1997P4.latinSquare line 209 source
no axioms what this means
Statement uses: Nat, Fin
Proof uses: HSub.hSub
2 instances, coercions and auxiliary constants left out.
lemma Imo1997P4.latinSquare_row line 211 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Finset.image, Prod, Function.HasUncurry.uncurry, Imo1997P4.latinSquare, Imo1997P4.row, Finset.univ
Proof uses: NeZero, NeZero.mk, LT.lt.ne', OfNat.ofNat, Fin.pos, Eq.mpr, id, congrArg, Eq.symm, Imo1997P4.image_row, Function.comp, Equiv, Equiv.subLeft, rfl, Finset.image_image, Finset.image_univ_equiv, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.latinSquare_col line 217 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Finset, Finset.image, Prod, Function.HasUncurry.uncurry, Imo1997P4.latinSquare, Imo1997P4.col, Finset.univ
Proof uses: NeZero, NeZero.mk, LT.lt.ne', OfNat.ofNat, Fin.pos, Eq.mpr, id, congrArg, Eq.symm, Imo1997P4.image_col, Function.comp, Equiv, Equiv.subRight, rfl, Finset.image_image, Finset.image_univ_equiv, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.Icc_union' line 223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, LE.le, Eq, Finset, Union.union, Finset.Icc, HSub.hSub, OfNat.ofNat
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Or, id, congr, congrArg, Eq.trans
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.silver_double line 226 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Fin, Imo1997P4.SilverMatrix, HAdd.hAdd
Proof uses: Exists.intro, Imo1997P4.blockMatrix, Imo1997P4.latinSquare, OrderEmbedding, Finset.orderEmbOfFin, Finset.Icc, HMul.hMul, HSub.hSub, Eq.mpr, Eq, Finset.card, id, congrArg, Nat.card_Icc, Iff.mpr, Finset, Finset.image, Prod, Function.HasUncurry.uncurry, Imo1997P4.cross and 43 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo1997P4.silver_two_pow line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Fin, HPow.hPow, OfNat.ofNat, Imo1997P4.SilverMatrix
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
problem Imo1997P4.imo1997_p4 line 249 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Not, Exists, Fin, OfNat.ofNat, Nat, Imo1997P4.SilverMatrix, Set.Infinite, Set.ofPred
Proof uses: And.intro, Imo1997P4.no_odd_SilverMatrix, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Exists.intro, Eq, HAdd.hAdd, HMul.hMul, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.isNat_mul, Set.infinite_of_injective_forall_mem, HPow.hPow, Nat.pow_right_injective, le_rfl, Imo1997P4.silver_two_pow
31 instances, coercions and auxiliary constants left out.

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