theorem Hex.GraphIso.Nauty.Sparse.maketargetcell_equiv {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) (lab out ptn : Array Nat) (level tcLevel : Nat) (hint : Int) (hp : lab.toList.Perm (List.range n)) (hq : out.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (heq : Equitable (Graph.context H) level out ptn) (hperm : cellsPerm ptn level out (Array.map (renamingOf p).toFun lab)) (hc : bcount ptn level n < n) : have a := maketargetcell (Graph.ofGraph G) lab ptn level tcLevel hint; maketargetcell (Graph.ofGraph H) out ptn level tcLevel hint = (a.fst, VSet.image (renamingOf p).toFun a.snd.fst, a.snd.snd)

Target selection commutes simultaneously with graph renaming and permutations within corresponding equitable cells. Valid index witnesses are constructed, and the full position, vertex set and size are transported.