theorem Hex.GraphIso.Nauty.Sparse.Graph.rows_map {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) (vertices visits : List Nat) (hb : ∀ (v : Nat), v ∈ vertices → v < n) (hp : visits.Perm (List.map (renamingOf p).toFun vertices)) : (List.flatMap (ofGraph H).row visits).Perm (List.map (renamingOf p).toFun (List.flatMap (ofGraph G).row vertices))

Concatenating native rows transports the neighbour multiset even when both the splitter order and individual native row orders change.

theorem Hex.GraphIso.Nauty.Sparse.Graph.cell_rows_map {n first len level : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) {lab out ptn : Array Nat} (hp : lab.toList.Perm (List.range n)) (hb : first + len ≤ n) (hc : IsCell ptn level first len) (hperm : cellsPerm ptn level out (Array.map (renamingOf p).toFun lab)) : (List.flatMap (fun (q : Nat) => (ofGraph H).row out[q]!) (List.range' first len)).Perm (List.map (renamingOf p).toFun (List.flatMap (fun (q : Nat) => (ofGraph G).row lab[q]!) (List.range' first len)))

The native row sequence of a whole partition cell transports under renaming and arbitrary permutations within the original cells.