mathlib

b977dbac - fix(solve_by_elim): handle multiple goals with different hypotheses (#4519)

fix(solve_by_elim): handle multiple goals with different hypotheses (#4519) Previously `solve_by_elim*` would operate on multiple goals (only succeeding if it could close all of them, and performing backtracking across goals), however it would incorrectly only use the local context from the main goal. If other goals had different sets of hypotheses, ... various bad things could happen! This PR arranges so that `solve_by_elim*` inspects the local context later, so it picks up the correct hypotheses. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>