feat(solve_by_elim): improve backtracking behaviour when there are mu…

…ltiple subgoals

tactic/basic.lean

@@ -423,10 +423,10 @@ meta def apply_assumption
   (asms : tactic (list expr) := local_context)
   (tac : tactic unit := skip) : tactic unit :=
 do { ctx ← asms,
-     ctx.any_of (λ H, () <$ symm_apply H; tac) } <|>
+     ctx.any_of (λ H, symm_apply H >> tac) } <|>
 do { exfalso,
      ctx ← asms,
-     ctx.any_of (λ H, () <$ symm_apply H; tac) }
+     ctx.any_of (λ H, symm_apply H >> tac) }
 <|> fail "assumption tactic failed"
 
 open nat
@@ -443,7 +443,8 @@ meta structure by_elim_opt :=
 meta def solve_by_elim (opt : by_elim_opt := { }) : tactic unit :=
 do
   tactic.fail_if_no_goals,
-  solve_by_elim_aux opt.discharger opt.assumptions opt.max_rep
+  focus1 $
+    solve_by_elim_aux opt.discharger opt.assumptions opt.max_rep
 
 meta def metavariables : tactic (list expr) :=
 do r ← result,

tests/solve_by_elim.lean

@@ -77,3 +77,17 @@ begin
   trivial
 end
 
+example {α : Type} (r : α → α → Prop) (f : α → α → α)
+  (l : ∀ a b c : α, r a b → r a (f b c) → r a c)
+  (a b c : α) (h₁ : r a b) (h₂ : r a (f b c)) : r a c :=
+begin
+  solve_by_elim,
+end
+
+-- Verifying that solve_by_elim behaves as expected in the presence of multiple goals.
+example (n : ℕ) : ℕ × ℕ :=
+begin
+  split,
+  solve_by_elim,
+  solve_by_elim
+end