feat: allow solve_by_elim to use projections of hypotheses

[kim-em]

This powers up solve_by_elim by allowing it to use projections of hypotheses. It does so by saturating the context with let-bindings for projections (recursively).

For interactive use of solve_by_elim, this is on by default, but not on by default for non-interactive use. There is a flag solve_by_elim (config := {letProjs := false}) to disable it.

As a simple example, this allows

example (x : P ∧ Q) : P := by
  solve_by_elim

which previously would fail.

It also powers up exact? (example from Mathlib):

example (p : ℕ) [Fact p.Prime] : 1 < p := by exact? says exact Nat.Prime.one_lt Fact.out

• [ ] depends on #582
• [ ] depends on #548

[kim-em]

I will check this against Mathlib.

[kim-em]

apply_rules should probably turn this off, as it is non-terminal.

[kim-em]

apply_rules should probably turn this off, as it is non-terminal.

Done.

[kim-em]

I will check this against Mathlib.

Mathlib reveals a nasty problem, which is that somehow we are now generating proofs with additional, unused, universe variables in them!

[kim-em]

Checking what this does to Mathlib in https://github.com/leanprover-community/mathlib4/pull/10266.