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.
cf3e7de143