theorem Hex.GraphIso.Nauty.Sparse.matching_prepare {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} {targets : List Nat} {key : Key n} (hn : 0 < n) (hl : 1 ≤ level) (hnode : NodeInv G level numcells st) (hocc : Generation.HasLeaf G.graph tcLevel level (State.refined (Graph.ofGraph G.graph) level numcells st) targets key) (hm : Generation.Matches G.graph level st targets key) (heq : st.eqlevFirst = level - 1) (hnc : (State.refined (Graph.ofGraph G.graph) level numcells st).numcells < n) : have p := prepareOther (Graph.ofGraph G.graph) tcLevel level numcells st; classify (Graph.ofGraph G.graph) level p.fst p.snd.snd.snd.snd.snd = (Generic.Leaf.internal, p.snd.snd.snd.snd.snd) ∧ p.snd.snd.fst = st.firsttc[level]! ∧ (cheapCheck false level p.snd.snd.snd.snd.snd).eqlevFirst = level

A matching selected occurrence keeps the production comparison on the first reference and selects its stored target through the actual cached dispatch. The node need not be cheap or uniform.