partial def Hex.PermGroup.Mathlib.Tactic.setLitElems (s : Lean.Expr) : Lean.MetaM (Option (List Lean.Expr))

The elements of a set literal {a, b, …}, or of the coercion of a Finset literal.

def Hex.PermGroup.Mathlib.Tactic.permDegree (ty : Lean.Expr) : Lean.MetaM ℕ

The degree n of a type Equiv.Perm (Fin n), as a numeral.

Equations

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

inductive Hex.PermGroup.Mathlib.Tactic.GoalKind : Type

The shape of a supported goal.

• card (N : ℕ) : GoalKind
• mem (g : Lean.Expr) : GoalKind
• notMem (g : Lean.Expr) : GoalKind
• top : GoalKind

partial def Hex.PermGroup.Mathlib.Tactic.unfoldToClosure? (H : Lean.Expr) (fuel : ℕ := 32) : Lean.MetaM (Option Lean.Expr)

H unfolded until it is Subgroup.closure s, so that a subgroup given by a definition, such as def M : Subgroup _ := Subgroup.closure {a, b}, is recognised. Definitions are unfolded one at a time, and Subgroup.closure itself is never unfolded.

def Hex.PermGroup.Mathlib.Tactic.closureArg? (H : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

The generating set s when H is Subgroup.closure s, possibly behind definitions.

Equations

• Hex.PermGroup.Mathlib.Tactic.closureArg? H = do let __x ← Hex.PermGroup.Mathlib.Tactic.unfoldToClosure? H match __x with | some H' => pure (some (H'.getArg! 2)) | x => pure none

partial def Hex.PermGroup.Mathlib.Tactic.unfoldSetDefs (s : Lean.Expr) (fuel : ℕ := 32) : Lean.MetaM Lean.Expr

s with definitions unfolded until it is a set literal or a coerced Finset, so that a generating set such as def gens : Set _ := {a, b} is recognised.

def Hex.PermGroup.Mathlib.Tactic.unfoldClosures (goal : Lean.Expr) : Lean.MetaM Lean.Expr

The goal with every subgroup that unfolds to Subgroup.closure s replaced by that closure, and s unfolded to a literal. It is definitionally equal to the goal, and later steps rewrite s syntactically.

Equations

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

def Hex.PermGroup.Mathlib.Tactic.coeSortArg? (T : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

The subgroup H when the type T is ↥H, that is {x // x ∈ H}.

Equations

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

def Hex.PermGroup.Mathlib.Tactic.readGoal? (goal : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × GoalKind))

Match one of the four supported goals exactly, returning the generating set.

Equations

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

partial def Hex.PermGroup.Mathlib.Tactic.setOfListEq (permTy : Lean.Expr) : List Lean.Expr → Lean.MetaM Lean.Expr

A proof of {x | x ∈ [g₁, …, gₖ]} = {g₁, …, gₖ} built from the list lemmas, without traversing the elements.

def Hex.PermGroup.Mathlib.Tactic.rewriteSet (mvarId : Lean.MVarId) (s _gsList : Lean.Expr) (_gens : List Lean.Expr) (_permTy : Lean.Expr) : Lean.Elab.Tactic.TacticM Lean.MVarId

Compatibility normalization entry point for graph automorphism consumers.

Equations

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

partial def Hex.PermGroup.Mathlib.Tactic.setLitStx (stx : Lean.Syntax) : Option (Array Lean.Syntax)

The elements of a set-literal syntax {a, b, …}, possibly under a type ascription.

def Hex.PermGroup.Mathlib.Tactic.extension : Tactic.Extension

Translate Mathlib's goal, run the shared computational tactic and transport its conclusion through the correspondence theorems.

Equations

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