getContrLemma — Mathlib

Lean4
/-- If `e` is a comparison `a R b` or the negation of a comparison `¬ a R b`, found in the target,
`getContrLemma e` returns the name of a lemma that will change the goal to an
implication, along with the type of `a` and `b`.

For example, if `e` is `(a : ℕ) < b`, returns ``(`lt_of_not_ge, ℕ)``.
-/
def getContrLemma (e : Expr) : MetaM (Name × Expr) := do
  match ← e.ineqOrNotIneq? with
  | (true, Ineq.lt, t, _) =>
    pure (``lt_of_not_ge, t)
  | (true, Ineq.le, t, _) =>
    pure (``le_of_not_gt, t)
  | (true, Ineq.eq, t, _) =>
    pure (``eq_of_not_lt_of_not_gt, t)
  | (false, _, t, _) =>
    pure (``Not.intro, t)
Похожие утверждения