feat: let simp apply rules with higher-order patterns

[nomeata]

after this change, simp will be able to discharge side-goals that, after simplification, are of the form ∀ …, a = b with a =?= b.

Usually these side-goals are solved by simplification using eq_self, but that does not work when there are metavariables involved.

This enables us to have rewrite rules like

theorem List.foldl_subtype (p : α → Prop) (l : List (Subtype p)) (f : β → Subtype p → β)
  (g : β → α → β) (b : β)
  (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
  l.foldl f b = (l.map (·.val)).foldl g b := by

where the parameter g does not appear on the lhs, but can be solved for using the hf equation. See tests/lean/run/simpHigherOrder.lean for more examples.

The motivating use-case is that simp should be able to clean up the usual

  l.attach.map (fun <x, _> => x)

idiom often seen in well-founded recursive functions with nested recursion.

Care needs to be taken with adding such rules to the default simp set if the lhs is very general, and thus causes them to be tried everywhere.

Performance impact of just this PR (no additional simp rules) on mathlib is unsuspicious: http://speed.lean-fro.org/mathlib4/compare/b5bc44c7-e53c-4b6c-9184-bbfea54c4f80/to/ae1d769b-2ff2-4894-940c-042d5a698353

I tried a few alternatives, e.g. letting simp apply eq_self without bumping the mvar depth, or just solve equalities directly, but that broke too much things, and adding code to the default discharger seemed simpler.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5479 build failed against this PR. (2024-09-26 09:31:54) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5479 build failed against this PR. (2024-09-26 11:29:12) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-5479 build against this PR was cancelled. (2024-09-26 12:42:40) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5479 has successfully built against this PR. (2024-09-26 13:34:23) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5479 has successfully built against this PR. (2024-09-26 15:30:17) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5479 has successfully built against this PR. (2024-09-26 17:17:41) View Log