structure HexGraphIsoMathlib.Tactic.Shape : Type

A supported goal, as read off the target.

• G : Lean.Expr

  The left-hand graph.

• H : Lean.Expr

  The right-hand graph.

• colored : Bool

  Whether the goal is about Colored graphs rather than bare SimpleGraphs.

• negative : Bool

  Whether the goal refutes isomorphism.

• wrap : Bool

  Whether a positive goal asks for the Nonempty/Isomorphic wrapper around the isomorphism.

• useNot : Bool

  For negatives: build ¬ · (true) or IsEmpty · (false).

def HexGraphIsoMathlib.Tactic.matchIsoType? (t : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Match a SimpleGraph isomorphism type G ≃g H.

Equations

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

def HexGraphIsoMathlib.Tactic.matchColoredIso? (t : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Match a Colored.Iso type.

Equations

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

def HexGraphIsoMathlib.Tactic.matchColoredIsomorphic? (t : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Match a Colored.Isomorphic proposition.

Equations

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

def HexGraphIsoMathlib.Tactic.parseGoal? (target : Lean.Expr) : Lean.MetaM (Option Shape)

The shape of the goal, or none when the target is not one of the supported shapes.

Equations

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

def HexGraphIsoMathlib.Tactic.vertexType (colored : Bool) (g : Lean.Expr) : Lean.MetaM Lean.Expr

The vertex type of a graph expression (SimpleGraph V or Colored V k).

Equations

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

structure HexGraphIsoMathlib.Tactic.Side : Type

Elaboration data for one side of the goal.

• V : Lean.Expr

  The vertex type.

• instV : Lean.Expr

  The Fintype V instance.

• cardTerm : Lean.Expr

  The term Fintype.card V.

• card : ℕ

  The value of Fintype.card V.

• equiv : Lean.Expr

  The enumeration V ≃ Fin (Fintype.card V), a listEquiv application on a literal element list.

def HexGraphIsoMathlib.Tactic.mkSide (colored : Bool) (g : Lean.Expr) : Lean.MetaM Side

Collect the elaboration data for one side: its vertex type, the Fintype instance, the cardinality, and the enumeration equivalence built from the reduced Finset.univ.val. A vertex type with no Fintype or DecidableEq instance, or one whose enumeration does not reduce to a literal list, is reported here.

Equations

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

def HexGraphIsoMathlib.Tactic.applyTrailingInstances (e : Lean.Expr) : Lean.MetaM Lean.Expr

Synthesize any trailing instance-implicit arguments left unapplied by mkAppM.

Equations

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

def HexGraphIsoMathlib.Tactic.encodeSide (colored : Bool) (g : Lean.Expr) (side : Side) : Lean.MetaM (Lean.Expr × Option Lean.Expr)

The encoded executable graph term for one side, together with the 0 < card proof for uncoloured sides.

Equations

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

def HexGraphIsoMathlib.Tactic.proveShape (cfg : Hex.GraphIso.Tactic.Config) (target : Lean.Expr) (shape : Shape) : Lean.MetaM Lean.Expr

The proof term for a parsed goal. When the goal does not hold, or a logical limit runs out, this fails with a message saying which.

Equations

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

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

The graph_iso extension for SimpleGraph goals.

Equations

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