Semantics of "only" option of solve_by_elim

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

This is a request of changing the behavior of the "only" option to solve_by_elim in order to clarify the semantics, bring it in line with similar tactics in other systems (Coq/Matita/...) and make the tactic more useful.

solve_by_elim automatically introduces new hypotheses when proving implications/foralls. These new hypotheses are not automatically added to the set of "only" usable assumptions. Analogous tactics in every other system I am aware of have the opposite behavior, for good reasons that I explain here. First let's show an example

theorem iff_example: ∀A B: Prop, (A ↔ B) → (B ↔ A) := by
 intros A B U
 cases U
 case _ h1 h2 =>
  constructor
  . solve_by_elim [h2]             -- here it works without only
  . solve_by_elim only [h1]    -- but with only it does not work anymore

Reasons to change the semantics to always allow hypotheses introduced by the tactic itself:

1. [important] once solve_by_elim has found a proof using only lemmas l1 ... ln, with the new semantics "solve by elim only [l1,...,ln]" would be able to find the same proof reducing the search time. This is an important principle when reconstructing proofs found by hammers for example. However, as the example above shows, this is not the case with the current semantics
2. [minor] applications to didactics: "only" can be always automatically triggered (e.g. using a macro) to force students to list the lemmas that they think are necessary in a proof. However, as the example above shows, the current semantics does not allow that when (recursive) goals have implications

Context

See also the following conversation of Zulip

https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/solve_by_elim.20.3A.20.22only.22weirdness

Steps to Reproduce

1. check the code above

Expected behavior: both calls to solve_by_elim should solve the goal

Actual behavior: only the first does because the implementation of the tactic starts introducing an hypothesis "a : A" that is not added to the list of usable hypotheses

Versions

4.9.0-rc3

Start by running the minimal iff_example reproduction in Lean and compare the two solve_by_elim calls. Then inspect the solve_by_elim tactic implementation and its handling of hypotheses introduced during implication or forall goals. Done means solve_by_elim only [h1] also solves the second goal, with a regression test covering the behavior.