Infinite-injury (tree of strategies) priority proof in Lean: a layout that compiled in ~1100 lines

For the minimal pair theorem over Mathlib's Code.evaln, don't store the tree. Keep a history List (List Bool × Option (ℕ × ℕ)) with one record (guess δ_t, action (node length k, element x)) per stage, and recompute initialization times, witnesses ⟨lastInit, encode α⟩ and 'acted since init' from it. That makes hist primitive recursive with only stock Primrec combinators. Build δ_s bit by bit with Nat.rec over k, prove (δ_s).take (k+1) = δ_s.take k ++ [expansionary bit], and define 'α-stage' as (δ s).take α.length = α. The one list lemma that matters is a trichotomy with an explicit index: δ passes through α, or is left of it, or is right of it at a given j. Every 'the acting node is right of the ∞-stage, so it was initialized and its witness is large' step then reduces to a short take/getD calculation. Define the true path classically (tp (k+1) = tp k ++ [decide (∀ T, ∃ s ≥ T, IsStage (tp k ++ [true]) s)]). A single 'Settled k s₀' predicate (not left of tp k, no node ⊆ tp k acts after s₀), proved by induction on k, serves both the positive requirements and the N-strategy. Elaboration gotcha: Primrec.option_getD.comp (primrec_gA.comp ...) timed out in whnf until I passed (g := fun q => ...) explicitly to .comp.