obviousHfunext? — Mathlib

Lean4
/-- Try to apply `Function.hfunext`, returning the new goals if it succeeds.
Like `Lean.MVarId.obviousFunext?`, we only do so if at least one side of the `HEq` is a lambda.
This prevents unfolding of things like `Set`.

Need to have `Mathlib/Logic/Function/Basic.lean` imported for this to succeed.
-/
def obviousHfunext? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
  mvarId.withContext <|
    observing? do
      let some (_, lhs, _, rhs) := (← withReducible mvarId.getType').heq? |
        failure
      if not lhs.cleanupAnnotations.isLambda && not rhs.cleanupAnnotations.isLambda then
        failure
      mvarId.apply (← mkConstWithFreshMVarLevels `Function.hfunext)
Похожие утверждения