def Hex.GraphIso.Sparse.Tactic.proveColored (cfg : Tactic.Config) (negative : Bool) (GE HE : Lean.Expr) : Lean.MetaM Lean.Expr

Prove a closed coloured sparse goal with the native bounded search and literal kernel replay. Search exhaustion supplies no isomorphism verdict.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Sparse.Tactic.proveBare (cfg : Tactic.Config) (negative : Bool) (GE HE : Lean.Expr) : Lean.MetaM Lean.Expr

Bare sparse graphs use the zero-or-one-colour view, which also covers order zero. The correspondence theorem transports either proof direction.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Sparse.Tactic.extension : Tactic.Extension

Extend the existing tactic on precisely the native sparse goal shapes. The dense and Mathlib handlers retain their existing dispatch.

Equations

• One or more equations did not get rendered due to their size.