Builds a collection of lemmas for use in the backtracking search in solve_by_elim.

• By default, it includes all local hypotheses, along with rfl, trivial, congr_fun and congr_arg.
• The flag no_dflt removes these.
• The argument hs is a list of simp_arg_types, and can be used to add, or remove, lemmas or expressions from the set.
• The argument attr : list name adds all lemmas tagged with one of a specified list of attributes.

The internal implementation of solve_by_elim, with a limiting counter.

Configuration options for solve_by_elim.

• By default solve_by_elim operates only on the first goal, but with backtrack_all_goals := true, it operates on all goals at once, backtracking across goals as needed, and only succeeds if it dischargers all goals.
• discharger specifies a tactic to try discharge subgoals (this is only attempted on subgoals for which no lemma applies successfully).
• assumptions generates the list of lemmas to use in the backtracking search.
• max_rep bounds the depth of the search.

solve_by_elim repeatedly tries applying a lemma from the list of assumptions (passed via the by_elim_opt argument), recursively operating on any generated subgoals. It succeeds only if it discharges the first goal (or with backtrack_all_goals := tt, if it discharges all goals.)

apply_assumption looks for an assumption of the form ... → ∀ _, ... → head where head matches the current goal.

alternatively, when encountering an assumption of the form sg₀ → ¬ sg₁, after the main approach failed, the goal is dismissed and sg₀ and sg₁ are made into the new goal.

optional arguments:

• asms: list of rules to consider instead of the local constants
• tac: a tactic to run on each subgoals after applying an assumption; if this tactic fails, the corresponding assumption will be rejected and the next one will be attempted.

solve_by_elim calls apply on the main goal to find an assumption whose head matches and then repeatedly calls apply on the generated subgoals until no subgoals remain, performing at most max_rep recursive steps.

solve_by_elim discharges the current goal or fails.

solve_by_elim performs back-tracking if apply_assumption chooses an unproductive assumption.

By default, the assumptions passed to apply_assumption are the local context, rfl, trivial, congr_fun and congr_arg.

solve_by_elim [h₁, h₂, ..., hᵣ] also applies the named lemmas.

`solve_by_elim with attr₁ ... attrᵣ also applied all lemmas tagged with the specified attributes.

solve_by_elim only [h₁, h₂, ..., hᵣ] does not include the local context, rfl, trivial, congr_fun, or congr_arg unless they are explicitly included.

solve_by_elim [-id] removes a specified assumption.

solve_by_elim* tries to solve all goals together, using backtracking if a solution for one goal makes other goals impossible.

optional arguments:

• discharger: a subsidiary tactic to try at each step (e.g. cc may be helpful)
• max_rep: number of attempts at discharging generated sub-goals