A simple assertion command for Lean4.
Assert standard boolean (BEq) equality by using #assert TERM == TERM:
Assert equality with a custom predicate using #assert TERM == TERM via PRED:
Failed assertions are highlighted and show actual and expected values:
