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

USA Mathematical Olympiad 2002, Problem 6

I have an n×n sheet of stamps, from which I've been asked to tear out blocks of three adjacent stamps in a single row or column. (I can only tear along the perforations separating adjacent stamps, and each block must come out of the sheet in one piece.) Let b(n) be the smallest number of blocks I can tear out and make it impossible to tear out any more blocks. Prove that there are real constants c and d such that

(1/7)n² - cn ≤ b(n) ≤ (1/5)n² - dn

for all n > 0.

Imports (4)

Imported by 1 file

Compfiles.lean

def Usa2002P6.hblock A horizontal block: three adjacent stamps in a single row line 36 source
Source documentation
A horizontal block: three adjacent stamps in a single row.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod
Proof uses: Insert.insert, Prod.mk, HAdd.hAdd, OfNat.ofNat, Singleton.singleton
7 instances, coercions and auxiliary constants left out.
```
def hblock (i j : ℕ) : Finset (ℕ × ℕ) := {(i, j), (i, j + 1), (i, j + 2)}
```
def Usa2002P6.vblock A vertical block: three adjacent stamps in a single column line 39 source
Source documentation
A vertical block: three adjacent stamps in a single column.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod
Proof uses: Insert.insert, Prod.mk, HAdd.hAdd, OfNat.ofNat, Singleton.singleton
7 instances, coercions and auxiliary constants left out.
```
def vblock (i j : ℕ) : Finset (ℕ × ℕ) := {(i, j), (i + 1, j), (i + 2, j)}
```
def Usa2002P6.IsBlock A block that can be torn out of the n×n sheet line 42 source
Source documentation
A block that can be torn out of the n×n sheet.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod
Proof uses: Or, Exists, And, LT.lt, HAdd.hAdd, OfNat.ofNat, Eq, Usa2002P6.hblock, Usa2002P6.vblock
4 instances, coercions and auxiliary constants left out.
```
def IsBlock (n : ℕ) (s : Finset (ℕ × ℕ)) : Prop :=
…
```
def Usa2002P6.IsMaximalTearing A tearing-out of pairwise disjoint blocks from the n×n sheet which makes it impossible to tear out any more blocks line 48 source
Source documentation
A tearing-out of pairwise disjoint blocks from the n×n sheet which makes it impossible to tear out any more blocks.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod
Proof uses: And, Membership.mem, Usa2002P6.IsBlock, Ne, Disjoint, Exists, Not
4 instances, coercions and auxiliary constants left out.
```
def IsMaximalTearing (n : ℕ) (T : Finset (Finset (ℕ × ℕ))) : Prop :=
…
```
def Usa2002P6.trivialTearing A wasteful maximal tearing: fill the sheet with vertical blocks, column by column, and fill the leftover bottom rows with horizontal blocks line 56 source
Source documentation
A wasteful maximal tearing: fill the sheet with vertical blocks, column by column, and fill the leftover bottom rows with horizontal blocks. Used to show that a maximal tearing always exists (and for the upper bound at small n).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod
Proof uses: Union.union, Finset.image, Usa2002P6.vblock, HMul.hMul, OfNat.ofNat, Prod.fst, Prod.snd, SProd.sprod, Finset.range, HDiv.hDiv, Usa2002P6.hblock, HAdd.hAdd, HMod.hMod
14 instances, coercions and auxiliary constants left out.
```
def trivialTearing (n : ℕ) : Finset (Finset (ℕ × ℕ)) :=
…
```
def Usa2002P6.phase The phase of row i in the efficient tearing pattern: in row i, the torn blocks start at columns congruent to phase i modulo 5 line 63 source
Source documentation
The phase of row i in the efficient tearing pattern: in row i, the torn blocks start at columns congruent to phase i modulo 5.

no axioms what this means
Statement uses: Nat
Proof uses: HMod.hMod, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
def phase (i : ℕ) : ℕ := i % 5
```
def Usa2002P6.patRowTearing The blocks torn out of row i in the efficient tearing pattern line 66 source
Source documentation
The blocks torn out of row i in the efficient tearing pattern.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod
Proof uses: Union.union, Finset.image, Usa2002P6.hblock, HAdd.hAdd, Usa2002P6.phase, HMul.hMul, OfNat.ofNat, Finset.filter, LT.lt, Finset.range, HDiv.hDiv, ite, LE.le, Singleton.singleton, EmptyCollection.emptyCollection, HMod.hMod, HSub.hSub
21 instances, coercions and auxiliary constants left out.
```
def patRowTearing (n i : ℕ) : Finset (Finset (ℕ × ℕ)) :=
…
```
def Usa2002P6.patTearing The efficient maximal tearing, with asymptotic density n²/5 line 73 source
Source documentation
The efficient maximal tearing, with asymptotic density n²/5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod
Proof uses: Finset.biUnion, Finset.range, Usa2002P6.patRowTearing
3 instances, coercions and auxiliary constants left out.
```
def patTearing (n : ℕ) : Finset (Finset (ℕ × ℕ)) :=
…
```
def Usa2002P6.cov cov n i j means that cell (i, j) is torn out by the efficient pattern line 77 source
Source documentation
cov n i j means that cell (i, j) is torn out by the efficient pattern.

no axioms what this means
Statement uses: Nat
Proof uses: Or, And, LE.le, OfNat.ofNat, Usa2002P6.phase, HMod.hMod, HSub.hSub, LT.lt, HAdd.hAdd
9 instances, coercions and auxiliary constants left out.
```
def cov (n i j : ℕ) : Prop :=
…
```
theorem Usa2002P6.mem_hblock line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Membership.mem, Prod, Finset, Usa2002P6.hblock, Prod.mk, And, Eq, LE.le, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, Or, id, congrFun', congrArg, Eq.trans, Insert.insert, Singleton.singleton, congr, Prod.mk.injEq
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.mem_vblock line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Membership.mem, Prod, Finset, Usa2002P6.vblock, Prod.mk, And, LE.le, HAdd.hAdd, OfNat.ofNat, Eq
Proof uses: Eq.mpr, Or, id, congrFun', congrArg, Eq.trans, Insert.insert, Singleton.singleton, congr, Prod.mk.injEq
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.trivialTearing_isMaximalTearing line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2002P6.IsMaximalTearing, Usa2002P6.trivialTearing
Proof uses: And.intro, Finset, Prod, Membership.mem, Usa2002P6.IsBlock, And, Ne, Disjoint, Exists, Not, LT.lt, Prod.fst, HDiv.hDiv, OfNat.ofNat, Prod.snd, Eq, Usa2002P6.vblock, HMul.hMul, HMod.hMod, Usa2002P6.hblock and 45 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 86 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.trivialTearing_card_le line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Finset.card, Finset, Prod, Usa2002P6.trivialTearing, HAdd.hAdd, HMul.hMul, HDiv.hDiv, OfNat.ofNat, HMod.hMod
Proof uses: LE.le.trans, Union.union, Finset.image, Usa2002P6.vblock, Prod.fst, Prod.snd, SProd.sprod, Finset.range, Usa2002P6.hblock, Finset.card_union_le, add_le_add, Finset.card_image_le, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.card_product, congr, Finset.card_range
32 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.exists_maximalTearing line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Finset, Prod, And, Usa2002P6.IsMaximalTearing, Eq, Finset.card
Proof uses: Exists.intro, Usa2002P6.trivialTearing, And.intro, Usa2002P6.trivialTearing_isMaximalTearing, rfl
def Usa2002P6.b Documented declaration: b line 173 source
Source documentation
b n: the smallest number of blocks one can tear out of an n×n sheet of stamps (tearing out whole blocks of three adjacent stamps in a single row or column) making it impossible to tear out any more blocks.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Nat.find, Exists, Finset, Prod, And, Usa2002P6.IsMaximalTearing, Eq, Finset.card, Classical.propDecidable, Usa2002P6.exists_maximalTearing
```
noncomputable def b (n : ℕ) : ℕ :=
…
```
theorem Usa2002P6.b_le line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Usa2002P6.IsMaximalTearing, LE.le, Usa2002P6.b, Finset.card
Proof uses: Nat.find_le, Exists, And, Eq, Classical.propDecidable, Usa2002P6.exists_maximalTearing, Exists.intro, And.intro, rfl
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.b_spec line 183 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Finset, Prod, And, Usa2002P6.IsMaximalTearing, Eq, Finset.card, Usa2002P6.b
Proof uses: Nat.find_spec, Classical.propDecidable, Usa2002P6.exists_maximalTearing

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Usa2002P6.segsH The set of all horizontal 1 × 3 block positions on the n × n sheet line 188 source
Source documentation
The set of all horizontal 1 × 3 block positions on the n × n sheet.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod
Proof uses: Finset.image, Usa2002P6.hblock, Prod.fst, Prod.snd, SProd.sprod, Finset.range, HSub.hSub, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
def segsH (n : ℕ) : Finset (Finset (ℕ × ℕ)) :=
…
```
def Usa2002P6.segsV The set of all vertical 3 × 1 block positions on the n × n sheet line 192 source
Source documentation
The set of all vertical 3 × 1 block positions on the n × n sheet.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod
Proof uses: Finset.image, Usa2002P6.vblock, Prod.fst, Prod.snd, SProd.sprod, Finset.range, HSub.hSub, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
def segsV (n : ℕ) : Finset (Finset (ℕ × ℕ)) :=
…
```
theorem Usa2002P6.lower_hblock_inj line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Prod, Usa2002P6.hblock, And
Proof uses: Membership.mem, Prod.mk, Iff.mpr, LE.le, HAdd.hAdd, OfNat.ofNat, Usa2002P6.mem_hblock, And.intro, rfl, le_rfl, Eq.mp, congrArg, propext, Eq.symm
9 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.lower_vblock_inj line 204 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Prod, Usa2002P6.vblock, And
Proof uses: Membership.mem, Prod.mk, Iff.mpr, LE.le, HAdd.hAdd, OfNat.ofNat, Usa2002P6.mem_vblock, And.intro, le_rfl, rfl, Eq.mp, congrArg, propext, Eq.symm
9 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.lower_hblock_ne_vblock line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, Finset, Prod, Usa2002P6.hblock, Usa2002P6.vblock
Proof uses: Eq, Membership.mem, Prod.mk, Iff.mpr, And, LE.le, HAdd.hAdd, OfNat.ofNat, Usa2002P6.mem_vblock, And.intro, le_rfl, rfl, Eq.mp, congrArg, propext, Usa2002P6.mem_hblock, Eq.symm
11 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.lower_card_segsH line 221 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Finset, Prod, Usa2002P6.segsH, HMul.hMul, HSub.hSub, OfNat.ofNat
Proof uses: Eq.mpr, Finset.image, Usa2002P6.hblock, Prod.fst, Prod.snd, SProd.sprod, Finset.range, id, congrArg, Usa2002P6.segsH.eq_1, Finset.card_image_of_injOn, Membership.mem, Set, And, Usa2002P6.lower_hblock_inj, Iff.mpr, Prod.ext_iff, And.intro, Finset.card_product, Finset.card_range and 1 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.lower_card_segsV line 228 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Finset, Prod, Usa2002P6.segsV, HMul.hMul, HSub.hSub, OfNat.ofNat
Proof uses: Eq.mpr, Finset.image, Usa2002P6.vblock, Prod.fst, Prod.snd, SProd.sprod, Finset.range, id, congrArg, Usa2002P6.segsV.eq_1, Finset.card_image_of_injOn, Membership.mem, Set, And, Usa2002P6.lower_vblock_inj, Iff.mpr, Prod.ext_iff, And.intro, Finset.card_product, Finset.card_range and 2 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.lower_disjoint_segs line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Disjoint, Finset, Prod, Usa2002P6.segsH, Usa2002P6.segsV
Proof uses: Eq.mpr, Membership.mem, Not, id, Eq, congrArg, propext, Finset.disjoint_left, And, SProd.sprod, Finset.range, HSub.hSub, OfNat.ofNat, Usa2002P6.hblock, Prod.fst, Prod.snd, Exists, False, Eq.mp, Finset.image and 6 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.lower_card_segs line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Finset, Prod, Union.union, Usa2002P6.segsH, Usa2002P6.segsV, HMul.hMul, OfNat.ofNat, HSub.hSub
Proof uses: Eq.mpr, HAdd.hAdd, id, congrArg, Finset.card_union_of_disjoint, Usa2002P6.lower_disjoint_segs, Usa2002P6.lower_card_segsH, Usa2002P6.lower_card_segsV, two_mul, Eq.refl
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.lower_isBlock_of_mem_segs line 248 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Membership.mem, Union.union, Usa2002P6.segsH, Usa2002P6.segsV, Usa2002P6.IsBlock
Proof uses: Or, Eq.mp, congrArg, propext, Finset.mem_union, And, SProd.sprod, Finset.range, HSub.hSub, OfNat.ofNat, Eq, Usa2002P6.hblock, Prod.fst, Prod.snd, Exists, Finset.image, Finset.mem_image, Usa2002P6.segsH.eq_1, Or.inl, LT.lt and 11 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.lower_card_filter_le_fourteen Every block meets at most 14 of the possible block positions line 262 source
Source documentation
Every block meets at most 14 of the possible block positions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Usa2002P6.IsBlock, LE.le, Finset.card, Finset.filter, Not, Disjoint, Union.union, Usa2002P6.segsH, Usa2002P6.segsV, OfNat.ofNat
Proof uses: Exists, And, LT.lt, HAdd.hAdd, Eq, Usa2002P6.hblock, Usa2002P6.vblock, Eq.mpr, id, congrArg, Finset.filter_union, Finset.image, Finset.Icc, HSub.hSub, Membership.mem, Eq.mp, propext, Finset.mem_filter, SProd.sprod, Finset.range and 36 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 104 steps
Open to load the checked before-and-after goal states.
```
theorem lower_card_filter_le_fourteen {n : ℕ} {s : Finset (ℕ × ℕ)} (hs : IsBlock n s) :
    ((segsH n ∪ segsV n).filter fun u => ¬ Disjoint u s).card ≤ 14 := by
…
```
Mentions: Usa2002P6.IsBlock, Usa2002P6.segsH, Usa2002P6.segsV
theorem Usa2002P6.counting_lower_bound The lower bound b(n) ≥ n(n - 2)/7: double-counting pairs of a possible block position and a torn-out block meeting it line 373 source
Source documentation
The lower bound b(n) ≥ n(n - 2)/7: double-counting pairs of a possible block position and a torn-out block meeting it. Every one of the 2n(n - 2) positions must be met by the tearing, and every torn-out block meets at most 14 positions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Usa2002P6.IsMaximalTearing, LE.le, HMul.hMul, OfNat.ofNat, HSub.hSub, Finset.card
Proof uses: Membership.mem, Usa2002P6.IsBlock, And, Ne, Disjoint, Exists, Not, Union.union, Usa2002P6.segsH, Usa2002P6.segsV, Finset.filter, Prod.fst, Prod.snd, SProd.sprod, Finset.image, Usa2002P6.lower_isBlock_of_mem_segs, Eq.mpr, Eq, id, congrArg and 31 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
theorem counting_lower_bound {n : ℕ} {T : Finset (Finset (ℕ × ℕ))}
    (hT : IsMaximalTearing n T) : 2 * (n * (n - 2)) ≤ 14 * T.card := by
…
```
Mentions: Usa2002P6.IsMaximalTearing
theorem Usa2002P6.mem_patRowTearing Membership in a row of the efficient tearing pattern, in a usable form line 421 source
Source documentation
Membership in a row of the efficient tearing pattern, in a usable form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Membership.mem, Usa2002P6.patRowTearing, Or, Exists, And, LT.lt, HAdd.hAdd, HDiv.hDiv, OfNat.ofNat, Usa2002P6.phase, HMul.hMul, Eq, Usa2002P6.hblock, LE.le, HMod.hMod, HSub.hSub
Proof uses: ite, Singleton.singleton, EmptyCollection.emptyCollection, Eq.mp, Eq.trans, Union.union, Finset.image, Finset.filter, Finset.range, congrFun', congrArg, funext, Or.inl, Exists.intro, And.intro, rfl, dite, Or.inr, Iff.mp, Finset.mem_singleton and 5 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
theorem mem_patRowTearing {n i : ℕ} {s : Finset (ℕ × ℕ)} (hs : s ∈ patRowTearing n i) :
    (∃ k, k < n / 5 + 1 ∧ phase i + 5 * k + 2 < n ∧ s = hblock i (phase i + 5 * k)) ∨
      (3 ≤ phase i ∧ s = hblock i 0) ∨
        (3 ≤ (n + 2 - phase i) % 5 ∧ s = hblock i (n - 3)) := by
…
```
Mentions: Usa2002P6.patRowTearing, Usa2002P6.phase, Usa2002P6.hblock
theorem Usa2002P6.fst_eq_of_mem_patRowTearing Every block of row i of the pattern lies entirely within row i line 441 source
Source documentation
Every block of row i of the pattern lies entirely within row i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Membership.mem, Usa2002P6.patRowTearing, Prod.mk, Eq
Proof uses: Exists, And, LT.lt, HAdd.hAdd, HDiv.hDiv, OfNat.ofNat, Usa2002P6.phase, HMul.hMul, Usa2002P6.hblock, Or, LE.le, HMod.hMod, HSub.hSub, Usa2002P6.mem_patRowTearing, Eq.mp, congrArg, propext, Usa2002P6.mem_hblock, Eq.symm
24 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem fst_eq_of_mem_patRowTearing {n i a b : ℕ} {s : Finset (ℕ × ℕ)}
    (hs : s ∈ patRowTearing n i) (hx : (a, b) ∈ s) : a = i := by
…
```
Mentions: Usa2002P6.b, Usa2002P6.patRowTearing
theorem Usa2002P6.patTearing_isBlock line 446 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Finset, Prod, Membership.mem, Usa2002P6.patTearing, Usa2002P6.IsBlock
Proof uses: And, Finset.range, Usa2002P6.patRowTearing, Exists, Eq.mp, Finset.biUnion, congrArg, propext, Finset.mem_biUnion, Usa2002P6.patTearing.eq_1, LT.lt, HAdd.hAdd, HDiv.hDiv, Usa2002P6.phase, HMul.hMul, Eq, Usa2002P6.hblock, Or, HMod.hMod, HSub.hSub and 8 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.patTearing_disjoint line 456 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Finset, Prod, Membership.mem, Usa2002P6.patTearing, Ne, Disjoint
Proof uses: And, Finset.range, Usa2002P6.patRowTearing, Exists, Eq.mp, Finset.biUnion, congrArg, propext, Finset.mem_biUnion, Usa2002P6.patTearing.eq_1, Eq.mpr, Not, id, Eq, Finset.disjoint_left, False, Prod.mk, Usa2002P6.fst_eq_of_mem_patRowTearing, LT.lt, HAdd.hAdd and 12 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.cov_covered Every cell satisfying cov is torn out by the pattern line 492 source
Source documentation
Every cell satisfying cov is torn out by the pattern.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Usa2002P6.cov, Exists, Finset, Prod, And, Membership.mem, Usa2002P6.patRowTearing, Prod.mk
Proof uses: Usa2002P6.phase, Or, HMod.hMod, HSub.hSub, HAdd.hAdd, Exists.intro, Usa2002P6.hblock, And.intro, Iff.mpr, Union.union, Finset.image, HMul.hMul, Finset.filter, Finset.range, HDiv.hDiv, ite, Singleton.singleton, EmptyCollection.emptyCollection, Finset.mem_union, Or.inl and 13 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
theorem cov_covered {n i j : ℕ} (hn : 6 ≤ n) (_hi : i < n) (hj : j < n) (h : cov n i j) :
    ∃ s ∈ patRowTearing n i, (i, j) ∈ s := by
…
```
Mentions: h, Usa2002P6.cov, Usa2002P6.patRowTearing
theorem Usa2002P6.row_cov Every three consecutive cells of a row of the sheet contain a torn-out cell line 513 source
Source documentation
Every three consecutive cells of a row of the sheet contain a torn-out cell.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HAdd.hAdd, Or, Usa2002P6.cov
Proof uses: id
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem row_cov {n i j : ℕ} (hn : 6 ≤ n) (hi : i < n) (hj : j + 2 < n) :
    cov n i j ∨ cov n i (j + 1) ∨ cov n i (j + 2) := by
…
```
Mentions: Usa2002P6.cov
theorem Usa2002P6.col_cov Every three consecutive cells of a column of the sheet contain a torn-out cell line 520 source
Source documentation
Every three consecutive cells of a column of the sheet contain a torn-out cell.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HAdd.hAdd, Or, Usa2002P6.cov
Proof uses: id
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem col_cov {n i j : ℕ} (hn : 6 ≤ n) (hi : i + 2 < n) (hj : j < n) :
    cov n i j ∨ cov n (i + 1) j ∨ cov n (i + 2) j := by
…
```
Mentions: Usa2002P6.cov
theorem Usa2002P6.patTearing_maximal line 525 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Finset, Prod, Usa2002P6.IsBlock, Exists, And, Membership.mem, Usa2002P6.patTearing, Not, Disjoint
Proof uses: LT.lt, HAdd.hAdd, Eq, Usa2002P6.hblock, Usa2002P6.vblock, Usa2002P6.cov, Or, Usa2002P6.row_cov, Usa2002P6.patRowTearing, Prod.mk, Usa2002P6.cov_covered, Exists.intro, And.intro, Iff.mpr, Finset.biUnion, Finset.range, Finset.mem_biUnion, Finset.mem_range, Finset.not_disjoint_iff, of_eq_true and 16 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.patRowTearing_card_le line 551 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Finset.card, Finset, Prod, Usa2002P6.patRowTearing, HAdd.hAdd, HDiv.hDiv, OfNat.ofNat
Proof uses: Finset.image, Usa2002P6.hblock, Usa2002P6.phase, HMul.hMul, Finset.filter, LT.lt, Finset.range, LE.le.trans, Finset.card_image_le, Finset.card_filter_le, Eq.mpr, id, Eq, congrArg, Finset.card_range, le_refl, ite, Singleton.singleton, EmptyCollection.emptyCollection, Decidable and 16 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.patTearing_card_le line 568 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Finset.card, Finset, Prod, Usa2002P6.patTearing, HMul.hMul, HAdd.hAdd, HDiv.hDiv, OfNat.ofNat
Proof uses: LE.le.trans, Finset.biUnion, Finset.range, Usa2002P6.patRowTearing, Finset.sum, Finset.card_biUnion_le, Trans.trans, Eq, Finset.sum_le_sum, Membership.mem, Usa2002P6.patRowTearing_card_le, Eq.mpr, HSMul.hSMul, id, congrArg, Finset.sum_const, Finset.card_range, smul_eq_mul, Eq.refl
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa2002P6.patTearing_isMaximalTearing line 576 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Usa2002P6.IsMaximalTearing, Usa2002P6.patTearing
Proof uses: And.intro, Finset, Prod, Membership.mem, Usa2002P6.IsBlock, And, Ne, Disjoint, Exists, Not, Usa2002P6.patTearing_isBlock, Usa2002P6.patTearing_disjoint, Usa2002P6.patTearing_maximal
8 instances, coercions and auxiliary constants left out.
problem Usa2002P6.usa2002_p6 USAMO 2002, Problem 6 line 587 source
Source documentation
USAMO 2002, Problem 6. There are real constants c and d such that (1/7)n² - cn ≤ b(n) ≤ (1/5)n² - dn for all n > 0. Here we take c = 2/7 and d = -3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Real, Nat, LT.lt, OfNat.ofNat, And, LE.le, HSub.hSub, HDiv.hDiv, HPow.hPow, HMul.hMul, Usa2002P6.b
Proof uses: Exists.intro, Neg.neg, And.intro, Finset, Prod, Usa2002P6.IsMaximalTearing, Eq, Finset.card, Usa2002P6.b_spec, Or, le_or_gt, Nat.cast_nonneg, cast, Eq.symm, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, inferInstance, AddMonoidWithOne and 127 more
153 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
```
problem usa2002_p6 :
    ∃ c d : ℝ, ∀ n : ℕ, 0 < n →
      (n : ℝ) ^ 2 / 7 - c * n ≤ (b n : ℝ) ∧ (b n : ℝ) ≤ (n : ℝ) ^ 2 / 5 - d * n := by
…
```
Mentions: Usa2002P6.b