theorem Hex.GraphIso.Aut.indiv_exists {n k : Nat} {G : Colored n k} {v : Fin n} (w : Fin n) (hne : w ≠ v) (hcolor : G.coloring.cells[w] = G.coloring.cells[v]) : ∃ (H : Colored n (k + 1)), indiv? G v = some H

Individualizing a vertex succeeds when its original colour cell contains another vertex.

theorem Hex.GraphIso.Aut.indiv_fields {n k : Nat} {G : Colored n k} {v : Fin n} {H : Colored n (k + 1)} (h : indiv? G v = some H) : H.graph = G.graph ∧ ∀ (u : Fin n), ↑H.coloring.cells[u] = if u = v then k else ↑G.coloring.cells[u]

The checked individualization keeps the graph and splits exactly the selected vertex into a new final colour.

theorem Hex.GraphIso.Aut.indiv_isIso {n k : Nat} {G : Colored n k} {v : Fin n} {H : Colored n (k + 1)} (h : indiv? G v = some H) (p : Perm n) : IsIso H H p ↔ IsIso G G p ∧ p.get v = v

Automorphisms after individualization are exactly the automorphisms of the original graph that fix the selected vertex.