obviousFunext? — Mathlib

Lean4
/-- Try to apply `funext`, but only if it is an equality of two functions where at least one is
a lambda expression.

One thing this check prevents is accidentally applying `funext` to a set equality, but also when
doing congruence we don't want to apply `funext` unnecessarily.
-/
def obviousFunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
  mvarId.withContext <|
    observing? do
      let some (_, lhs, rhs) := (← withReducible mvarId.getType').eq? |
        failure
      if not lhs.cleanupAnnotations.isLambda && not rhs.cleanupAnnotations.isLambda then
        failure
      mvarId.apply (← mkConstWithFreshMVarLevels ``funext)
Похожие утверждения