Tactic for Commute

This tactic uses aesop to discharge goals relating to the Commute relation. It mostly tries to do straightforward recursion on expressions, along with some basic normalization of ring operations.

def commutesTac : Lean.ParserDescr

A tactic for proving goals of the Commute relation.

You can use commutes? to get a corresponding proof script.

Equations

• commutesTac = Lean.ParserDescr.node `commutesTac 1024 (Lean.ParserDescr.nonReservedSymbol "commutes" false)

def commutesTac? : Lean.ParserDescr

A variant of the commutes tactic for proving Commute goals that produces a proof script.

Equations

• commutesTac? = Lean.ParserDescr.node `commutesTac? 1024 (Lean.ParserDescr.nonReservedSymbol "commutes?" false)