relImpRelLemma — Mathlib

Lean4
/-- Construct a `GCongrLemma` for `gcongr` goals of the form `a ≺ b → c ≺ d`.
This will be tried if there is no other available `@[gcongr]` lemma.
For example, the relation `a ≡ b [ZMOD n]` has an instance of `IsTrans`, so a congruence of the form
`a ≡ b [ZMOD n] → c ≡ d [ZMOD n]` can be solved with `rel_imp_rel`, `rel_trans` or `rel_trans'`.
-/
def relImpRelLemma (arity : Nat) : List GCongrLemma :=
  if arity < 2 then []
  else [{
        declName := ``rel_imp_rel
        mainSubgoals := #[(7, arity - 2, 0), (8, arity - 1, 0)]
        numHyps := 9
        key := default, prio := default, numVarying := default }]
Похожие утверждения