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

USA Mathematical Olympiad 2007, Problem 4

An animal with n cells is a connected figure consisting of n equal-sized square cells (equivalently, a polyomino with n cells). A dinosaur is an animal with at least 2007 cells. It is said to be primitive if its cells cannot be partitioned into two or more dinosaurs. Find with proof the maximum number of cells in a primitive dinosaur.

Imports (10)

Imported by 1 file

Compfiles.lean

def Usa2007P4.gridAdj Two cells of the integer lattice are adjacent when they share an edge, i.e. their Manhattan distance is 1 line 38 source
Source documentation
Two cells of the integer lattice are adjacent when they share an edge, i.e. their Manhattan distance is 1.

no axioms what this means
Statement uses: Prod, Int
Proof uses: Eq, Nat, HAdd.hAdd, Int.natAbs, HSub.hSub, Prod.fst, Prod.snd, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def gridAdj (a b : ℤ × ℤ) : Prop := (a.1 - b.1).natAbs + (a.2 - b.2).natAbs = 1
```
def Usa2007P4.gridGraph The infinite grid graph on ℤ × ℤ: vertices are cells, edges join edge-adjacent cells line 42 source
Source documentation
The infinite grid graph on ℤ × ℤ: vertices are cells, edges join edge-adjacent cells.

standard axioms: propext what this means
Statement uses: SimpleGraph, Prod, Int
Proof uses: SimpleGraph.mk, Usa2007P4.gridAdj
2 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def gridGraph : SimpleGraph (ℤ × ℤ) where
…
```
structure Usa2007P4.IsAnimal An animal is a nonempty finite set of cells whose induced subgraph of the grid graph is connected line 54 source
Source documentation
An animal is a nonempty finite set of cells whose induced subgraph of the grid graph is connected.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
```
structure IsAnimal (s : Finset (ℤ × ℤ)) : Prop where
…
```
def Usa2007P4.IsDinosaur A dinosaur is an animal with at least 2007 cells line 59 source
Source documentation
A dinosaur is an animal with at least 2007 cells.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: And, Usa2007P4.IsAnimal, LE.le, Nat, OfNat.ofNat, Finset.card
2 instances, coercions and auxiliary constants left out.
```
def IsDinosaur (s : Finset (ℤ × ℤ)) : Prop := IsAnimal s ∧ 2007 ≤ s.card
```
Mentions: Usa2007P4.IsAnimal
def Usa2007P4.IsDinoPartition parts is a partition of the animal d into two or more dinosaurs: at least two pairwise disjoint dinosaurs whose union is d line 63 source
Source documentation
parts is a partition of the animal d into two or more dinosaurs: at least two pairwise disjoint dinosaurs whose union is d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: And, LE.le, Nat, OfNat.ofNat, Finset.card, Membership.mem, Usa2007P4.IsDinosaur, Ne, Disjoint, Eq, Finset.biUnion, id
8 instances, coercions and auxiliary constants left out.
```
def IsDinoPartition (d : Finset (ℤ × ℤ)) (parts : Finset (Finset (ℤ × ℤ))) : Prop :=
…
```
def Usa2007P4.IsPrimitive A dinosaur is primitive if its cells cannot be partitioned into two or more dinosaurs line 71 source
Source documentation
A dinosaur is primitive if its cells cannot be partitioned into two or more dinosaurs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: And, Usa2007P4.IsDinosaur, Not, Exists, Usa2007P4.IsDinoPartition
```
def IsPrimitive (d : Finset (ℤ × ℤ)) : Prop :=
…
```
lemma Usa2007P4.gridAdj_iff line 78 source
no axioms what this means
Statement uses: Prod, Int, Iff, Usa2007P4.gridAdj, Eq, Nat, HAdd.hAdd, Int.natAbs, HSub.hSub, Prod.fst, Prod.snd, OfNat.ofNat
Proof uses: Iff.rfl
5 instances, coercions and auxiliary constants left out.
lemma Usa2007P4.gridAdj_of_gridAdj line 81 source
standard axioms: propext what this means
Statement uses: Prod, Int, Usa2007P4.gridAdj
Proof uses: SimpleGraph.adj_symm, Usa2007P4.gridGraph
lemma Usa2007P4.ne_of_gridAdj line 84 source
standard axioms: propext what this means
Statement uses: Prod, Int, Usa2007P4.gridAdj, Ne
Proof uses: SimpleGraph.ne_of_adj, Usa2007P4.gridGraph
lemma Usa2007P4.gridAdj_cases A cell adjacent to a is one of its four neighbours line 87 source
Source documentation
A cell adjacent to a is one of its four neighbours.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Usa2007P4.gridAdj, Or, And, Eq, Prod.fst, HAdd.hAdd, OfNat.ofNat, Prod.snd, HSub.hSub
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma gridAdj_cases {a b : ℤ × ℤ} (h : gridAdj a b) :
    (b.1 = a.1 + 1 ∧ b.2 = a.2) ∨ (b.1 = a.1 - 1 ∧ b.2 = a.2) ∨
    (b.1 = a.1 ∧ b.2 = a.2 + 1) ∨ (b.1 = a.1 ∧ b.2 = a.2 - 1) := by
…
```
Mentions: h, Usa2007P4.gridAdj
def Usa2007P4.neighbors4 The explicit four-element finset of neighbours of a cell line 94 source
Source documentation
The explicit four-element finset of neighbours of a cell.

standard axioms: Quot.sound, propext what this means
Statement uses: Prod, Int, Finset
Proof uses: Insert.insert, Prod.mk, HAdd.hAdd, Prod.fst, OfNat.ofNat, Prod.snd, HSub.hSub, Singleton.singleton
9 instances, coercions and auxiliary constants left out.
```
def neighbors4 (a : ℤ × ℤ) : Finset (ℤ × ℤ) :=
…
```
lemma Usa2007P4.mem_neighbors4_of_gridAdj line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Usa2007P4.gridAdj, Membership.mem, Finset, Usa2007P4.neighbors4
Proof uses: And, Eq, Prod.fst, HAdd.hAdd, OfNat.ofNat, Prod.snd, Or, HSub.hSub, Usa2007P4.gridAdj_cases, of_eq_true, Insert.insert, Prod.mk, Singleton.singleton, Eq.trans, True, congr, congrArg, congrFun', eq_self, and_self and 10 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.card_neighbors4_le line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, LE.le, Nat, Finset.card, Usa2007P4.neighbors4, OfNat.ofNat
Proof uses: Insert.insert, Finset, Prod.mk, HAdd.hAdd, Prod.fst, Prod.snd, HSub.hSub, Singleton.singleton, Finset.card_insert_le, Eq, Finset.card_singleton, id
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.card_erase_neighbors4_le line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Membership.mem, Finset, Usa2007P4.neighbors4, LE.le, Nat, Finset.card, Finset.erase, OfNat.ofNat
Proof uses: Eq.mpr, HSub.hSub, id, Eq, congrArg, Finset.card_erase_of_mem, Usa2007P4.card_neighbors4_le
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.preconnected_of_forall_reachable If every cell of T reaches a fixed cell v ∈ T in the induced subgraph on T, then that subgraph is preconnected line 120 source
Source documentation
If every cell of T reaches a fixed cell v ∈ T in the induced subgraph on T, then that subgraph is preconnected.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Reachable, SimpleGraph.induce, Usa2007P4.gridGraph, Subtype.mk, Set, SimpleGraph.Preconnected
Proof uses: SimpleGraph.Reachable.trans, Subtype.property, SimpleGraph.Reachable.symm
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma preconnected_of_forall_reachable (T : Finset (ℤ × ℤ)) {v : ℤ × ℤ} (hv : v ∈ T)
    (h : ∀ c : ℤ × ℤ, ∀ hc : c ∈ T,
      (gridGraph.induce (T : Set (ℤ × ℤ))).Reachable ⟨c, hc⟩ ⟨v, hv⟩) :
    (gridGraph.induce (T : Set (ℤ × ℤ))).Preconnected := by
…
```
Mentions: h
lemma Usa2007P4.exists_walk_length line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Exists, Nat, SimpleGraph.Walk, Subtype.mk, Set, Eq, SimpleGraph.Walk.length
Proof uses: SimpleGraph.Reachable, Exists.intro, rfl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Usa2007P4.dw The depth of a cell: length of a shortest walk from the root r inside D (defined to be 0 outside D) line 152 source
Source documentation
The depth of a cell: length of a shortest walk from the root r inside D (defined to be 0 outside D).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Nat
Proof uses: dite, Nat.find, Exists, SimpleGraph.Walk, Subtype.mk, Set, Eq, SimpleGraph.Walk.length, Classical.propDecidable, Usa2007P4.exists_walk_length, Not, OfNat.ofNat
13 instances, coercions and auxiliary constants left out.
```
noncomputable def dw (c : ℤ × ℤ) : ℕ :=
…
```
lemma Usa2007P4.dw_spec line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Exists, SimpleGraph.Walk, Subtype.mk, Set, Eq, Nat, SimpleGraph.Walk.length, Usa2007P4.dw
Proof uses: Eq.mpr, Nat.find, Classical.propDecidable, Usa2007P4.exists_walk_length, id, congrArg, funext, Decidable, Not, dite_eq_left, OfNat.ofNat, Nat.find_spec
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.dw_le line 161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, SimpleGraph.Walk, Subtype.mk, Set, LE.le, Nat, Usa2007P4.dw, SimpleGraph.Walk.length
Proof uses: Eq.mpr, Nat.find, Exists, Eq, Classical.propDecidable, Usa2007P4.exists_walk_length, id, congrFun', congrArg, Decidable, Not, dite_eq_left, OfNat.ofNat, Nat.find_le, Exists.intro, rfl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.dw_root line 167 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Eq, Nat, Usa2007P4.dw, OfNat.ofNat
Proof uses: Eq.mpr, Nat.find, Exists, SimpleGraph.Walk, Subtype.mk, Set, SimpleGraph.Walk.length, Classical.propDecidable, Usa2007P4.exists_walk_length, id, congrFun', congrArg, Decidable, Not, dite_eq_left, Nat.eq_zero_of_le_zero, Nat.find_le, Exists.intro, SimpleGraph.Walk.nil, rfl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.eq_of_dw_eq_zero line 171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Eq, Nat, Usa2007P4.dw, OfNat.ofNat
Proof uses: SimpleGraph.Walk, Subtype.mk, Set, SimpleGraph.Walk.length, Nat.find, Exists, Classical.propDecidable, Usa2007P4.exists_walk_length, Nat.find_spec, Iff.mp, SimpleGraph.Walk.exists_length_eq_zero_iff, Exists.intro, Eq.mp, congrArg, congrFun', Decidable, Not, dite_eq_left, Eq.symm, Subtype
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.parent_exists Any cell c ≠ r of D has a neighbour of strictly smaller depth: the penultimate cell of a shortest walk from r to c line 181 source
Source documentation
Any cell c ≠ r of D has a neighbour of strictly smaller depth: the penultimate cell of a shortest walk from r to c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Ne, Exists, And, Usa2007P4.gridAdj, LT.lt, Nat, Usa2007P4.dw
Proof uses: SimpleGraph.Walk, Subtype.mk, Set, Eq, SimpleGraph.Walk.length, Usa2007P4.dw_spec, OfNat.ofNat, GT.gt, Or, Nat.eq_zero_or_pos, False.elim, Iff.mp, SimpleGraph.Walk.exists_length_eq_zero_iff, Exists.intro, Eq.symm, congrArg, Subtype, SimpleGraph.Walk.getVert, HSub.hSub, And.intro and 18 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma parent_exists {c : ℤ × ℤ} (hc : c ∈ D) (hcr : c ≠ r) :
    ∃ u ∈ D, gridAdj c u ∧ dw D r hr hpre u < dw D r hr hpre c := by
…
```
Mentions: Usa2007P4.gridAdj, Usa2007P4.dw
def Usa2007P4.parent The parent map: for c ∈ D, c ≠ r a chosen neighbour of c of smaller depth; anything else is mapped to itself line 202 source
Source documentation
The parent map: for c ∈ D, c ≠ r a chosen neighbour of c of smaller depth; anything else is mapped to itself.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph
Proof uses: dite, And, Ne, Eq, Exists.choose, Usa2007P4.gridAdj, LT.lt, Nat, Usa2007P4.dw, Not
15 instances, coercions and auxiliary constants left out.
```
noncomputable def parent (c : ℤ × ℤ) : ℤ × ℤ :=
…
```
lemma Usa2007P4.parent_mem line 205 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Usa2007P4.parent
Proof uses: id, dite, And, Ne, Eq, Exists.choose, Usa2007P4.gridAdj, LT.lt, Nat, Usa2007P4.dw, Not, Eq.mpr, congrArg, dite_eq_left, And.left, Usa2007P4.parent_exists, And.right, Exists.choose_spec, dite_eq_right
15 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.gridAdj_parent line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Ne, Usa2007P4.gridAdj, Usa2007P4.parent
Proof uses: id, Eq.mpr, dite, And, Eq, Exists.choose, LT.lt, Nat, Usa2007P4.dw, Not, And.intro, congrArg, dite_eq_left, And.left, Usa2007P4.parent_exists, And.right, Exists.choose_spec
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.dw_parent_lt line 219 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Ne, LT.lt, Nat, Usa2007P4.dw, Usa2007P4.parent
Proof uses: id, Eq.mpr, dite, And, Eq, Exists.choose, Usa2007P4.gridAdj, Not, And.intro, congrArg, dite_eq_left, And.right, Usa2007P4.parent_exists, Exists.choose_spec
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.parent_root line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Eq, Usa2007P4.parent
Proof uses: id, Eq.mpr, dite, And, Ne, Exists.choose, Usa2007P4.gridAdj, LT.lt, Nat, Usa2007P4.dw, Not, congrArg, dite_eq_right, And.right, rfl, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.parent_ne_self line 229 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Ne, Usa2007P4.parent
Proof uses: Ne.symm, Usa2007P4.ne_of_gridAdj, Usa2007P4.gridAdj_parent
8 instances, coercions and auxiliary constants left out.
lemma Usa2007P4.iterate_parent_mem line 233 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Nat, Nat.iterate, Usa2007P4.parent
Proof uses: Nat.recAux, Eq.mpr, HAdd.hAdd, OfNat.ofNat, id, Eq, congrArg, Nat.succ, Function.iterate_succ_apply', Usa2007P4.parent_mem
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.iterate_parent_root line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Nat, Eq, Nat.iterate, Usa2007P4.parent
Proof uses: Nat.recAux, Eq.refl, OfNat.ofNat, Eq.mpr, HAdd.hAdd, id, congrArg, Nat.succ, Function.iterate_succ_apply', Usa2007P4.parent_root
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.dw_iterate_parent_lt line 246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Ne, Nat, LE.le, OfNat.ofNat, LT.lt, Usa2007P4.dw, Nat.iterate, Usa2007P4.parent
Proof uses: Nat.recAux, absurd, HAdd.hAdd, dite, Eq, Usa2007P4.dw_parent_lt, Eq.symm, Not, Eq.mpr, id, congrArg, Nat.succ, Function.iterate_succ_apply', Usa2007P4.parent_root, Usa2007P4.dw_root, Nat.zero_lt_of_lt, Usa2007P4.iterate_parent_mem, lt_trans
23 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.exists_iterate_parent_eq_root Following parents from any cell of D eventually reaches the root line 264 source
Source documentation
Following parents from any cell of D eventually reaches the root.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Exists, Nat, Eq, Nat.iterate, Usa2007P4.parent
Proof uses: LE.le, Usa2007P4.dw, Nat.recAux, OfNat.ofNat, Exists.intro, Usa2007P4.eq_of_dw_eq_zero, HAdd.hAdd, dite, Not, Ne, False, Eq.mp, congrArg, Usa2007P4.dw_root, Nat.zero_le, Usa2007P4.parent_mem, LT.lt, Usa2007P4.dw_parent_lt, Eq.mpr, id and 3 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma exists_iterate_parent_eq_root {c : ℤ × ℤ} (hc : c ∈ D) :
    ∃ i, (parent D r hr hpre)^[i] c = r := by
…
```
Mentions: Usa2007P4.parent
def Usa2007P4.subtree The subtree rooted at v: all cells of D whose parent chain hits v line 290 source
Source documentation
The subtree rooted at v: all cells of D whose parent chain hits v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph
Proof uses: Finset.filter, Exists, Nat, Eq, Nat.iterate, Usa2007P4.parent, Classical.propDecidable
8 instances, coercions and auxiliary constants left out.
```
noncomputable def subtree (v : ℤ × ℤ) : Finset (ℤ × ℤ) :=
…
```
lemma Usa2007P4.mem_subtree line 293 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Iff, Usa2007P4.subtree, And, Exists, Nat, Eq, Nat.iterate, Usa2007P4.parent
Proof uses: Finset.mem_filter, Classical.propDecidable
8 instances, coercions and auxiliary constants left out.
lemma Usa2007P4.mem_subtree_self line 297 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Usa2007P4.subtree
Proof uses: Eq.mpr, And, Exists, Nat, Eq, Nat.iterate, Usa2007P4.parent, id, congrArg, propext, Usa2007P4.mem_subtree, And.intro, Exists.intro, OfNat.ofNat, rfl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.iterate_parent_mem_subtree_of_le line 301 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Usa2007P4.subtree, Nat, Eq, Nat.iterate, Usa2007P4.parent, LE.le
Proof uses: Eq.mpr, And, Exists, id, congrArg, propext, Usa2007P4.mem_subtree, And.intro, Usa2007P4.iterate_parent_mem, And.left, Eq.mp, Exists.intro, HSub.hSub, HAdd.hAdd, Eq.symm, Function.iterate_add_apply, Nat.sub_add_cancel
14 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.not_mem_subtree_iterate line 310 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Not, Usa2007P4.subtree, Nat, Nat.iterate, Usa2007P4.parent
Proof uses: Exists, Eq, And, False, Eq.mp, congrArg, propext, Usa2007P4.mem_subtree, Eq.mpr, id, And.intro, Exists.intro, HAdd.hAdd, Function.iterate_add_apply
12 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.subtree_root line 320 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Eq, Usa2007P4.subtree
Proof uses: Finset.ext, Eq.mpr, Iff, And, Exists, Nat, Nat.iterate, Usa2007P4.parent, id, congrArg, propext, Usa2007P4.mem_subtree, Iff.intro, And.left, And.intro, Usa2007P4.exists_iterate_parent_eq_root
8 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Usa2007P4.children The children of v: cells of D whose parent is v line 329 source
Source documentation
The children of v: cells of D whose parent is v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph
Proof uses: Finset.filter, And, Eq, Usa2007P4.parent, Ne
12 instances, coercions and auxiliary constants left out.
```
noncomputable def children (v : ℤ × ℤ) : Finset (ℤ × ℤ) :=
…
```
lemma Usa2007P4.mem_children line 332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Iff, Usa2007P4.children, And, Eq, Usa2007P4.parent, Ne
Proof uses: Finset.mem_filter
12 instances, coercions and auxiliary constants left out.
lemma Usa2007P4.children_ne_root line 336 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Usa2007P4.children, Ne
Proof uses: Eq, And, Usa2007P4.parent, False, And.right, Eq.mp, congrArg, Usa2007P4.parent_root, And.left, propext, Usa2007P4.mem_children
9 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.dw_child line 343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Usa2007P4.children, LT.lt, Nat, Usa2007P4.dw
Proof uses: Ne, Usa2007P4.children_ne_root, Usa2007P4.parent, Usa2007P4.dw_parent_lt, And.left, And, Eq, Iff.mp, Usa2007P4.mem_children, Eq.mp, congrArg, And.right
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.children_subset_neighbors line 349 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Usa2007P4.children, Usa2007P4.neighbors4
Proof uses: Ne, Usa2007P4.children_ne_root, Usa2007P4.gridAdj, Usa2007P4.parent, Usa2007P4.gridAdj_parent, And.left, And, Eq, Iff.mp, Usa2007P4.mem_children, Usa2007P4.mem_neighbors4_of_gridAdj, Usa2007P4.gridAdj_of_gridAdj, Eq.mp, congrArg, And.right
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.child_ne_parent line 356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Ne, Usa2007P4.children, Usa2007P4.parent
Proof uses: And, Eq, Iff.mp, Usa2007P4.mem_children, LT.lt, Nat, Usa2007P4.dw, Usa2007P4.dw_child, Usa2007P4.dw_parent_lt, absurd, False, lt_trans, Eq.mp, congrArg, lt_irrefl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.card_children_le_three line 366 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Ne, LE.le, Nat, Finset.card, Usa2007P4.children, OfNat.ofNat
Proof uses: Finset.erase, Usa2007P4.neighbors4, Usa2007P4.parent, Eq.mpr, And, id, Eq, congrArg, propext, Finset.mem_erase, And.intro, Usa2007P4.child_ne_parent, Usa2007P4.children_subset_neighbors, le_trans, Finset.card_le_card, Usa2007P4.card_erase_neighbors4_le, Usa2007P4.mem_neighbors4_of_gridAdj, Usa2007P4.gridAdj_parent
17 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.card_children_le_four line 376 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, LE.le, Nat, Finset.card, Usa2007P4.children, OfNat.ofNat
Proof uses: le_trans, Usa2007P4.neighbors4, Finset.card_le_card, Usa2007P4.children_subset_neighbors, Usa2007P4.card_neighbors4_le
12 instances, coercions and auxiliary constants left out.
lemma Usa2007P4.subtree_eq The subtree of v decomposes as v together with the subtrees of its children line 382 source
Source documentation
The subtree of v decomposes as v together with the subtrees of its children.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Eq, Usa2007P4.subtree, Insert.insert, Finset.biUnion, Usa2007P4.children
Proof uses: Finset.ext, Eq.mpr, Iff, And, Exists, Nat, Nat.iterate, Usa2007P4.parent, Or, Ne, id, congr, congrArg, Eq.trans, funext, Iff.intro, dite, Or.inl, Not, Or.inr and 16 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma subtree_eq {v : ℤ × ℤ} (hv : v ∈ D) :
    subtree D r hr hpre v =
      insert v ((children D r hr hpre v).biUnion (subtree D r hr hpre)) := by
…
```
Mentions: Usa2007P4.subtree, Usa2007P4.children
lemma Usa2007P4.disjoint_subtree_children The subtrees of distinct children of v are disjoint line 410 source
Source documentation
The subtrees of distinct children of v are disjoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Set.PairwiseDisjoint, Usa2007P4.children, Usa2007P4.subtree
Proof uses: Set, Ne, id, Function.onFun, Disjoint, Eq.mpr, Not, Eq, congrArg, propext, Finset.disjoint_left, Exists, Nat, Nat.iterate, Usa2007P4.parent, And, False, Iff.mp, Usa2007P4.mem_subtree, LT.lt and 22 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma disjoint_subtree_children {v : ℤ × ℤ} (hv : v ∈ D) :
    ((children D r hr hpre v) : Set (ℤ × ℤ)).PairwiseDisjoint (subtree D r hr hpre) := by
…
```
Mentions: Usa2007P4.children, Usa2007P4.subtree
lemma Usa2007P4.card_subtree The size of a subtree is one more than the sum of the sizes of the subtrees of its children line 453 source
Source documentation
The size of a subtree is one more than the sum of the sizes of the subtrees of its children.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Eq, Nat, Finset.card, Usa2007P4.subtree, HAdd.hAdd, OfNat.ofNat, Finset.sum, Usa2007P4.children
Proof uses: Not, Finset.biUnion, And, Exists, False, Eq.mp, congrArg, propext, Finset.mem_biUnion, Nat.iterate, Usa2007P4.parent, Iff.mp, Usa2007P4.mem_subtree, Ne, Usa2007P4.mem_children, GT.gt, Or, Nat.eq_zero_or_pos, Eq.symm, dite and 12 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma card_subtree {v : ℤ × ℤ} (hv : v ∈ D) :
    (subtree D r hr hpre v).card =
      1 + ∑ u ∈ children D r hr hpre v, (subtree D r hr hpre u).card := by
…
```
Mentions: Usa2007P4.subtree, Usa2007P4.children
lemma Usa2007P4.reachable_of_chain If the parent chain from c stays inside T and reaches v, then c reaches v in the induced subgraph on T line 480 source
Source documentation
If the parent chain from c stays inside T and reaches v, then c reaches v in the induced subgraph on T.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, LE.le, Nat, Nat.iterate, Usa2007P4.parent, Eq, SimpleGraph.Reachable, Subtype.mk, Set
Proof uses: Nat.recAux, OfNat.ofNat, SimpleGraph.Reachable.refl, HAdd.hAdd, dite, Not, Ne, False, Eq.mp, congrArg, Usa2007P4.iterate_parent_root, Usa2007P4.gridAdj, Usa2007P4.gridAdj_parent, Nat.succ, Function.iterate_succ_apply, SimpleGraph.Adj, Iff.mpr, SimpleGraph.induce_adj, Nonempty.map, SimpleGraph.Walk and 1 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma reachable_of_chain (T : Finset (ℤ × ℤ)) (hTD : T ⊆ D) {c v : ℤ × ℤ}
    (hc : c ∈ T) (hv : v ∈ T) (i : ℕ)
    (hchain : ∀ j ≤ i, (parent D r hr hpre)^[j] c ∈ T)
    (hiv : (parent D r hr hpre)^[i] c = v) :
    (gridGraph.induce (T : Set (ℤ × ℤ))).Reachable ⟨c, hc⟩ ⟨v, hv⟩ := by
…
```
Mentions: Usa2007P4.parent
lemma Usa2007P4.isAnimal_subtree The subtree rooted at any cell of D is an animal line 515 source
Source documentation
The subtree rooted at any cell of D is an animal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Usa2007P4.IsAnimal, Usa2007P4.subtree
Proof uses: Usa2007P4.IsAnimal.mk, Exists.intro, Usa2007P4.mem_subtree_self, Usa2007P4.preconnected_of_forall_reachable, Exists, Nat, Eq, Nat.iterate, Usa2007P4.parent, And, SimpleGraph.Reachable, Subtype.mk, Set, Iff.mp, Usa2007P4.mem_subtree, Usa2007P4.reachable_of_chain, Finset.filter_subset, Classical.propDecidable, LE.le, Usa2007P4.iterate_parent_mem_subtree_of_le
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma isAnimal_subtree {v : ℤ × ℤ} (hv : v ∈ D) : IsAnimal (subtree D r hr hpre v) := by
…
```
Mentions: Usa2007P4.IsAnimal, Usa2007P4.subtree
lemma Usa2007P4.isAnimal_sdiff_subtree Removing a rooted subtree (with v ≠ r) from D leaves an animal line 526 source
Source documentation
Removing a rooted subtree (with v ≠ r) from D leaves an animal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, Ne, Usa2007P4.IsAnimal, SDiff.sdiff, Usa2007P4.subtree
Proof uses: Eq.mpr, And, Not, id, Eq, congrArg, propext, Finset.mem_sdiff, And.intro, Exists, Nat, Nat.iterate, Usa2007P4.parent, False, Iff.mp, Usa2007P4.mem_subtree, Eq.symm, Eq.mp, Usa2007P4.iterate_parent_root, Usa2007P4.IsAnimal.mk and 13 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma isAnimal_sdiff_subtree {v : ℤ × ℤ} (_hv : v ∈ D) (hvr : v ≠ r) :
    IsAnimal (D \ subtree D r hr hpre v) := by
…
```
Mentions: Usa2007P4.IsAnimal, Usa2007P4.subtree
lemma Usa2007P4.exists_split Splitting lemma line 548 source
Source documentation
Splitting lemma. Any animal with at least 4 * 2007 - 2 cells can be partitioned into two dinosaurs; in particular it is not primitive.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Membership.mem, SimpleGraph.Preconnected, SimpleGraph.induce, Usa2007P4.gridGraph, LE.le, Nat, HSub.hSub, HMul.hMul, OfNat.ofNat, Finset.card, Exists, And, Usa2007P4.IsDinosaur, Disjoint, Eq, Union.union
Proof uses: Finset.filter, Usa2007P4.subtree, rfl, Eq.mpr, id, congrArg, propext, Finset.mem_filter, And.intro, Usa2007P4.subtree_root, Usa2007P4.dw, Finset.exists_max_image, Exists.intro, Eq.mp, Usa2007P4.children, Decidable.byContradiction, Not, LT.lt, Nat.lt_of_not_le, And.left and 32 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
lemma exists_split (hcard : 4 * 2007 - 2 ≤ D.card) :
    ∃ A B : Finset (ℤ × ℤ), IsDinosaur A ∧ IsDinosaur B ∧ Disjoint A B ∧ A ∪ B = D := by
…
```
Mentions: Usa2007P4.IsDinosaur
def Usa2007P4.crossAux The body of cross, kept reducible so that membership and cardinality can be unfolded in the auxiliary lemmas mem_aux and card_aux line 606 source
Source documentation
The body of cross, kept reducible so that membership and cardinality can be unfolded in the auxiliary lemmas mem_aux and card_aux. (In this environment, Finset.Icc on ℤ records a Preorder ℤ instance whose term contains the noncomputable Int.instConditionallyCompleteLinearOrder, hence the noncomputable keyword.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: Union.union, Finset.product, Finset.Icc, Neg.neg, OfNat.ofNat, Singleton.singleton
8 instances, coercions and auxiliary constants left out.
```
noncomputable def crossAux : Finset (ℤ × ℤ) :=
…
```
def Usa2007P4.cross The cross with center (0,0) and four arms of length 2006 line 619 source
Source documentation
The cross with center (0,0) and four arms of length 2006.
Marked irreducible: the Preorder ℤ instance recorded in the Finset.Icc terms of the body is a very large term, and any definitional unfolding of cross (as happens when checking x ∈ cross against x ∈ ↑cross for the coercion to Set, e.g. when building elements of ↥(↑cross)) exceeds the elaborator's recursion depth limit. Unfold instead via cross_def, mem_aux and card_aux where needed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int
Proof uses: Usa2007P4.crossAux
```
noncomputable def cross : Finset (ℤ × ℤ) := crossAux
```
Mentions: Usa2007P4.crossAux
lemma Usa2007P4.cross_def Unfolding lemma for cross line 624 source
Source documentation
Unfolding lemma for cross. Do not use simp only [cross] or cross.eq_unfold: re-elaborating the auto-generated equation lemma hits the recursion depth limit.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Finset, Prod, Int, Usa2007P4.cross, Usa2007P4.crossAux
Proof uses: Eq.refl

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma cross_def : cross = crossAux := by
…
```
Mentions: Usa2007P4.cross, Usa2007P4.crossAux
lemma Usa2007P4.mem_aux Coordinate characterization of membership in crossAux line 628 source
Source documentation
Coordinate characterization of membership in crossAux.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Iff, Membership.mem, Finset, Usa2007P4.crossAux, Or, And, Eq, Prod.snd, OfNat.ofNat, LE.le, Neg.neg, Prod.fst
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, Union.union, SProd.sprod, Finset.Icc, Singleton.singleton, congr, Iff.intro, Or.inl, And.intro, Or.inr
24 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma mem_aux {c : ℤ × ℤ} :
    c ∈ crossAux ↔ (c.2 = 0 ∧ -2006 ≤ c.1 ∧ c.1 ≤ 2006) ∨
      (c.1 = 0 ∧ -2006 ≤ c.2 ∧ c.2 ≤ 2006) := by
…
```
Mentions: Usa2007P4.crossAux
lemma Usa2007P4.mem_cross_iff Coordinate characterization of membership in cross line 642 source
Source documentation
Coordinate characterization of membership in cross.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Iff, Membership.mem, Finset, Usa2007P4.cross, Or, And, Eq, Prod.snd, OfNat.ofNat, LE.le, Neg.neg, Prod.fst
Proof uses: Eq.mpr, Usa2007P4.crossAux, id, congrArg, Usa2007P4.cross_def, Usa2007P4.mem_aux
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma mem_cross_iff {c : ℤ × ℤ} :
    c ∈ cross ↔ (c.2 = 0 ∧ -2006 ≤ c.1 ∧ c.1 ≤ 2006) ∨
      (c.1 = 0 ∧ -2006 ≤ c.2 ∧ c.2 ≤ 2006) := by
…
```
Mentions: Usa2007P4.cross
lemma Usa2007P4.mem_center_cross line 648 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Membership.mem, Prod, Int, Finset, Usa2007P4.cross, Prod.mk, OfNat.ofNat
Proof uses: Eq.mpr, Or, And, Eq, Prod.snd, LE.le, Neg.neg, Prod.fst, id, congrArg, propext, Usa2007P4.mem_cross_iff, Or.inl, And.intro, rfl, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.mem_cross_of_nat The four arm points at distance n from the center lie in cross when n ≤ 2006 line 654 source
Source documentation
The four arm points at distance n from the center lie in cross when n ≤ 2006.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, And, Membership.mem, Prod, Int, Finset, Usa2007P4.cross, Prod.mk, Neg.neg
Proof uses: Int.natCast_nonneg, cast, Eq.symm, And.intro, Eq.mpr, Or, Eq, Prod.snd, Prod.fst, id, congrArg, propext, Usa2007P4.mem_cross_iff
32 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma mem_cross_of_nat {n : ℕ} (hn : n ≤ 2006) :
    (((n : ℤ), 0) ∈ cross) ∧ ((-((n : ℤ)), 0) ∈ cross) ∧
      (((0 : ℤ), (n : ℤ)) ∈ cross) ∧ (((0 : ℤ), -((n : ℤ))) ∈ cross) := by
…
```
Mentions: Usa2007P4.cross
lemma Usa2007P4.card_aux line 661 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Prod, Int, Usa2007P4.crossAux, OfNat.ofNat
Proof uses: Finset, Finset.product, HMul.hMul, Finset.card_product, Finset.Icc, Neg.neg, Singleton.singleton, Eq.mpr, id, congrArg, Int.toNat, HSub.hSub, HAdd.hAdd, Int.card_Icc, Finset.card_singleton, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl and 20 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.card_cross line 688 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Prod, Int, Usa2007P4.cross, OfNat.ofNat
Proof uses: Eq.mpr, Usa2007P4.crossAux, id, congrArg, Finset, Usa2007P4.cross_def, Usa2007P4.card_aux
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.reach_right Walking down the positive x-arm: ((n,0)) reaches the center line 693 source
Source documentation
Walking down the positive x-arm: ((n,0)) reaches the center.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Membership.mem, Prod, Int, Finset, Usa2007P4.cross, Prod.mk, SimpleGraph.Reachable, SimpleGraph.induce, Usa2007P4.gridGraph, Subtype.mk, Set, Usa2007P4.mem_center_cross
Proof uses: Nat.recAux, SimpleGraph.Reachable.refl, HAdd.hAdd, And.left, And, Neg.neg, Usa2007P4.mem_cross_of_nat, Usa2007P4.gridAdj, id, Eq, Int.natAbs, HSub.hSub, Prod.fst, Prod.snd, Eq.mpr, congrArg, Nat.cast_add, Nat.cast_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast and 41 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma reach_right :
    ∀ n : ℕ, n ≤ 2006 → ∀ h : (((n : ℤ), 0) ∈ cross),
      (gridGraph.induce (cross : Set (ℤ × ℤ))).Reachable ⟨((n : ℤ), 0), h⟩
        ⟨(0, 0), mem_center_cross⟩ := by
…
```
Mentions: h, Usa2007P4.cross, Usa2007P4.mem_center_cross
lemma Usa2007P4.reach_left Walking down the negative x-arm: ((-n,0)) reaches the center line 718 source
Source documentation
Walking down the negative x-arm: ((-n,0)) reaches the center.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Membership.mem, Prod, Int, Finset, Usa2007P4.cross, Prod.mk, Neg.neg, SimpleGraph.Reachable, SimpleGraph.induce, Usa2007P4.gridGraph, Subtype.mk, Set, Usa2007P4.mem_center_cross
Proof uses: Nat.recAux, SimpleGraph.Reachable.refl, HAdd.hAdd, And.left, And, And.right, Usa2007P4.mem_cross_of_nat, Usa2007P4.gridAdj, id, Eq, Int.natAbs, HSub.hSub, Prod.fst, Prod.snd, Eq.mpr, congrArg, Nat.cast_add, Nat.cast_one, Mathlib.Tactic.Ring.of_eq, Int.rawCast and 44 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma reach_left :
    ∀ n : ℕ, n ≤ 2006 → ∀ h : ((-((n : ℤ)), 0) ∈ cross),
      (gridGraph.induce (cross : Set (ℤ × ℤ))).Reachable ⟨(-((n : ℤ)), 0), h⟩
        ⟨(0, 0), mem_center_cross⟩ := by
…
```
Mentions: h, Usa2007P4.cross, Usa2007P4.mem_center_cross
lemma Usa2007P4.reach_up Walking down the positive y-arm: ((0,n)) reaches the center line 743 source
Source documentation
Walking down the positive y-arm: ((0,n)) reaches the center.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Membership.mem, Prod, Int, Finset, Usa2007P4.cross, Prod.mk, SimpleGraph.Reachable, SimpleGraph.induce, Usa2007P4.gridGraph, Subtype.mk, Set, Usa2007P4.mem_center_cross
Proof uses: Nat.recAux, SimpleGraph.Reachable.refl, HAdd.hAdd, And.left, Neg.neg, And.right, And, Usa2007P4.mem_cross_of_nat, Usa2007P4.gridAdj, id, Eq, Int.natAbs, HSub.hSub, Prod.fst, Prod.snd, Eq.mpr, congrArg, Nat.cast_add, Nat.cast_one, Mathlib.Tactic.Ring.of_eq and 42 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma reach_up :
    ∀ n : ℕ, n ≤ 2006 → ∀ h : (((0 : ℤ), (n : ℤ)) ∈ cross),
      (gridGraph.induce (cross : Set (ℤ × ℤ))).Reachable ⟨((0 : ℤ), (n : ℤ)), h⟩
        ⟨(0, 0), mem_center_cross⟩ := by
…
```
Mentions: h, Usa2007P4.cross, Usa2007P4.mem_center_cross
lemma Usa2007P4.reach_down Walking down the negative y-arm: ((0,-n)) reaches the center line 768 source
Source documentation
Walking down the negative y-arm: ((0,-n)) reaches the center.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Membership.mem, Prod, Int, Finset, Usa2007P4.cross, Prod.mk, Neg.neg, SimpleGraph.Reachable, SimpleGraph.induce, Usa2007P4.gridGraph, Subtype.mk, Set, Usa2007P4.mem_center_cross
Proof uses: Nat.recAux, SimpleGraph.Reachable.refl, HAdd.hAdd, And.right, And, Usa2007P4.mem_cross_of_nat, Usa2007P4.gridAdj, id, Eq, Int.natAbs, HSub.hSub, Prod.fst, Prod.snd, Eq.mpr, congrArg, Nat.cast_add, Nat.cast_one, Mathlib.Tactic.Ring.of_eq, Int.rawCast, inferInstance and 43 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma reach_down :
    ∀ n : ℕ, n ≤ 2006 → ∀ h : (((0 : ℤ), -((n : ℤ))) ∈ cross),
      (gridGraph.induce (cross : Set (ℤ × ℤ))).Reachable ⟨((0 : ℤ), -((n : ℤ))), h⟩
        ⟨(0, 0), mem_center_cross⟩ := by
…
```
Mentions: h, Usa2007P4.cross, Usa2007P4.mem_center_cross
lemma Usa2007P4.isAnimal_cross line 792 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2007P4.IsAnimal, Usa2007P4.cross
Proof uses: Usa2007P4.IsAnimal.mk, Exists.intro, Prod, Int, Membership.mem, Finset, Prod.mk, OfNat.ofNat, Usa2007P4.mem_center_cross, SimpleGraph.Reachable, SimpleGraph.induce, Usa2007P4.gridGraph, Subtype.mk, Set, Or, And, Eq, Prod.snd, LE.le, Neg.neg and 16 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
def Usa2007P4.InSameArm b lies in the same arm of the cross as a (meaningful when a is not the center) line 829 source
Source documentation
b lies in the same arm of the cross as a (meaningful when a is not the center).

no axioms what this means
Statement uses: Prod, Int
Proof uses: And, LT.lt, OfNat.ofNat, Prod.snd, Eq, Prod.fst
2 instances, coercions and auxiliary constants left out.
```
def InSameArm (a b : ℤ × ℤ) : Prop :=
…
```
lemma Usa2007P4.inSameArm_refl line 833 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Membership.mem, Finset, Usa2007P4.cross, Usa2007P4.InSameArm
Proof uses: Or, And, Eq, Prod.snd, OfNat.ofNat, LE.le, Neg.neg, Prod.fst, Iff.mp, Usa2007P4.mem_cross_iff, And.intro, LT.lt
18 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.inSameArm_trans line 838 source
no axioms what this means
Statement uses: Prod, Int, Usa2007P4.InSameArm
Proof uses: LT.lt, OfNat.ofNat, Prod.snd, And, Eq, Prod.fst, And.intro, And.right
3 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.inSameArm_of_gridAdj A step along the cross between two cells, the target not being the center, stays in the same arm line 847 source
Source documentation
A step along the cross between two cells, the target not being the center, stays in the same arm.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Membership.mem, Finset, Usa2007P4.cross, Ne, Prod.mk, OfNat.ofNat, Usa2007P4.gridAdj, Usa2007P4.InSameArm
Proof uses: Or, And, Eq, Prod.snd, LE.le, Neg.neg, Prod.fst, Iff.mp, Usa2007P4.mem_cross_iff, Not, Prod.ext, And.left, And.right, HAdd.hAdd, HSub.hSub, Usa2007P4.gridAdj_cases, And.intro, LT.lt
63 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma inSameArm_of_gridAdj {a b : ℤ × ℤ} (ha : a ∈ cross) (hb : b ∈ cross)
    (hb0 : b ≠ (0, 0)) (h : gridAdj a b) : InSameArm a b := by
…
```
Mentions: Usa2007P4.cross, h, Usa2007P4.gridAdj, Usa2007P4.InSameArm
lemma Usa2007P4.inSameArm_walk Any walk inside a center-free subset of the cross stays in one arm line 858 source
Source documentation
Any walk inside a center-free subset of the cross stays in one arm.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, LE.le, Usa2007P4.cross, Not, Membership.mem, Prod.mk, OfNat.ofNat, SimpleGraph.Walk, SimpleGraph.induce, Usa2007P4.gridGraph, Usa2007P4.InSameArm, Set
Proof uses: SimpleGraph.Walk.rec, Usa2007P4.inSameArm_refl, Iff.mp, Finset.mem_coe, Subtype.property, SimpleGraph.Adj, Usa2007P4.inSameArm_trans, Usa2007P4.inSameArm_of_gridAdj, Eq, Eq.rec, SimpleGraph.induce_adj
20 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma inSameArm_walk {T : Finset (ℤ × ℤ)} (hsub : T ⊆ cross) (h0 : ((0, 0) : ℤ × ℤ) ∉ T)
    {u v : (T : Set (ℤ × ℤ))}
    (w : (gridGraph.induce (T : Set (ℤ × ℤ))).Walk u v) :
    InSameArm (u : ℤ × ℤ) (v : ℤ × ℤ) := by
…
```
Mentions: Usa2007P4.cross, Usa2007P4.InSameArm
lemma Usa2007P4.mem_center_of_dinosaur_subset line 872 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Prod, Int, Usa2007P4.IsDinosaur, LE.le, Usa2007P4.cross, Membership.mem, Prod.mk, OfNat.ofNat
Proof uses: Decidable.byContradiction, Not, Nat, Finset.card, And.right, Usa2007P4.IsAnimal, Finset.Nonempty, False, Usa2007P4.IsAnimal.nonempty, And.left, Ne, Eq, Eq.rec, Usa2007P4.InSameArm, Usa2007P4.inSameArm_walk, Subtype.mk, Set, Iff.mpr, Finset.mem_coe, Nonempty.some and 39 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 75 steps
Open to load the checked before-and-after goal states.
lemma Usa2007P4.isPrimitive_cross line 946 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2007P4.IsPrimitive, Usa2007P4.cross
Proof uses: And.intro, Usa2007P4.IsDinosaur, Not, Exists, Finset, Prod, Int, Usa2007P4.IsDinoPartition, Usa2007P4.IsAnimal, LE.le, Nat, OfNat.ofNat, Finset.card, Usa2007P4.isAnimal_cross, Eq.mpr, id, Eq, congrArg, Usa2007P4.card_cross, Mathlib.Meta.NormNum.isNat_le_true and 20 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
determine Usa2007P4.answer The answer to USAMO 2007 Problem 4 line 966 source
Source documentation
The answer to USAMO 2007 Problem 4.

no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
determine answer : ℕ := 8025
```
problem Usa2007P4.usa2007_p4 line 968 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsGreatest, Nat, Set.ofPred, Exists, Finset, Prod, Int, And, Usa2007P4.IsPrimitive, Eq, Finset.card, Usa2007P4.answer
Proof uses: And.intro, Membership.mem, Set, upperBounds, Exists.intro, Usa2007P4.cross, Usa2007P4.isPrimitive_cross, Usa2007P4.card_cross, LE.le, Usa2007P4.IsDinosaur, Not, Usa2007P4.IsDinoPartition, Usa2007P4.IsAnimal, OfNat.ofNat, Decidable.byContradiction, LT.lt, Nat.lt_of_not_le, HSub.hSub, HMul.hMul, Finset.Nonempty and 37 more
28 instances, coercions and auxiliary constants left out.

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