Lean4
/-- `findCompLemma e` arranges `e` in the form `lhs R rhs`, where `R ∈ {<, ≤, =, ≠}`, and returns
`lhs`, `rhs`, the `cancel_factors` lemma corresponding to `R`, and a Boolean indicating whether
`R` involves the order (i.e. `<` and `≤`) or not (i.e. `=` and `≠`).
In the case of `LT`, `LE`, `GE`, and `GT` an order on the type is needed, in the last case
it is not, the final component of the return value tracks this.
-/
def findCompLemma (e : Expr) : MetaM (Option (Expr × Expr × Name × Bool)) := do
match (← whnfR e).getAppFnArgs with
| (``LT.lt, #[_, _, a, b]) =>
return (a, b, ``cancel_factors_lt, true)
| (``LE.le, #[_, _, a, b]) =>
return (a, b, ``cancel_factors_le, true)
| (``Eq, #[_, a, b]) =>
return
(a, b, ``cancel_factors_eq, false)
-- `a ≠ b` reduces to `¬ a = b` under `whnf`
| (``Not, #[p]) =>
match (← whnfR p).getAppFnArgs with
| (``Eq, #[_, a, b]) =>
return (a, b, ``cancel_factors_ne, false)
| _ =>
return none
| (``GE.ge, #[_, _, a, b]) =>
return (b, a, ``cancel_factors_le, true)
| (``GT.gt, #[_, _, a, b]) =>
return (b, a, ``cancel_factors_lt, true)
| _ =>
return none
