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

67 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2020 Problem 2

An empty 2020 × 2020 × 2020 cube is given, and a 2020 × 2020 grid of square unit cells is drawn on each of its six faces. A beam is a 1 × 1 × 2020 rectangular prism. Several beams are placed inside the cube subject to the following conditions:

The two 1 × 1 faces of each beam coincide with unit cells lying on opposite faces of the cube. (Hence, there are 3 · 2020² possible positions for a beam.)
No two beams have intersecting interiors.
The interiors of each of the four 1 × 2020 faces of each beam touch either a face of the cube or the interior of the face of another beam.

What is the smallest positive number of beams that can be placed to satisfy these conditions?

Imports (11)

Imported by 1 file

Compfiles.lean

inductive Usa2020P2.Dir The three possible orientations of a beam line 84 source

Source documentation

The three possible orientations of a beam.

no axioms what this means

inductive Dir | X | Y | Z deriving DecidableEq

/-- A beam in an `n × n × n` cube, given by its orientation and the two
coordinates of its cross-section:
* `xBeam j k` occupies `y = j`, `z = k` and spans the `x`-direction;
* `yBeam i k` occupies `x = i`, `z = k` and spans the `y`-direction;
* `zBeam i j` occupies `x = i`, `y = j` and spans the `z`-direction. -/

inductive Usa2020P2.Beam Documented declaration: Beam line 91 source
Source documentation
A beam in an n × n × n cube, given by its orientation and the two coordinates of its cross-section:
- xBeam j k occupies y = j, z = k and spans the x-direction;
- yBeam i k occupies x = i, z = k and spans the y-direction;
- zBeam i j occupies x = i, y = j and spans the z-direction.
no axioms what this means
Statement uses: Nat
```
inductive Beam (n : ℕ)
  | xBeam (j k : Fin n)
  | yBeam (i k : Fin n)
  | zBeam (i j : Fin n)
  deriving DecidableEq

variable {n : ℕ}

namespace Beam

/-- The orientation of a beam. -/
```
def Usa2020P2.Beam.dir The orientation of a beam line 102 source
Source documentation
The orientation of a beam.

no axioms what this means
Statement uses: Nat, Usa2020P2.Beam, Usa2020P2.Dir
Proof uses: Usa2020P2.Beam.dir.match_1, Fin, Usa2020P2.Dir.X, Usa2020P2.Dir.Y, Usa2020P2.Dir.Z
```
def dir : Beam n → Dir
  | xBeam .. => .X
  | yBeam .. => .Y
  | zBeam .. => .Z

/-- `covers b x y z` means that beam `b` contains the unit cube at
coordinates `(x, y, z)`. -/
```
Mentions: Usa2020P2.Beam, Usa2020P2.Dir, Usa2020P2.Beam.covers
def Usa2020P2.Beam.covers covers b x y z means that beam b contains the unit cube at coordinates (x, y, z) line 109 source
Source documentation
covers b x y z means that beam b contains the unit cube at coordinates (x, y, z).

no axioms what this means
Statement uses: Nat, Usa2020P2.Beam, Fin
Proof uses: Usa2020P2.Beam.dir.match_1, And, Eq
```
def covers : Beam n → Fin n → Fin n → Fin n → Prop
  | xBeam j k => fun _ y z => y = j ∧ z = k
  | yBeam i k => fun x _ z => x = i ∧ z = k
  | zBeam i j => fun x y _ => x = i ∧ y = j

end Beam

open Beam

/-- The non-intersection condition: two distinct beams do not share a unit
cube. -/
```
Mentions: Usa2020P2.Beam
def Usa2020P2.DisjointBeams The non-intersection condition: two distinct beams do not share a unit cube line 120 source
Source documentation
The non-intersection condition: two distinct beams do not share a unit cube.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam
Proof uses: Membership.mem, Exists, Fin, And, Usa2020P2.Beam.covers, Eq
2 instances, coercions and auxiliary constants left out.
```
def DisjointBeams (S : Finset (Beam n)) : Prop :=
…
```
Mentions: S, Usa2020P2.Beam
def Usa2020P2.xSupp The four side-face support conditions for xBeam j k: faces at y = j, y = j+1, z = k, z = k+1 line 125 source
Source documentation
The four side-face support conditions for xBeam j k: faces at y = j, y = j+1, z = k, z = k+1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Fin
Proof uses: And, Or, Eq, OfNat.ofNat, Exists, HAdd.hAdd, Membership.mem, Usa2020P2.Beam.xBeam, Usa2020P2.Beam.zBeam, Usa2020P2.Beam.yBeam
6 instances, coercions and auxiliary constants left out.
```
def xSupp {n : ℕ} (S : Finset (Beam n)) (j k : Fin n) : Prop :=
…
```
Mentions: S, Usa2020P2.Beam
def Usa2020P2.ySupp The four side-face support conditions for yBeam i k: faces at x = i, x = i+1, z = k, z = k+1 line 137 source
Source documentation
The four side-face support conditions for yBeam i k: faces at x = i, x = i+1, z = k, z = k+1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Fin
Proof uses: And, Or, Eq, OfNat.ofNat, Exists, HAdd.hAdd, Membership.mem, Usa2020P2.Beam.yBeam, Usa2020P2.Beam.zBeam, Usa2020P2.Beam.xBeam
6 instances, coercions and auxiliary constants left out.
```
def ySupp {n : ℕ} (S : Finset (Beam n)) (i k : Fin n) : Prop :=
…
```
Mentions: S, Usa2020P2.Beam
def Usa2020P2.zSupp The four side-face support conditions for zBeam i j: faces at x = i, x = i+1, y = j, y = j+1 line 149 source
Source documentation
The four side-face support conditions for zBeam i j: faces at x = i, x = i+1, y = j, y = j+1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Fin
Proof uses: And, Or, Eq, OfNat.ofNat, Exists, HAdd.hAdd, Membership.mem, Usa2020P2.Beam.zBeam, Usa2020P2.Beam.yBeam, Usa2020P2.Beam.xBeam
6 instances, coercions and auxiliary constants left out.
```
def zSupp {n : ℕ} (S : Finset (Beam n)) (i j : Fin n) : Prop :=
…
```
Mentions: S, Usa2020P2.Beam
def Usa2020P2.Supp The face-support condition for every beam in S line 160 source
Source documentation
The face-support condition for every beam in S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam
Proof uses: And, Fin, Membership.mem, Usa2020P2.Beam.xBeam, Usa2020P2.xSupp, Usa2020P2.Beam.yBeam, Usa2020P2.ySupp, Usa2020P2.Beam.zBeam, Usa2020P2.zSupp
2 instances, coercions and auxiliary constants left out.
```
def Supp (S : Finset (Beam n)) : Prop :=
…
```
Mentions: S, Usa2020P2.Beam
def Usa2020P2.zLayer The z-layer of a beam (dummy value for zBeams, which span all layers) line 167 source
Source documentation
The z-layer of a beam (dummy value for zBeams, which span all layers).

no axioms what this means
Statement uses: Nat, Usa2020P2.Beam, Fin
Proof uses: Usa2020P2.Beam.dir.match_1
```
def zLayer : Beam n → Fin n
  | xBeam _ k => k
  | yBeam _ k => k
  | zBeam i _ => i

/-- The `x`-layer of a beam (dummy value for `xBeam`s). -/
```
Mentions: Usa2020P2.Beam
def Usa2020P2.xLayer The x-layer of a beam (dummy value for xBeams) line 173 source
Source documentation
The x-layer of a beam (dummy value for xBeams).

no axioms what this means
Statement uses: Nat, Usa2020P2.Beam, Fin
Proof uses: Usa2020P2.Beam.dir.match_1
```
def xLayer : Beam n → Fin n
  | xBeam j _ => j
  | yBeam i _ => i
  | zBeam i _ => i

/-- The `y`-layer of a beam (dummy value for `yBeam`s). -/
```
Mentions: Usa2020P2.Beam

def Usa2020P2.yLayer The y-layer of a beam (dummy value for yBeams) line 179 source

Source documentation

The y-layer of a beam (dummy value for yBeams).

no axioms what this means

Statement uses: Nat, Usa2020P2.Beam, Fin

Proof uses: Usa2020P2.Beam.dir.match_1

def yLayer : Beam n → Fin n
  | xBeam j _ => j
  | yBeam i _ => i
  | zBeam _ j => j

/-- A one-dimensional propagation lemma: if a property of positions always
propagates to the left and right neighbors (unless at the boundary), then it
holds everywhere once it holds somewhere. -/

Mentions: Usa2020P2.Beam

theorem Usa2020P2.fill1d Documented declaration: fill1d line 187 source
Source documentation
A one-dimensional propagation lemma: if a property of positions always propagates to the left and right neighbors (unless at the boundary), then it holds everywhere once it holds somewhere.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, And, Or, Eq, OfNat.ofNat, Exists, HAdd.hAdd
Proof uses: LT.lt, Fin.mk, Nat.recAux, Eq.mpr, id, congrArg, Fin.mk.congr_simp, add_zero, Fin.ext, Eq.mp, LE.le, HSub.hSub, tsub_zero, le_total
37 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
```
theorem fill1d {n : ℕ} (P : Fin n → Prop)
    (hP : ∀ i, P i → (i.val = 0 ∨ ∃ i', i'.val + 1 = i.val ∧ P i') ∧
      (i.val + 1 = n ∨ ∃ i', i'.val = i.val + 1 ∧ P i'))
    {i₀ : Fin n} (hi₀ : P i₀) (i : Fin n) : P i := by
…
```
Mentions: P
theorem Usa2020P2.fill_xBeam_y An xBeam in a cube without zBeams fills its whole row along y line 232 source
Source documentation
An xBeam in a cube without zBeams fills its whole row along y.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.zBeam, Usa2020P2.Beam.xBeam
Proof uses: Usa2020P2.fill1d, Or, Eq, OfNat.ofNat, Exists, And, HAdd.hAdd, Usa2020P2.Beam.yBeam, Usa2020P2.xSupp, And.left, Usa2020P2.ySupp, Usa2020P2.zSupp, And.intro, Or.inl, Or.inr, Exists.intro, absurd
11 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem fill_xBeam_y {n : ℕ} {S : Finset (Beam n)} (hS : Supp S)
    (hz : ∀ i j, zBeam i j ∉ S) {k j : Fin n} (h : xBeam j k ∈ S) (j' : Fin n) :
    xBeam j' k ∈ S :=
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp, h
theorem Usa2020P2.fill_yBeam_x A yBeam in a cube without zBeams fills its whole column along x line 250 source
Source documentation
A yBeam in a cube without zBeams fills its whole column along x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.zBeam, Usa2020P2.Beam.yBeam
Proof uses: Usa2020P2.fill1d, Or, Eq, OfNat.ofNat, Exists, And, HAdd.hAdd, Usa2020P2.Beam.xBeam, Usa2020P2.ySupp, And.left, Usa2020P2.zSupp, And.right, Usa2020P2.xSupp, And.intro, Or.inl, Or.inr, Exists.intro, absurd
11 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem fill_yBeam_x {n : ℕ} {S : Finset (Beam n)} (hS : Supp S)
    (hz : ∀ i j, zBeam i j ∉ S) {i k : Fin n} (h : yBeam i k ∈ S) (i' : Fin n) :
    yBeam i' k ∈ S :=
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp, h
theorem Usa2020P2.fill_yBeam_z A yBeam in a cube without xBeams fills its whole column along z line 268 source
Source documentation
A yBeam in a cube without xBeams fills its whole column along z.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.xBeam, Usa2020P2.Beam.yBeam
Proof uses: Usa2020P2.fill1d, Or, Eq, OfNat.ofNat, Exists, And, HAdd.hAdd, Usa2020P2.Beam.zBeam, Usa2020P2.ySupp, And.left, Usa2020P2.zSupp, And.right, Usa2020P2.xSupp, And.intro, Or.inl, Or.inr, Exists.intro, absurd
11 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem fill_yBeam_z {n : ℕ} {S : Finset (Beam n)} (hS : Supp S)
    (hx : ∀ j k, xBeam j k ∉ S) {i k : Fin n} (h : yBeam i k ∈ S) (k' : Fin n) :
    yBeam i k' ∈ S :=
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp, h
theorem Usa2020P2.fill_xBeam_z An xBeam in a cube without yBeams fills its whole row along z line 286 source
Source documentation
An xBeam in a cube without yBeams fills its whole row along z.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.yBeam, Usa2020P2.Beam.xBeam
Proof uses: Usa2020P2.fill1d, Or, Eq, OfNat.ofNat, Exists, And, HAdd.hAdd, Usa2020P2.Beam.zBeam, Usa2020P2.xSupp, And.left, Usa2020P2.ySupp, Usa2020P2.zSupp, And.intro, Or.inl, Or.inr, Exists.intro, absurd
11 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem fill_xBeam_z {n : ℕ} {S : Finset (Beam n)} (hS : Supp S)
    (hy : ∀ i k, yBeam i k ∉ S) {j k : Fin n} (h : xBeam j k ∈ S) (k' : Fin n) :
    xBeam j k' ∈ S :=
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp, h
theorem Usa2020P2.fill_zBeam_x A zBeam in a cube without yBeams fills its whole row along x line 304 source
Source documentation
A zBeam in a cube without yBeams fills its whole row along x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.yBeam, Usa2020P2.Beam.zBeam
Proof uses: Usa2020P2.fill1d, Or, Eq, OfNat.ofNat, Exists, And, HAdd.hAdd, Usa2020P2.Beam.xBeam, Usa2020P2.zSupp, And.right, Usa2020P2.ySupp, Usa2020P2.xSupp, And.intro, Or.inl, Or.inr, Exists.intro, absurd
11 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem fill_zBeam_x {n : ℕ} {S : Finset (Beam n)} (hS : Supp S)
    (hy : ∀ i k, yBeam i k ∉ S) {i j : Fin n} (h : zBeam i j ∈ S) (i' : Fin n) :
    zBeam i' j ∈ S :=
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp, h
theorem Usa2020P2.fill_zBeam_y A zBeam in a cube without xBeams fills its whole row along y line 322 source
Source documentation
A zBeam in a cube without xBeams fills its whole row along y.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.xBeam, Usa2020P2.Beam.zBeam
Proof uses: Usa2020P2.fill1d, Or, Eq, OfNat.ofNat, Exists, And, HAdd.hAdd, Usa2020P2.Beam.yBeam, Usa2020P2.zSupp, And.right, Usa2020P2.ySupp, Usa2020P2.xSupp, And.intro, Or.inl, Or.inr, Exists.intro, absurd
11 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem fill_zBeam_y {n : ℕ} {S : Finset (Beam n)} (hS : Supp S)
    (hx : ∀ j k, xBeam j k ∉ S) {i j : Fin n} (h : zBeam i j ∈ S) (j' : Fin n) :
    zBeam i j' ∈ S :=
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp, h
def Usa2020P2.zFull Layer k (in the z-direction) is completely filled line 340 source
Source documentation
Layer k (in the z-direction) is completely filled.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Fin
Proof uses: Or, Membership.mem, Usa2020P2.Beam.xBeam, Usa2020P2.Beam.yBeam
2 instances, coercions and auxiliary constants left out.
```
def zFull (S : Finset (Beam n)) (k : Fin n) : Prop :=
…
```
Mentions: S, Usa2020P2.Beam
def Usa2020P2.xFull Layer i (in the x-direction) is completely filled line 344 source
Source documentation
Layer i (in the x-direction) is completely filled.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Fin
Proof uses: Or, Membership.mem, Usa2020P2.Beam.yBeam, Usa2020P2.Beam.zBeam
2 instances, coercions and auxiliary constants left out.
```
def xFull (S : Finset (Beam n)) (i : Fin n) : Prop :=
…
```
Mentions: S, Usa2020P2.Beam
def Usa2020P2.yFull Layer j (in the y-direction) is completely filled line 348 source
Source documentation
Layer j (in the y-direction) is completely filled.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Fin
Proof uses: Or, Membership.mem, Usa2020P2.Beam.xBeam, Usa2020P2.Beam.zBeam
2 instances, coercions and auxiliary constants left out.
```
def yFull (S : Finset (Beam n)) (j : Fin n) : Prop :=
…
```
Mentions: S, Usa2020P2.Beam
theorem Usa2020P2.zFull_of_mem line 351 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.zBeam, Usa2020P2.zFull, Usa2020P2.zLayer
Proof uses: Eq, Usa2020P2.Beam.xBeam, Or.inl, Usa2020P2.Beam.yBeam, Usa2020P2.fill_xBeam_y, Eq.symm, Or.inr, Usa2020P2.fill_yBeam_x, absurd, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.xFull_of_mem line 358 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.xBeam, Usa2020P2.xFull, Usa2020P2.xLayer
Proof uses: Eq, absurd, Eq.symm, Usa2020P2.Beam.yBeam, Or.inl, Usa2020P2.Beam.zBeam, Usa2020P2.fill_yBeam_z, Or.inr, Usa2020P2.fill_zBeam_y, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.yFull_of_mem line 365 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.yBeam, Usa2020P2.yFull, Usa2020P2.yLayer
Proof uses: Eq, Usa2020P2.Beam.xBeam, Or.inl, Usa2020P2.Beam.zBeam, Usa2020P2.fill_xBeam_z, Eq.symm, absurd, Or.inr, Usa2020P2.fill_zBeam_x, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.zFull_step line 372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.zBeam, Usa2020P2.zFull, And, Or, Eq, Exists, HAdd.hAdd
Proof uses: Usa2020P2.Beam.xBeam, Fin.mk, Usa2020P2.Beam.yBeam, Usa2020P2.xSupp, And.left, Usa2020P2.ySupp, Usa2020P2.zSupp, And.intro, Or.inl, Or.inr, Exists.intro, Usa2020P2.fill_xBeam_y, Usa2020P2.fill_yBeam_x, And.right
17 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.xFull_step line 398 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.xBeam, Usa2020P2.xFull, And, Or, Eq, Exists, HAdd.hAdd
Proof uses: Usa2020P2.Beam.yBeam, Fin.mk, Usa2020P2.Beam.zBeam, Usa2020P2.ySupp, And.left, Usa2020P2.zSupp, And.right, Usa2020P2.xSupp, And.intro, Or.inl, Or.inr, Exists.intro, Usa2020P2.fill_yBeam_z, Usa2020P2.fill_zBeam_y
17 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.yFull_step line 424 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.yBeam, Usa2020P2.yFull, And, Or, Eq, Exists, HAdd.hAdd
Proof uses: Usa2020P2.Beam.xBeam, Fin.mk, Usa2020P2.Beam.zBeam, Usa2020P2.xSupp, And.left, Usa2020P2.ySupp, Usa2020P2.zSupp, And.intro, Or.inl, Or.inr, Exists.intro, Usa2020P2.fill_xBeam_z, Usa2020P2.fill_zBeam_x, And.right
17 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.zFull_all line 450 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.zBeam, Finset.Nonempty, Usa2020P2.zFull
Proof uses: Usa2020P2.fill1d, Usa2020P2.zFull_step, Usa2020P2.zLayer, Usa2020P2.zFull_of_mem
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.xFull_all line 456 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.xBeam, Finset.Nonempty, Usa2020P2.xFull
Proof uses: Usa2020P2.fill1d, Usa2020P2.xFull_step, Usa2020P2.xLayer, Usa2020P2.xFull_of_mem
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.yFull_all line 462 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.yBeam, Finset.Nonempty, Usa2020P2.yFull
Proof uses: Usa2020P2.fill1d, Usa2020P2.yFull_step, Usa2020P2.yLayer, Usa2020P2.yFull_of_mem
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.card_zLayer line 468 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Fin, Not, Membership.mem, Usa2020P2.Beam.zBeam, Usa2020P2.zFull, LE.le, Finset.card, Finset.filter, Eq, Usa2020P2.zLayer
Proof uses: dite, Usa2020P2.Beam.xBeam, Finset.image, Finset.univ, And, Exists, Eq.mp, congrArg, propext, Finset.mem_image, Eq.mpr, id, Finset.mem_filter, And.intro, rfl, Trans.trans, Finset.card_image_of_injOn, Set, And.left, Usa2020P2.Beam.xBeam.inj and 10 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.card_xLayer line 499 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Fin, Not, Membership.mem, Usa2020P2.Beam.xBeam, Usa2020P2.xFull, LE.le, Finset.card, Finset.filter, Eq, Usa2020P2.xLayer
Proof uses: dite, Usa2020P2.Beam.yBeam, Finset.image, Finset.univ, And, Exists, Eq.mp, congrArg, propext, Finset.mem_image, Eq.mpr, id, Finset.mem_filter, And.intro, rfl, Trans.trans, Finset.card_image_of_injOn, Set, And.right, Usa2020P2.Beam.yBeam.inj and 10 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.card_yLayer line 530 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Fin, Not, Membership.mem, Usa2020P2.Beam.yBeam, Usa2020P2.yFull, LE.le, Finset.card, Finset.filter, Eq, Usa2020P2.yLayer
Proof uses: dite, Usa2020P2.Beam.xBeam, Finset.image, Finset.univ, And, Exists, Eq.mp, congrArg, propext, Finset.mem_image, Eq.mpr, id, Finset.mem_filter, And.intro, rfl, Trans.trans, Finset.card_image_of_injOn, Set, And.right, Usa2020P2.Beam.xBeam.inj and 11 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.card_ge_sq_of_no_zBeam If there are no zBeams, every layer is filled and n² ≤ S.card line 562 source
Source documentation
If there are no zBeams, every layer is filled and n² ≤ S.card.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.zBeam, Finset.Nonempty, LE.le, HMul.hMul, Finset.card
Proof uses: Usa2020P2.zFull, Usa2020P2.zFull_all, Eq.mpr, Finset.sum, Finset.univ, Finset.filter, Eq, Usa2020P2.zLayer, id, congrArg, Finset.card_eq_sum_card_fiberwise, Set, Finset.mem_univ, of_eq_true, Eq.trans, True, congrFun', HSMul.hSMul, Finset.sum_const, Fintype.card_fin and 4 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem card_ge_sq_of_no_zBeam {n : ℕ} (hn : 0 < n) {S : Finset (Beam n)} (hS : Supp S)
    (hz : ∀ i j, zBeam i j ∉ S) (hne : S.Nonempty) : n * n ≤ S.card := by
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp
theorem Usa2020P2.card_ge_sq_of_no_xBeam If there are no xBeams, every layer is filled and n² ≤ S.card line 573 source
Source documentation
If there are no xBeams, every layer is filled and n² ≤ S.card.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.xBeam, Finset.Nonempty, LE.le, HMul.hMul, Finset.card
Proof uses: Usa2020P2.xFull, Usa2020P2.xFull_all, Eq.mpr, Finset.sum, Finset.univ, Finset.filter, Eq, Usa2020P2.xLayer, id, congrArg, Finset.card_eq_sum_card_fiberwise, Set, Finset.mem_univ, of_eq_true, Eq.trans, True, congrFun', HSMul.hSMul, Finset.sum_const, Fintype.card_fin and 4 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem card_ge_sq_of_no_xBeam {n : ℕ} (hn : 0 < n) {S : Finset (Beam n)} (hS : Supp S)
    (hx : ∀ j k, xBeam j k ∉ S) (hne : S.Nonempty) : n * n ≤ S.card := by
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp
theorem Usa2020P2.card_ge_sq_of_no_yBeam If there are no yBeams, every layer is filled and n² ≤ S.card line 584 source
Source documentation
If there are no yBeams, every layer is filled and n² ≤ S.card.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Fin, Not, Membership.mem, Usa2020P2.Beam.yBeam, Finset.Nonempty, LE.le, HMul.hMul, Finset.card
Proof uses: Usa2020P2.yFull, Usa2020P2.yFull_all, Eq.mpr, Finset.sum, Finset.univ, Finset.filter, Eq, Usa2020P2.yLayer, id, congrArg, Finset.card_eq_sum_card_fiberwise, Set, Finset.mem_univ, of_eq_true, Eq.trans, True, congrFun', HSMul.hSMul, Finset.sum_const, Fintype.card_fin and 4 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem card_ge_sq_of_no_yBeam {n : ℕ} (hn : 0 < n) {S : Finset (Beam n)} (hS : Supp S)
    (hy : ∀ i k, yBeam i k ∉ S) (hne : S.Nonempty) : n * n ≤ S.card := by
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp
theorem Usa2020P2.card_filter_ne_z line 594 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Eq, Finset.card, Finset.filter, Ne, Usa2020P2.Dir, Usa2020P2.Beam.dir, Usa2020P2.Dir.Z, HAdd.hAdd, Usa2020P2.Dir.X, Usa2020P2.Dir.Y
Proof uses: Disjoint, Eq.mpr, Membership.mem, Not, id, congrArg, propext, Finset.disjoint_left, absurd, False, And.right, Eq.mp, And, Finset.mem_filter, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, Union.union and 22 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.card_filter_ne_x line 610 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Eq, Finset.card, Finset.filter, Ne, Usa2020P2.Dir, Usa2020P2.Beam.dir, Usa2020P2.Dir.X, HAdd.hAdd, Usa2020P2.Dir.Y, Usa2020P2.Dir.Z
Proof uses: Disjoint, Eq.mpr, Membership.mem, Not, id, congrArg, propext, Finset.disjoint_left, absurd, False, And.right, Eq.mp, And, Finset.mem_filter, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, Union.union and 22 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.card_filter_ne_y line 626 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Eq, Finset.card, Finset.filter, Ne, Usa2020P2.Dir, Usa2020P2.Beam.dir, Usa2020P2.Dir.Y, HAdd.hAdd, Usa2020P2.Dir.Z, Usa2020P2.Dir.X
Proof uses: Disjoint, Eq.mpr, Membership.mem, Not, id, congrArg, propext, Finset.disjoint_left, absurd, False, And.right, Eq.mp, And, Finset.mem_filter, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, Union.union and 22 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.n_le_of_mem_nonZ If some beam is not a zBeam, every z-layer contains an xBeam or a yBeam, hence n ≤ Nx + Ny line 644 source
Source documentation
If some beam is not a zBeam, every z-layer contains an xBeam or a yBeam, hence n ≤ Nx + Ny.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Exists, And, Membership.mem, Ne, Usa2020P2.Dir, Usa2020P2.Beam.dir, Usa2020P2.Dir.Z, LE.le, HAdd.hAdd, Finset.card, Finset.filter, Eq, Usa2020P2.Dir.X, Usa2020P2.Dir.Y
Proof uses: Fin, Usa2020P2.zLayer, Or, Usa2020P2.Beam.xBeam, id, Usa2020P2.Beam.zBeam, Usa2020P2.Beam.yBeam, Usa2020P2.xSupp, And.left, Usa2020P2.ySupp, Usa2020P2.zSupp, And.intro, Or.inl, Or.inr, Exists.intro, of_eq_true, Not, Eq.trans, False, True and 33 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 65 steps
Open to load the checked before-and-after goal states.
```
theorem n_le_of_mem_nonZ {n : ℕ} (_hn : 0 < n) {S : Finset (Beam n)} (hS : Supp S)
    (hxy : ∃ b ∈ S, b.dir ≠ .Z) :
    n ≤ (S.filter fun b => b.dir = .X).card + (S.filter fun b => b.dir = .Y).card := by
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp
theorem Usa2020P2.n_le_of_mem_nonX If some beam is not an xBeam, every x-layer contains a yBeam or a zBeam, hence n ≤ Ny + Nz line 698 source
Source documentation
If some beam is not an xBeam, every x-layer contains a yBeam or a zBeam, hence n ≤ Ny + Nz.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Exists, And, Membership.mem, Ne, Usa2020P2.Dir, Usa2020P2.Beam.dir, Usa2020P2.Dir.X, LE.le, HAdd.hAdd, Finset.card, Finset.filter, Eq, Usa2020P2.Dir.Y, Usa2020P2.Dir.Z
Proof uses: Fin, Usa2020P2.xLayer, Or, Usa2020P2.Beam.xBeam, absurd, rfl, Eq.symm, Usa2020P2.Beam.yBeam, id, Usa2020P2.Beam.zBeam, Usa2020P2.ySupp, And.left, Usa2020P2.zSupp, And.right, Usa2020P2.xSupp, And.intro, Or.inl, Or.inr, Exists.intro, of_eq_true and 33 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 65 steps
Open to load the checked before-and-after goal states.
```
theorem n_le_of_mem_nonX {n : ℕ} (_hn : 0 < n) {S : Finset (Beam n)} (hS : Supp S)
    (hxy : ∃ b ∈ S, b.dir ≠ .X) :
    n ≤ (S.filter fun b => b.dir = .Y).card + (S.filter fun b => b.dir = .Z).card := by
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp
theorem Usa2020P2.n_le_of_mem_nonY If some beam is not a yBeam, every y-layer contains a zBeam or an xBeam, hence n ≤ Nz + Nx line 752 source
Source documentation
If some beam is not a yBeam, every y-layer contains a zBeam or an xBeam, hence n ≤ Nz + Nx.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Exists, And, Membership.mem, Ne, Usa2020P2.Dir, Usa2020P2.Beam.dir, Usa2020P2.Dir.Y, LE.le, HAdd.hAdd, Finset.card, Finset.filter, Eq, Usa2020P2.Dir.Z, Usa2020P2.Dir.X
Proof uses: Fin, Usa2020P2.yLayer, Or, Usa2020P2.Beam.xBeam, id, Usa2020P2.Beam.zBeam, Usa2020P2.Beam.yBeam, Usa2020P2.xSupp, And.left, Usa2020P2.ySupp, Usa2020P2.zSupp, And.intro, Or.inl, Or.inr, Exists.intro, of_eq_true, Not, Eq.trans, False, True and 33 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 65 steps
Open to load the checked before-and-after goal states.
```
theorem n_le_of_mem_nonY {n : ℕ} (_hn : 0 < n) {S : Finset (Beam n)} (hS : Supp S)
    (hxy : ∃ b ∈ S, b.dir ≠ .Y) :
    n ≤ (S.filter fun b => b.dir = .Z).card + (S.filter fun b => b.dir = .X).card := by
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp
theorem Usa2020P2.card_eq_sum_dirs line 804 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa2020P2.Beam, Eq, Finset.card, HAdd.hAdd, Finset.filter, Usa2020P2.Dir, Usa2020P2.Beam.dir, Usa2020P2.Dir.X, Usa2020P2.Dir.Y, Usa2020P2.Dir.Z
Proof uses: Disjoint, Eq.mpr, Membership.mem, Not, id, congrArg, propext, Finset.disjoint_left, absurd, False, And.right, Eq.mp, And, Finset.mem_filter, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl, Union.union and 19 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.lower_bound The lower bound: any supported nonempty configuration has 3 * n ≤ 2 * S.card line 834 source
Source documentation
The lower bound: any supported nonempty configuration has 3 * n ≤ 2 * S.card.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Finset, Usa2020P2.Beam, Usa2020P2.Supp, Finset.Nonempty, HMul.hMul, Finset.card
Proof uses: LT.lt, Nat.mul_le_mul, le_rfl, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne and 93 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
theorem lower_bound {n : ℕ} (hn : 2 ≤ n) {S : Finset (Beam n)} (hS : Supp S)
    (hne : S.Nonempty) : 3 * n ≤ 2 * S.card := by
…
```
Mentions: S, Usa2020P2.Beam, Usa2020P2.Supp
def Usa2020P2.zPart The zBeams of the construction: (2t, 2t) for t = 0, …, 1009 line 864 source
Source documentation
The zBeams of the construction: (2t, 2t) for t = 0, …, 1009.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa2020P2.Beam, OfNat.ofNat, Nat
Proof uses: Finset.image, Subtype, Membership.mem, Finset.range, Usa2020P2.Beam.zBeam, Fin.mk, HMul.hMul, Finset.attach
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def zPart : Finset (Beam 2020) :=
…
```
Mentions: Usa2020P2.Beam
def Usa2020P2.yPart The yBeams of the construction: (2t+1, 2t) for t = 0, …, 1009 line 870 source
Source documentation
The yBeams of the construction: (2t+1, 2t) for t = 0, …, 1009.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa2020P2.Beam, OfNat.ofNat, Nat
Proof uses: Finset.image, Subtype, Membership.mem, Finset.range, Usa2020P2.Beam.yBeam, Fin.mk, HAdd.hAdd, HMul.hMul, Finset.attach
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def yPart : Finset (Beam 2020) :=
…
```
Mentions: Usa2020P2.Beam
def Usa2020P2.xPart The xBeams of the construction: (2t+1, 2t+1) for t = 0, …, 1009 line 876 source
Source documentation
The xBeams of the construction: (2t+1, 2t+1) for t = 0, …, 1009.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa2020P2.Beam, OfNat.ofNat, Nat
Proof uses: Finset.image, Subtype, Membership.mem, Finset.range, Usa2020P2.Beam.xBeam, Fin.mk, HAdd.hAdd, HMul.hMul, Finset.attach
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def xPart : Finset (Beam 2020) :=
…
```
Mentions: Usa2020P2.Beam
def Usa2020P2.halfBeams The construction: 3030 beams forming a staircase line 882 source
Source documentation
The construction: 3030 beams forming a staircase.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa2020P2.Beam, OfNat.ofNat, Nat
Proof uses: Union.union, Usa2020P2.zPart, Usa2020P2.yPart, Usa2020P2.xPart
4 instances, coercions and auxiliary constants left out.
```
def halfBeams : Finset (Beam 2020) := zPart ∪ yPart ∪ xPart
```
Mentions: Usa2020P2.Beam, Usa2020P2.zPart, Usa2020P2.yPart, Usa2020P2.xPart
theorem Usa2020P2.mem_zPart line 886 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Membership.mem, Usa2020P2.Beam, Finset, Usa2020P2.zPart, Usa2020P2.Beam.zBeam, Fin.mk, HMul.hMul
Proof uses: Eq.mpr, Finset.image, Subtype, Finset.range, Finset.attach, id, Eq, congrArg, Usa2020P2.zPart.eq_1, Exists, And, propext, Finset.mem_image, Exists.intro, Subtype.mk, Iff.mpr, Finset.mem_range, And.intro, of_eq_true, rfl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.mem_yPart line 891 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Membership.mem, Usa2020P2.Beam, Finset, Usa2020P2.yPart, Usa2020P2.Beam.yBeam, Fin.mk, HAdd.hAdd, HMul.hMul
Proof uses: Eq.mpr, Finset.image, Subtype, Finset.range, Finset.attach, id, Eq, congrArg, Usa2020P2.yPart.eq_1, Exists, And, propext, Finset.mem_image, Exists.intro, Subtype.mk, Iff.mpr, Finset.mem_range, And.intro, of_eq_true, rfl
25 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.mem_xPart line 896 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Membership.mem, Usa2020P2.Beam, Finset, Usa2020P2.xPart, Usa2020P2.Beam.xBeam, Fin.mk, HAdd.hAdd, HMul.hMul
Proof uses: Eq.mpr, Finset.image, Subtype, Finset.range, Finset.attach, id, Eq, congrArg, Usa2020P2.xPart.eq_1, Exists, And, propext, Finset.mem_image, Exists.intro, Subtype.mk, Iff.mpr, Finset.mem_range, And.intro, of_eq_true, rfl
22 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.mem_halfBeams_z line 901 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Membership.mem, Usa2020P2.Beam, Finset, Usa2020P2.halfBeams, Usa2020P2.Beam.zBeam, Fin.mk, HMul.hMul
Proof uses: Eq.mpr, Union.union, Usa2020P2.zPart, Usa2020P2.yPart, Usa2020P2.xPart, id, Eq, congrArg, Usa2020P2.halfBeams.eq_1, Finset.mem_union_left, Usa2020P2.mem_zPart
16 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.mem_halfBeams_y line 908 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Membership.mem, Usa2020P2.Beam, Finset, Usa2020P2.halfBeams, Usa2020P2.Beam.yBeam, Fin.mk, HAdd.hAdd, HMul.hMul
Proof uses: Eq.mpr, Union.union, Usa2020P2.zPart, Usa2020P2.yPart, Usa2020P2.xPart, id, Eq, congrArg, Usa2020P2.halfBeams.eq_1, Finset.mem_union_left, Finset.mem_union_right, Usa2020P2.mem_yPart
22 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.mem_halfBeams_x line 915 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Membership.mem, Usa2020P2.Beam, Finset, Usa2020P2.halfBeams, Usa2020P2.Beam.xBeam, Fin.mk, HAdd.hAdd, HMul.hMul
Proof uses: Eq.mpr, Union.union, Usa2020P2.zPart, Usa2020P2.yPart, Usa2020P2.xPart, id, Eq, congrArg, Usa2020P2.halfBeams.eq_1, Finset.mem_union_right, Usa2020P2.mem_xPart
20 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.of_mem_halfBeams_z line 921 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Membership.mem, Usa2020P2.Beam, Finset, Usa2020P2.halfBeams, Usa2020P2.Beam.zBeam, Exists, And, LT.lt, Eq, HMul.hMul
Proof uses: Or, Usa2020P2.zPart, Usa2020P2.yPart, Usa2020P2.xPart, Eq.mp, Union.union, congrArg, propext, Finset.mem_union, Usa2020P2.halfBeams.eq_1, Subtype, Finset.range, Finset.attach, Fin.mk, Finset.image, Finset.mem_image, Usa2020P2.zPart.eq_1, HEq, Exists.intro, And.intro and 15 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.of_mem_halfBeams_y line 937 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Membership.mem, Usa2020P2.Beam, Finset, Usa2020P2.halfBeams, Usa2020P2.Beam.yBeam, Exists, And, LT.lt, Eq, HAdd.hAdd, HMul.hMul
Proof uses: Or, Usa2020P2.zPart, Usa2020P2.yPart, Usa2020P2.xPart, Eq.mp, Union.union, congrArg, propext, Finset.mem_union, Usa2020P2.halfBeams.eq_1, Subtype, Finset.range, Finset.attach, Usa2020P2.Beam.zBeam, Fin.mk, Finset.image, Finset.mem_image, Usa2020P2.zPart.eq_1, HEq, False.elim and 14 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.of_mem_halfBeams_x line 953 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Membership.mem, Usa2020P2.Beam, Finset, Usa2020P2.halfBeams, Usa2020P2.Beam.xBeam, Exists, And, LT.lt, Eq, HAdd.hAdd, HMul.hMul
Proof uses: Or, Usa2020P2.zPart, Usa2020P2.yPart, Usa2020P2.xPart, Eq.mp, Union.union, congrArg, propext, Finset.mem_union, Usa2020P2.halfBeams.eq_1, Subtype, Finset.range, Finset.attach, Usa2020P2.Beam.zBeam, Fin.mk, Finset.image, Finset.mem_image, Usa2020P2.zPart.eq_1, HEq, False.elim and 14 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.zPart_card line 971 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Usa2020P2.Beam, OfNat.ofNat, Usa2020P2.zPart
Proof uses: Eq.mpr, Finset.image, Subtype, Membership.mem, Finset, Finset.range, Usa2020P2.Beam.zBeam, Fin.mk, HMul.hMul, Finset.attach, id, congrArg, Usa2020P2.zPart.eq_1, Finset.card_image_of_injOn, Set, HEq, Fin, eq_of_heq, Subtype.ext, Finset.card_attach and 2 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.yPart_card line 978 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Usa2020P2.Beam, OfNat.ofNat, Usa2020P2.yPart
Proof uses: Eq.mpr, Finset.image, Subtype, Membership.mem, Finset, Finset.range, Usa2020P2.Beam.yBeam, Fin.mk, HAdd.hAdd, HMul.hMul, Finset.attach, id, congrArg, Usa2020P2.yPart.eq_1, Finset.card_image_of_injOn, Set, HEq, Fin, eq_of_heq, Subtype.ext and 3 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.xPart_card line 985 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Usa2020P2.Beam, OfNat.ofNat, Usa2020P2.xPart
Proof uses: Eq.mpr, Finset.image, Subtype, Membership.mem, Finset, Finset.range, Usa2020P2.Beam.xBeam, Fin.mk, HAdd.hAdd, HMul.hMul, Finset.attach, id, congrArg, Usa2020P2.xPart.eq_1, Finset.card_image_of_injOn, Set, HEq, Fin, eq_of_heq, Subtype.ext 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.
theorem Usa2020P2.halfBeams_card line 992 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Usa2020P2.Beam, OfNat.ofNat, Usa2020P2.halfBeams
Proof uses: Disjoint, Finset, Usa2020P2.zPart, Usa2020P2.yPart, Eq.mpr, Membership.mem, Not, id, congrArg, propext, Finset.disjoint_left, Subtype, Finset.range, And, Finset.attach, Usa2020P2.Beam.zBeam, Fin.mk, HMul.hMul, Exists, False and 25 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.halfBeams_nonempty line 1021 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset.Nonempty, Usa2020P2.Beam, OfNat.ofNat, Nat, Usa2020P2.halfBeams
Proof uses: Eq.mpr, LT.lt, Finset.card, id, Eq, congrArg, Eq.symm, propext, Finset.card_pos, Usa2020P2.halfBeams_card, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.halfBeams_disjoint line 1027 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2020P2.DisjointBeams, OfNat.ofNat, Nat, Usa2020P2.halfBeams
Proof uses: Usa2020P2.Beam, Membership.mem, Finset, Exists, Fin, And, Usa2020P2.Beam.covers, Eq, Or, Usa2020P2.zPart, Usa2020P2.yPart, Usa2020P2.xPart, Eq.mp, Union.union, congrArg, propext, Finset.mem_union, Usa2020P2.halfBeams.eq_1, Subtype, Finset.range and 18 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 88 steps
Open to load the checked before-and-after goal states.
theorem Usa2020P2.halfBeams_supp line 1115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2020P2.Supp, OfNat.ofNat, Nat, Usa2020P2.halfBeams
Proof uses: And.intro, Fin, Membership.mem, Usa2020P2.Beam, Finset, Usa2020P2.Beam.xBeam, Usa2020P2.xSupp, And, Usa2020P2.Beam.yBeam, Usa2020P2.ySupp, Usa2020P2.Beam.zBeam, Usa2020P2.zSupp, LT.lt, Eq, HAdd.hAdd, HMul.hMul, Exists, Usa2020P2.of_mem_halfBeams_x, Or, Or.inr and 13 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 127 steps
Open to load the checked before-and-after goal states.
determine Usa2020P2.solution line 1186 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Usa2020P2.usa2020_p2 line 1188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Exists, Finset, Usa2020P2.Beam, OfNat.ofNat, And, Finset.Nonempty, Usa2020P2.DisjointBeams, Usa2020P2.Supp, Eq, Finset.card, Usa2020P2.solution
Proof uses: And.intro, Membership.mem, Set, lowerBounds, Exists.intro, Usa2020P2.halfBeams, Usa2020P2.halfBeams_nonempty, Usa2020P2.halfBeams_disjoint, Usa2020P2.halfBeams_supp, Usa2020P2.halfBeams_card, LE.le, HMul.hMul, Usa2020P2.lower_bound, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, id, Eq.mpr and 3 more
17 instances, coercions and auxiliary constants left out.

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