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

76 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2004, Problem 3

Define a "hook" to be a figure made up of six unit squares as shown below in the picture (a 3 × 3 square with the centre square, the middle square of one side, and a corner square adjacent to that middle square removed), or any of the figures obtained by applying rotations and reflections to this figure.

Which m × n rectangles can be tiled by hooks?

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo2004P3.rect The cells of an m × n rectangle, as a finite subset of ℤ × ℤ line 31 source
Source documentation
The cells of an m × n rectangle, as a finite subset of ℤ × ℤ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Int
Proof uses: Finset.image, Prod.mk, Prod.fst, Prod.snd, SProd.sprod, Finset.range
5 instances, coercions and auxiliary constants left out.
```
def rect (m n : ℕ) : Finset (ℤ × ℤ) :=
…
```
def Imo2004P3.hookShapes The eight orientations of the hook (rotations and reflections of the figure in the problem statement) line 38 source
Source documentation
The eight orientations of the hook (rotations and reflections of the figure in the problem statement). Each orientation is a 3 × 3 square with three cells removed: the centre cell, the middle cell of one side, and a corner cell adjacent to that middle cell.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: Insert.insert, Prod.mk, OfNat.ofNat, Singleton.singleton
6 instances, coercions and auxiliary constants left out.
```
def hookShapes : Finset (Finset (ℤ × ℤ)) :=
…
```
def Imo2004P3.IsHook A hook is a translate of one of the eight orientations line 49 source
Source documentation
A hook is a translate of one of the eight orientations.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: Exists, And, Membership.mem, Imo2004P3.hookShapes, Eq, Finset.image, HAdd.hAdd
7 instances, coercions and auxiliary constants left out.
```
def IsHook (s : Finset (ℤ × ℤ)) : Prop := ∃ σ ∈ hookShapes, ∃ t, s = σ.image (· + t)
```
Mentions: Imo2004P3.hookShapes
def Imo2004P3.Tileable R can be tiled by hooks: there is a finite family of pairwise disjoint hooks whose union is R line 53 source
Source documentation
R can be tiled by hooks: there is a finite family of pairwise disjoint hooks whose union is R.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: Exists, And, Membership.mem, Imo2004P3.IsHook, Ne, Disjoint, Eq, Finset.biUnion, id
6 instances, coercions and auxiliary constants left out.
```
def Tileable (R : Finset (ℤ × ℤ)) : Prop :=
…
```
def Imo2004P3.tileShapes The six orientations of the two-hook "tiles" (pairs of interlocking hooks): the 3 × 4 rectangle, the 4 × 3 rectangle, and the four orientations of the zigzag shape line 62 source
Source documentation
The six orientations of the two-hook "tiles" (pairs of interlocking hooks): the 3 × 4 rectangle, the 4 × 3 rectangle, and the four orientations of the zigzag shape.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: Insert.insert, Prod.mk, OfNat.ofNat, Singleton.singleton
6 instances, coercions and auxiliary constants left out.
```
def tileShapes : Finset (Finset (ℤ × ℤ)) :=
…
```
def Imo2004P3.IsTile A tile is a translate of one of the six tile shapes line 71 source
Source documentation
A tile is a translate of one of the six tile shapes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: Exists, And, Membership.mem, Imo2004P3.tileShapes, Eq, Finset.image, HAdd.hAdd
7 instances, coercions and auxiliary constants left out.
```
def IsTile (s : Finset (ℤ × ℤ)) : Prop := ∃ τ ∈ tileShapes, ∃ t, s = τ.image (· + t)
```
Mentions: Imo2004P3.tileShapes
def Imo2004P3.lo The lower-left corner of the bounding box of a set of cells line 74 source
Source documentation
The lower-left corner of the bounding box of a set of cells.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: Prod.mk, Option.getD, Finset.min, Finset.image, Prod.fst, OfNat.ofNat, Prod.snd
3 instances, coercions and auxiliary constants left out.
```
def lo (s : Finset (ℤ × ℤ)) : ℤ × ℤ :=
…
```
def Imo2004P3.hole The "hole" (notch) of a hook: the centre cell of its bounding box line 78 source
Source documentation
The "hole" (notch) of a hook: the centre cell of its bounding box.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: HAdd.hAdd, Imo2004P3.lo, Prod.mk, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def hole (s : Finset (ℤ × ℤ)) : ℤ × ℤ := lo s + (1, 1)
```
Mentions: Imo2004P3.lo
lemma Imo2004P3.mem_rect line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, Iff, Membership.mem, Finset, Imo2004P3.rect, And, LE.le, OfNat.ofNat, Prod.fst, LT.lt, Prod.snd
Proof uses: Iff.intro, Eq, Prod.mk, Exists, Eq.mp, Eq.trans, Finset.image, SProd.sprod, Finset.range, congrArg, funext, congrFun', congr, id, And.intro, Nat.cast_nonneg, cast, Eq.symm, Eq.mpr, Exists.intro and 11 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.card_rect line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Int, Imo2004P3.rect, HMul.hMul
Proof uses: Function.Injective, Prod.mk, Prod.fst, Prod.snd, Prod.ext, And.left, Eq.mp, And, Eq.trans, Prod.mk.injEq, congr, congrArg, And.right, Eq.mpr, Finset.image, SProd.sprod, Finset, Finset.range, id, Imo2004P3.rect.eq_1 and 4 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.lo_eq line 103 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Finset.Nonempty, Eq, Imo2004P3.lo, Prod.mk, Finset.min', Finset.image, Prod.fst, Finset.Nonempty.image, Prod.snd
Proof uses: Option.getD, Finset.min, OfNat.ofNat, Eq.mpr, id, congrArg, WithTop, Eq.symm, Finset.coe_min', Eq.refl, rfl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.min'_of_eq line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Int, Finset.Nonempty, Eq, Finset.min'
Proof uses: Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.lo_translate line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Finset.Nonempty, Eq, Imo2004P3.lo, Finset.image, HAdd.hAdd
Proof uses: Prod.fst, Eq.mpr, Function.comp, id, congrArg, Finset.image_image, Eq.refl, Prod.snd, Monotone, Monotone.add_const, monotone_id, Prod.mk, Finset.min', Finset.Nonempty.image, Imo2004P3.lo_eq, Imo2004P3.min'_of_eq, Finset.Nonempty.of_image, Finset.min'_image, Prod.ext
16 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.hole_translate line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Finset.Nonempty, Eq, Imo2004P3.hole, Finset.image, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, Imo2004P3.lo, Prod.mk, OfNat.ofNat, True, congr, congrArg, congrFun', Imo2004P3.lo_translate, add_right_comm, eq_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.shape_bounds line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.hookShapes, And, LE.le, OfNat.ofNat, Prod.fst, Prod.snd
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.shape_extremes line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.hookShapes, And, Exists, Eq, Prod.fst, OfNat.ofNat, Prod.snd
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.hole_shape line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.hookShapes, Eq, Imo2004P3.hole, Prod.mk, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.hole_not_mem line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.hookShapes, Not, Imo2004P3.hole
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.card_hook line 147 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.hookShapes, Eq, Nat, Finset.card, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.hook_row3 Every hook orientation contains cells two apart in some row line 151 source
Source documentation
Every hook orientation contains cells two apart in some row.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.hookShapes, Ne, Nat, Finset.card, Inter.inter, Finset.image, Prod.fst, Finset.filter, Eq, Prod.snd, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma hook_row3 : ∀ σ ∈ hookShapes,
    ((σ.filter fun c => c.2 = 0).image Prod.fst ∩
      (σ.filter fun c => c.2 = 2).image Prod.fst).card ≠ 0 := by
…
```
Mentions: Imo2004P3.hookShapes
lemma Imo2004P3.hook_col3 Every hook orientation contains cells two apart in some column line 157 source
Source documentation
Every hook orientation contains cells two apart in some column.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.hookShapes, Ne, Nat, Finset.card, Inter.inter, Finset.image, Prod.snd, Finset.filter, Eq, Prod.fst, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma hook_col3 : ∀ σ ∈ hookShapes,
    ((σ.filter fun c => c.1 = 0).image Prod.snd ∩
      (σ.filter fun c => c.1 = 2).image Prod.snd).card ≠ 0 := by
…
```
Mentions: Imo2004P3.hookShapes
lemma Imo2004P3.pair_check The key local fact line 168 source
Source documentation
The key local fact. Suppose two disjoint hooks are such that the hole of the first one is covered by the second one, and moreover the hole of the second hook is either covered by the first hook or can be covered by a third hook disjoint from both (as must happen in any tiling of a rectangle). Then the hole of the second hook is covered by the first, and the union of the two hooks is one of the six tiles. (Checked case by case.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.hookShapes, Finset.image, HSub.hSub, Prod.mk, OfNat.ofNat, Disjoint, HAdd.hAdd, Or, LT.lt, Nat, Finset.card, Finset.biUnion, Finset.filter, Union.union, And, Eq and 2 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma pair_check :
    ∀ σ₁ ∈ hookShapes, ∀ σ₂ ∈ hookShapes,
      ∀ t ∈ (σ₂.image fun c => (1, 1) - c),
        Disjoint σ₁ (σ₂.image (· + t)) →
          ((1, 1) + t ∈ σ₁ ∨
            0 < (hookShapes.biUnion fun σ₃ =>
              (σ₃.image fun c => ((1, 1) + t) - c).filter fun t₃ =>
                Disjoint (σ₃.image (· + t₃)) (σ₁ ∪ (σ₂.image (· + t)))).card) →
          ((1, 1) + t ∈ σ₁) ∧
            0 < (tileShapes.filter fun τ =>
              σ₁ ∪ (σ₂.image (· + t)) =
                τ.image (· + (lo (σ₁ ∪ (σ₂.image (· + t))) - lo τ))).card := by
…
```
Mentions: Imo2004P3.hookShapes, Imo2004P3.lo
lemma Imo2004P3.tileable_empty line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2004P3.Tileable, EmptyCollection.emptyCollection, Finset, Prod, Int
Proof uses: Exists.intro, And, Membership.mem, Imo2004P3.IsHook, Ne, Disjoint, Eq, Finset.biUnion, id, And.intro, of_eq_true, Eq.trans, True, forall_congr, False, implies_congr, Eq.refl, implies_true, Not, eq_self
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.image_add_image line 184 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Eq, Finset.image, HAdd.hAdd
Proof uses: Eq.mpr, Function.comp, id, congrArg, Finset.image_image, Finset.image_congr, Membership.mem, Set, add_assoc
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.image_swap_add line 191 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Eq, Finset.image, Prod.swap, HAdd.hAdd
Proof uses: Eq.mpr, Function.comp, id, congrArg, Finset.image_image, Finset.image_congr, Membership.mem, Set, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.isHook_translate line 198 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Imo2004P3.IsHook, Finset.image, HAdd.hAdd
Proof uses: And, Membership.mem, Imo2004P3.hookShapes, Exists, Eq, Exists.intro, And.intro, Imo2004P3.image_add_image, Eq.symm
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.hookShapes_swap The hook orientations are closed under transposition (which is one of the eight symmetries of the square) line 205 source
Source documentation
The hook orientations are closed under transposition (which is one of the eight symmetries of the square).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.hookShapes, LT.lt, Nat, OfNat.ofNat, Finset.card, Finset.filter, Eq, Finset.image, Prod.swap, HAdd.hAdd, HSub.hSub, Imo2004P3.lo
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma hookShapes_swap : ∀ σ ∈ hookShapes,
    0 < (hookShapes.filter fun σ' =>
      σ.image Prod.swap = σ'.image (· + (lo (σ.image Prod.swap) - lo σ'))).card := by
…
```
Mentions: Imo2004P3.hookShapes, Imo2004P3.lo
lemma Imo2004P3.isHook_swap line 210 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Imo2004P3.IsHook, Finset.image, Prod.swap
Proof uses: And, Membership.mem, Imo2004P3.hookShapes, Exists, Eq, HAdd.hAdd, LT.lt, Nat, OfNat.ofNat, Finset.card, Finset.filter, HSub.hSub, Imo2004P3.lo, Imo2004P3.hookShapes_swap, Finset.Nonempty, Eq.mp, congrArg, propext, Finset.card_pos, Finset.mem_filter and 11 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.biUnion_image_translate line 224 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Eq, Finset.biUnion, Finset.image, HAdd.hAdd, id
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, Iff.mp, Finset.mem_image, Exists.intro, And.intro, rfl, Iff.mpr
19 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.biUnion_image_swap line 236 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Eq, Finset.biUnion, Finset.image, Prod.swap, id
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, Iff.mp, Finset.mem_image, Exists.intro, And.intro, rfl, Iff.mpr
13 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.tileable_translate line 248 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Imo2004P3.Tileable, Finset.image, HAdd.hAdd
Proof uses: And, Membership.mem, Imo2004P3.IsHook, Ne, Disjoint, Eq, Finset.biUnion, id, Exists.intro, And.intro, Exists, Eq.mp, congrArg, propext, Finset.mem_image, Imo2004P3.isHook_translate, Eq.mpr, Eq.refl, Not, Finset.disjoint_left and 4 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.tileable_union line 271 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Disjoint, Imo2004P3.Tileable, Union.union
Proof uses: And, Membership.mem, Imo2004P3.IsHook, Ne, Eq, Finset.biUnion, id, Exists.intro, And.intro, Or, Iff.mp, Finset.mem_union, LE.le, Eq.mpr, congrArg, Finset.subset_biUnion_of_mem, Disjoint.mono, Disjoint.symm, Finset.union_biUnion, Eq.symm and 1 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.rect_zero_left line 292 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Prod, Int, Imo2004P3.rect, OfNat.ofNat, EmptyCollection.emptyCollection
Proof uses: of_eq_true, eq_self
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.rect_zero_right line 294 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Prod, Int, Imo2004P3.rect, OfNat.ofNat, EmptyCollection.emptyCollection
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, SProd.sprod, Finset.range, Finset.image, Prod.mk, Prod.fst, Prod.snd, Finset.product_empty, eq_self
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.rect_add_rows line 296 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Prod, Int, Imo2004P3.rect, HAdd.hAdd, Union.union, Finset.image, Prod.mk, OfNat.ofNat
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, LE.le, Prod.fst, LT.lt, Prod.snd, Or, Exists, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, dite, Or.inl and 13 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.rect_add_rows_disjoint line 314 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Disjoint, Finset, Prod, Int, Imo2004P3.rect, Finset.image, HAdd.hAdd, Prod.mk, OfNat.ofNat
Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Finset.disjoint_left, And, Exists, False, Eq.mp, LE.le, Prod.fst, LT.lt, Prod.snd, And.left, And.right, Imo2004P3.mem_rect
30 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.rect_add_cols line 326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Prod, Int, Imo2004P3.rect, HAdd.hAdd, Union.union, Finset.image, Prod.mk, OfNat.ofNat
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, LE.le, Prod.fst, LT.lt, Prod.snd, Or, Exists, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, dite, Or.inl and 13 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.rect_add_cols_disjoint line 344 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Disjoint, Finset, Prod, Int, Imo2004P3.rect, Finset.image, HAdd.hAdd, Prod.mk, OfNat.ofNat
Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Finset.disjoint_left, And, Exists, False, Eq.mp, LE.le, Prod.fst, LT.lt, Prod.snd, And.right, And.left, Imo2004P3.mem_rect
30 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.tileable_mul_rows line 356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2004P3.Tileable, Imo2004P3.rect, HMul.hMul
Proof uses: Nat.recAux, Eq.mpr, OfNat.ofNat, id, Eq, congrArg, Nat.zero_mul, EmptyCollection.emptyCollection, Finset, Prod, Int, Imo2004P3.rect_zero_left, Imo2004P3.tileable_empty, HAdd.hAdd, Nat.succ, Nat.succ_mul, Union.union, Finset.image, Prod.mk, Imo2004P3.rect_add_rows and 3 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.tileable_mul_cols line 364 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2004P3.Tileable, Imo2004P3.rect, HMul.hMul
Proof uses: Nat.recAux, Eq.mpr, OfNat.ofNat, id, Eq, congrArg, Nat.zero_mul, EmptyCollection.emptyCollection, Finset, Prod, Int, Imo2004P3.rect_zero_right, Imo2004P3.tileable_empty, HAdd.hAdd, Nat.succ, Nat.succ_mul, Union.union, Finset.image, Prod.mk, Imo2004P3.rect_add_cols and 3 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.tileable_mul line 372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2004P3.Tileable, Imo2004P3.rect, HMul.hMul
Proof uses: Imo2004P3.tileable_mul_cols, Imo2004P3.tileable_mul_rows
4 instances, coercions and auxiliary constants left out.
lemma Imo2004P3.rect_transpose line 376 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Prod, Int, Finset.image, Prod.swap, Imo2004P3.rect
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, Exists, And, LE.le, OfNat.ofNat, Prod.fst, LT.lt, Prod.snd, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, Prod.mk, And.intro and 2 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.tileable_swap line 385 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Imo2004P3.Tileable, Finset.image, Prod.swap
Proof uses: And, Membership.mem, Imo2004P3.IsHook, Ne, Disjoint, Eq, Finset.biUnion, id, Exists.intro, And.intro, Exists, Eq.mp, congrArg, propext, Finset.mem_image, Imo2004P3.isHook_swap, Eq.mpr, Eq.refl, Not, Finset.disjoint_left and 4 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.tileable_transpose line 407 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2004P3.Tileable, Imo2004P3.rect
Proof uses: Eq.mpr, Finset.image, Prod, Int, Prod.swap, id, Eq, congrArg, Finset, Eq.symm, Imo2004P3.rect_transpose, Imo2004P3.tileable_swap
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.tileable_3_4 Two hooks tile a 3 × 4 rectangle line 412 source
Source documentation
Two hooks tile a 3 × 4 rectangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2004P3.Tileable, Imo2004P3.rect, OfNat.ofNat, Nat
Proof uses: Imo2004P3.IsHook, Insert.insert, Prod, Int, Finset, Prod.mk, Singleton.singleton, Exists.intro, And, Membership.mem, Imo2004P3.hookShapes, Exists, Eq, Finset.image, HAdd.hAdd, And.intro, of_decide_eq_true, id, Bool, Decidable.decide and 19 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma tileable_3_4 : Tileable (rect 3 4) := by
…
```
Mentions: Imo2004P3.Tileable, Imo2004P3.rect
lemma Imo2004P3.nat_3_4 Every natural number other than 1, 2, 5 is a sum of 3s and 4s line 428 source
Source documentation
Every natural number other than 1, 2, 5 is a sum of 3s and 4s.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, Ne, OfNat.ofNat, Exists, Eq, HAdd.hAdd, HMul.hMul
Proof uses: Or, HMod.hMod, Exists.intro, HDiv.hDiv, HSub.hSub
21 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma nat_3_4 {n : ℕ} (h : n ≠ 1 ∧ n ≠ 2 ∧ n ≠ 5) : ∃ a b, n = 3 * a + 4 * b := by
…
```
Mentions: h
lemma Imo2004P3.tileable_12j A 12 × n rectangle with n ∉ {1, 2, 5} is tileable line 436 source
Source documentation
A 12 × n rectangle with n ∉ {1, 2, 5} is tileable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, Ne, OfNat.ofNat, Imo2004P3.Tileable, Imo2004P3.rect, HMul.hMul
Proof uses: Exists, Eq, HAdd.hAdd, Imo2004P3.nat_3_4, Imo2004P3.tileable_transpose, Imo2004P3.tileable_mul_cols, Imo2004P3.tileable_3_4, Eq.mpr, Union.union, Finset, Prod, Int, Finset.image, Prod.mk, id, congrArg, Imo2004P3.rect_add_cols, Imo2004P3.tileable_union, Imo2004P3.rect_add_cols_disjoint, Imo2004P3.tileable_mul and 4 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma tileable_12j (j : ℕ) {n : ℕ} (h2 : n ≠ 1 ∧ n ≠ 2 ∧ n ≠ 5) :
    Tileable (rect (12 * j) n) := by
…
```
Mentions: Imo2004P3.Tileable, Imo2004P3.rect
lemma Imo2004P3.tileable_of_conditions Sufficiency: every rectangle satisfying the conditions is tileable line 452 source
Source documentation
Sufficiency: every rectangle satisfying the conditions is tileable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, Ne, OfNat.ofNat, Or, Dvd.dvd, Imo2004P3.Tileable, Imo2004P3.rect
Proof uses: dite, Eq, HMul.hMul, Eq.mpr, id, congrArg, mul_comm, Imo2004P3.tileable_transpose, Imo2004P3.tileable_mul, Imo2004P3.tileable_3_4, Eq.symm, Not, Nat.Coprime.dvd_of_dvd_mul_left, of_decide_eq_true, Nat.Coprime, Bool, Decidable.decide, Bool.true, Eq.refl, Exists.intro and 19 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
```
lemma tileable_of_conditions {m n : ℕ}
    (h1 : m ≠ 1 ∧ m ≠ 2 ∧ m ≠ 5) (h2 : n ≠ 1 ∧ n ≠ 2 ∧ n ≠ 5)
    (h3 : 3 ∣ m ∨ 3 ∣ n) (h4 : 4 ∣ m ∨ 4 ∣ n) :
    Tileable (rect m n) := by
…
```
Mentions: Imo2004P3.Tileable, Imo2004P3.rect
lemma Imo2004P3.shape_nonempty line 510 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.hookShapes, Finset.Nonempty
Proof uses: Eq.mpr, LT.lt, Nat, OfNat.ofNat, Finset.card, id, Eq, congrArg, Eq.symm, propext, Finset.card_pos, Imo2004P3.card_hook, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.isHook_nonempty line 515 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Imo2004P3.IsHook, Finset.Nonempty
Proof uses: And, Membership.mem, Imo2004P3.hookShapes, Exists, Eq, Finset.image, HAdd.hAdd, Finset.Nonempty.image, Imo2004P3.shape_nonempty, Eq.symm
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.isHook_card line 519 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Imo2004P3.IsHook, Eq, Nat, Finset.card, OfNat.ofNat
Proof uses: And, Membership.mem, Imo2004P3.hookShapes, Exists, Finset.image, HAdd.hAdd, Eq.mpr, id, congrArg, Finset.card_image_of_injective, add_right_cancel, Imo2004P3.card_hook, Eq.symm
30 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.hole_image line 524 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.hookShapes, Eq, Imo2004P3.hole, Finset.image, HAdd.hAdd, Prod.mk, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Imo2004P3.hole_translate, Imo2004P3.shape_nonempty, Imo2004P3.hole_shape, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.hole_not_mem_of_hook line 528 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Imo2004P3.IsHook, Not, Membership.mem, Imo2004P3.hole
Proof uses: And, Imo2004P3.hookShapes, Exists, Eq, Finset.image, HAdd.hAdd, Eq.mpr, Prod.mk, OfNat.ofNat, id, congrArg, Imo2004P3.hole_image, False, Eq.mp, propext, Finset.mem_image, add_right_cancel, Imo2004P3.hole_not_mem, Imo2004P3.hole_shape, Eq.symm
31 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.hole_mem_rect_of_hook line 540 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Int, Imo2004P3.IsHook, LE.le, Imo2004P3.rect, Membership.mem, Imo2004P3.hole
Proof uses: And, Imo2004P3.hookShapes, Exists, Eq, Finset.image, HAdd.hAdd, Eq.mpr, Prod.mk, OfNat.ofNat, id, congrArg, Imo2004P3.hole_image, Prod.fst, LT.lt, Prod.snd, propext, Imo2004P3.mem_rect, Imo2004P3.shape_extremes, Iff.mpr, Finset.mem_image and 5 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.pair_general Documented declaration: pair_general line 560 source
Source documentation
The pairing lemma in its general form: in any tiling, the partner of a hook (the hook covering its hole) has its hole covered by the first hook, and the two hooks together form a tile.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Imo2004P3.IsHook, Disjoint, Membership.mem, Imo2004P3.hole, Or, Exists, And, Union.union, Imo2004P3.IsTile
Proof uses: Imo2004P3.hookShapes, Eq, Finset.image, HAdd.hAdd, HSub.hSub, Prod.mk, OfNat.ofNat, Eq.mp, congrArg, propext, Finset.mem_image, Imo2004P3.hole_image, Iff.mpr, Exists.intro, And.intro, Prod.fst, Prod.snd, Prod.ext, id, Eq.mpr and 28 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 111 steps
Open to load the checked before-and-after goal states.
```
lemma pair_general {H₁ H₂ : Finset (ℤ × ℤ)} (h1 : IsHook H₁) (h2 : IsHook H₂)
    (hd : Disjoint H₁ H₂) (hh : hole H₁ ∈ H₂)
    (h3 : hole H₂ ∈ H₁ ∨ ∃ H₃ : Finset (ℤ × ℤ), IsHook H₃ ∧ Disjoint H₃ (H₁ ∪ H₂) ∧
      hole H₂ ∈ H₃) :
    hole H₂ ∈ H₁ ∧ IsTile (H₁ ∪ H₂) := by
…
```
Mentions: Imo2004P3.IsHook, Imo2004P3.hole, Imo2004P3.IsTile
lemma Imo2004P3.tile_decomposition The main structural fact: any hook-tiling of a rectangle refines to a tiling by the six two-hook tiles line 658 source
Source documentation
The main structural fact: any hook-tiling of a rectangle refines to a tiling by the six two-hook tiles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2004P3.Tileable, Imo2004P3.rect, Exists, Finset, Prod, Int, And, Membership.mem, Imo2004P3.IsTile, Eq, Finset.card, OfNat.ofNat, Ne, Disjoint, Finset.biUnion, id
Proof uses: Imo2004P3.IsHook, Eq.mp, congrArg, propext, Finset.mem_biUnion, Decidable.byContradiction, Not, Iff.mp, Finset.disjoint_left, Imo2004P3.hole, Imo2004P3.hole_mem_rect_of_hook, Eq.mpr, LE.le, Finset.subset_biUnion_of_mem, dite, Classical.choose, rfl, Eq.mpr_prop, True, eq_true and 33 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 118 steps
Open to load the checked before-and-after goal states.
```
lemma tile_decomposition {m n : ℕ} (h : Tileable (rect m n)) :
    ∃ Tiles : Finset (Finset (ℤ × ℤ)),
      (∀ T ∈ Tiles, IsTile T ∧ T.card = 12) ∧
      (∀ T₁ ∈ Tiles, ∀ T₂ ∈ Tiles, T₁ ≠ T₂ → Disjoint T₁ T₂) ∧
      rect m n = Tiles.biUnion id := by
…
```
Mentions: h, Imo2004P3.Tileable, Imo2004P3.rect, Imo2004P3.IsTile
lemma Imo2004P3.twelve_dvd_of_tileable line 762 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2004P3.Tileable, Imo2004P3.rect, Dvd.dvd, OfNat.ofNat, HMul.hMul
Proof uses: Finset, Prod, Int, And, Membership.mem, Imo2004P3.IsTile, Eq, Finset.card, Ne, Disjoint, Finset.biUnion, id, Exists, Imo2004P3.tile_decomposition, Finset.sum, Eq.mpr, congrArg, Finset.card_biUnion, Exists.intro, Eq.mp and 28 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.three_dvd_of_tileable line 771 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2004P3.Tileable, Imo2004P3.rect, Or, Dvd.dvd, OfNat.ofNat
Proof uses: HMul.hMul, dvd_trans, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Imo2004P3.twelve_dvd_of_tileable, Iff.mp, Nat.Prime.dvd_mul, Nat.Prime
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.tile_parities On every tile, exactly one of the two parity counts (cells in columns divisible by four, cells in rows divisible by four) is odd line 777 source
Source documentation
On every tile, exactly one of the two parity counts (cells in columns divisible by four, cells in rows divisible by four) is odd.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.tileShapes, Eq, Nat, HAdd.hAdd, HMod.hMod, Finset.card, Finset.filter, Dvd.dvd, OfNat.ofNat, Prod.snd, Finset.image, Prod.fst
Proof uses: Or, Eq.mpr, id, congrArg, Finset.filter_image, DecidableEq, Eq.rec, Eq.refl, Finset.filter_congr, rfl, Iff, Iff.intro, Finset.card_image_of_injective, add_right_cancel, List, List.Mem, List.insert, Insert.insert, Prod.mk, Singleton.singleton and 14 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma tile_parities : ∀ τ ∈ tileShapes, ∀ t : ℤ × ℤ,
    ((τ.image (· + t)).filter fun c => 4 ∣ c.2).card % 2 +
    ((τ.image (· + t)).filter fun c => 4 ∣ c.1).card % 2 = 1 := by
…
```
Mentions: Imo2004P3.tileShapes
lemma Imo2004P3.rect_filter_snd_card line 808 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Int, Finset.filter, Dvd.dvd, OfNat.ofNat, Prod.snd, Imo2004P3.rect, HMul.hMul, Finset.range
Proof uses: Function.Injective, Prod.mk, Prod.fst, Prod.ext, And.left, Eq.mp, And, Eq.trans, Prod.mk.injEq, congr, congrArg, And.right, Finset, Finset.image, SProd.sprod, Finset.ext, Eq.mpr, Iff, Membership.mem, Exists and 12 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.rect_filter_fst_card line 827 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Int, Finset.filter, Dvd.dvd, OfNat.ofNat, Prod.fst, Imo2004P3.rect, HMul.hMul, Finset.range
Proof uses: Function.Injective, Prod.mk, Prod.snd, Prod.ext, And.left, Eq.mp, And, Eq.trans, Prod.mk.injEq, congr, congrArg, And.right, Finset, Finset.image, SProd.sprod, Finset.ext, Eq.mpr, Iff, Membership.mem, Exists and 13 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.mod4_eq_two_of If 4 ∣ a * b but 4 ∤ a and 4 ∤ b, then a ≡ b ≡ 2 (mod 4) line 848 source
Source documentation
If 4 ∣ a * b but 4 ∤ a and 4 ∤ b, then a ≡ b ≡ 2 (mod 4).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Dvd.dvd, OfNat.ofNat, HMul.hMul, Not, And, Eq, HMod.hMod
Proof uses: dvd_trans, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Decidable.byContradiction, Or, Iff.mp, Nat.Prime.dvd_mul, Nat.Prime, absurd, False, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf and 23 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 85 steps
Open to load the checked before-and-after goal states.
```
lemma mod4_eq_two_of {a b : ℕ} (h4ab : 4 ∣ a * b) (h4a : ¬ 4 ∣ a) (h4b : ¬ 4 ∣ b) :
    a % 4 = 2 ∧ b % 4 = 2 := by
…
```
lemma Imo2004P3.card_biUnion' Necessity of the divisibility condition on 4 line 911 source
Source documentation
Necessity of the divisibility condition on 4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Ne, Disjoint, Eq, Nat, Finset.card, Finset.biUnion, Finset.sum
Proof uses: Finset.card_biUnion
13 instances, coercions and auxiliary constants left out.
```
lemma card_biUnion' {s : Finset (Finset (ℤ × ℤ))} {t : Finset (ℤ × ℤ) → Finset (ℤ × ℤ)}
    (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → Disjoint (t x) (t y)) :
    (s.biUnion t).card = ∑ x ∈ s, (t x).card :=
…
```
Mentions: h
lemma Imo2004P3.four_dvd_of_tileable line 916 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2004P3.Tileable, Imo2004P3.rect, Or, Dvd.dvd, OfNat.ofNat
Proof uses: Finset, Prod, Int, And, Membership.mem, Imo2004P3.IsTile, Eq, Finset.card, Ne, Disjoint, Finset.biUnion, id, Exists, Imo2004P3.tile_decomposition, Decidable.byContradiction, Not, False, Iff.mp, not_or, HMul.hMul and 73 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 74 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.not_tileable_of_n_le_two A rectangle with a side of length at most 2 cannot be tiled (a hook spans three consecutive rows and three consecutive columns) line 1000 source
Source documentation
A rectangle with a side of length at most 2 cannot be tiled (a hook spans three consecutive rows and three consecutive columns).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Not, Imo2004P3.Tileable, Imo2004P3.rect
Proof uses: Finset, Prod, Int, And, Membership.mem, Imo2004P3.IsHook, Ne, Disjoint, Eq, Finset.biUnion, id, False, Finset.Nonempty, Exists.intro, Prod.mk, Eq.mpr, Prod.fst, Prod.snd, congrArg, propext and 34 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
lemma not_tileable_of_n_le_two {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (hnle : n ≤ 2) :
    ¬ Tileable (rect m n) := by
…
```
Mentions: Imo2004P3.Tileable, Imo2004P3.rect
def Imo2004P3.cornerCell The second cell used in the corner propagation argument for the 5 × n case: it is the cell just next to a tile placed in the corner which cannot be covered by any other tile line 1035 source
Source documentation
The second cell used in the corner propagation argument for the 5 × n case: it is the cell just next to a tile placed in the corner which cannot be covered by any other tile.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: ite, Not, Membership.mem, Prod.mk, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
def cornerCell (τ₀ : Finset (ℤ × ℤ)) : ℤ × ℤ :=
…
```
lemma Imo2004P3.cornerCell_not_mem line 1039 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.tileShapes, Prod.mk, OfNat.ofNat, Not, Imo2004P3.cornerCell
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.cornerCell_snd line 1042 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.tileShapes, LE.le, Prod.snd, Imo2004P3.cornerCell, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.cornerCell_val line 1045 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.tileShapes, Insert.insert, Prod.mk, OfNat.ofNat, Singleton.singleton, Imo2004P3.cornerCell
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.corner_check The corner propagation check: no tile covering cornerCell τ₀ within the bounds of a five-row strip is disjoint from the corner tile τ₀ line 1051 source
Source documentation
The corner propagation check: no tile covering cornerCell τ₀ within the bounds of a five-row strip is disjoint from the corner tile τ₀.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.tileShapes, Prod.mk, OfNat.ofNat, Finset.image, HSub.hSub, Imo2004P3.cornerCell, HAdd.hAdd, And, LE.le, Prod.fst, LT.lt, Prod.snd, Not, Disjoint
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma corner_check :
    ∀ τ₀ ∈ tileShapes, (0, 0) ∈ τ₀ →
      ∀ τ' ∈ tileShapes, ∀ v ∈ (τ'.image fun c => cornerCell τ₀ - c),
        (∀ cell ∈ τ'.image (· + v), 0 ≤ cell.1 ∧ cell.1 < 5 ∧ 0 ≤ cell.2 ∧ cell.2 < 6) →
        ¬ Disjoint (τ'.image (· + v)) τ₀ := by
…
```
Mentions: Imo2004P3.tileShapes, Imo2004P3.cornerCell
lemma Imo2004P3.tile_bounds line 1058 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.tileShapes, And, LE.le, OfNat.ofNat, Prod.fst, Prod.snd
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.tile_min line 1062 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, Imo2004P3.tileShapes, And, Exists, Eq, Prod.fst, OfNat.ofNat, Prod.snd
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2004P3.not_tileable_5 A 5 × n rectangle cannot be tiled line 1066 source
Source documentation
A 5 × n rectangle cannot be tiled.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Not, Imo2004P3.Tileable, Imo2004P3.rect
Proof uses: Dvd.dvd, Nat.Coprime.dvd_of_dvd_mul_left, of_decide_eq_true, Nat.Coprime, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Imo2004P3.twelve_dvd_of_tileable, LE.le, Nat.le_of_dvd, Finset, Prod, Int, And, Membership.mem, Imo2004P3.IsTile, Finset.card and 52 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 91 steps
Open to load the checked before-and-after goal states.
```
lemma not_tileable_5 (n : ℕ) (hn : 0 < n) : ¬ Tileable (rect 5 n) := by
…
```
Mentions: Imo2004P3.Tileable, Imo2004P3.rect
def Imo2004P3.GoodRect The predicate characterising the rectangles that can be tiled by hooks line 1151 source
Source documentation
The predicate characterising the rectangles that can be tiled by hooks.

no axioms what this means
Statement uses: Nat
Proof uses: And, Ne, OfNat.ofNat, Or, Dvd.dvd
2 instances, coercions and auxiliary constants left out.
```
def GoodRect (m n : ℕ) : Prop :=
…
```
determine Imo2004P3.answer line 1156 source
no axioms what this means
Statement uses: Set, Prod, Nat
Proof uses: Set.ofPred, Imo2004P3.GoodRect, Prod.fst, Prod.snd
problem Imo2004P3.imo2004_p3 line 1159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, Imo2004P3.Tileable, Imo2004P3.rect, Membership.mem, Prod, Set, Imo2004P3.answer, Prod.mk
Proof uses: Iff.intro, Or, Dvd.dvd, Imo2004P3.three_dvd_of_tileable, Imo2004P3.four_dvd_of_tileable, id, And.intro, Ne, And, Eq, Imo2004P3.not_tileable_of_n_le_two, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Mathlib.Meta.NormNum.isNat_le_true, Bool.true, Imo2004P3.tileable_transpose, Eq.mp and 6 more
14 instances, coercions and auxiliary constants left out.

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