fix(tactic/solve_by_elim): apply_assumption argument parsing (#15394)

The optional list of expressions to `apply_assumption` should be parsed interactively. This fixes a bug where `none` would have to be provided before a config object.



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

src/tactic/solve_by_elim.lean

@@ -273,13 +273,13 @@ Optional arguments:
   the next one will be attempted.
 -/
 meta def apply_assumption
-  (lemmas : option (list expr) := none)
+  (lemmas : parse pexpr_list?)
   (opt : apply_any_opt := {})
   (tac : tactic unit := skip) : tactic unit :=
 do
   lemmas ← match lemmas with
   | none := local_context
-  | some lemmas := return lemmas
+  | some lemmas := lemmas.mmap to_expr
   end,
   tactic.apply_any lemmas opt tac
 

test/solve_by_elim.lean

@@ -171,3 +171,7 @@ begin
   rintro ⟨n, hf | hg⟩,
   solve_by_elim* [or.inl, or.inr, Exists.intro] { max_depth := 20 },
 end
+
+-- Check that no list of arguments is needed when using a config object
+example (a : ℤ) (h : a = 2) : a = 2 :=
+by apply_assumption {use_exfalso := ff}