SimpLte Tactic

Try to prove goals like LT.lt or LE.le from local declarations of type LT.lt, LE.le, EQ, And or Subtype using Nat theorems.

instance SimpLte.instReprFunType : Repr SimpLte.FunType✝

Equations

• SimpLte.instReprFunType = { reprPrec := SimpLte.reprFunType✝ }

instance SimpLte.instBEqFunType : BEq SimpLte.FunType✝

Equations

• SimpLte.instBEqFunType = { beq := SimpLte.beqFunType✝ }

def SimpLte.renameShadowed (mvarId : Lean.MVarId) : Lean.Elab.Tactic.TacticM Lean.MVarId

rename decls with same name, see Lean.Elab.Tactic.renameInaccessibles.

Equations

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

def SimpLte.tacticSimp_lte? : Lean.ParserDescr

Show proof of goals like LT.lt or LE.le from local declarations of type LT.lt, LE.le or EQ using Nat theorems.

Equations

• SimpLte.tacticSimp_lte? = Lean.ParserDescr.node `SimpLte.tacticSimp_lte? 1024 (Lean.ParserDescr.nonReservedSymbol "simp_lte?" false)

def SimpLte.tacticSimp_lte : Lean.ParserDescr

try to prove goals like LT.lt or LE.le from local declarations of type LT.lt, LE.le or EQ using Nat theorems.

Equations

• SimpLte.tacticSimp_lte = Lean.ParserDescr.node `SimpLte.tacticSimp_lte 1024 (Lean.ParserDescr.nonReservedSymbol "simp_lte" false)