GeneralCustomTactics

This module provides general-purpose custom tactics for MRiscX.

def tacticSimpSetEq : Lean.ParserDescr

Simplify using the available set-equality hypotheses.

Equations

• tacticSimpSetEq = Lean.ParserDescr.node `tacticSimpSetEq 1024 (Lean.ParserDescr.nonReservedSymbol "simpSetEq" false)

def tacticApplyToLastGoal_ : Lean.ParserDescr

Run the given tactic sequence on the last goal only.

Equations

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

def tacticZeroLtNeZero : Lean.ParserDescr

Discharge a 0 < n goal by rewriting it as n ≠ 0.

Equations

• tacticZeroLtNeZero = Lean.ParserDescr.node `tacticZeroLtNeZero 1024 (Lean.ParserDescr.nonReservedSymbol "zeroLtNeZero" false)