op by : term quotation * tactic -> tactic
STRUCTURE
bossLib
SYNOPSIS
Prove and place a theorem on the assumptions of the goal.
DESCRIPTION
An invocation tm by tac, when applied to goal A ?- g, applies tac to goal A ?- tm. If tm is thereby proved, it is added to A, yielding the new goal A,tm ?- g. If tm is not proved by tac, then the application fails.

When tm is added to the existing assumptions A, it is “stripped”, i.e., broken apart by eliminating existentials, conjunctions, and disjunctions. This can lead to case splitting.

FAILURE
Fails if tac fails when applied to A ?- tm, or if tac fails to prove that goal.
EXAMPLE
Given the goal {x <= y, w < x} ?- P, suppose that the fact ?n. y = n + w would help in eventually proving P. Invoking 
   `?n. y = n + w` by (EXISTS_TAC ``y-w`` THEN DECIDE_TAC)
yields the goal {y = n + w, x <= y, w < x} ?- P in which the proved fact has been added to the assumptions after its existential quantifier is eliminated. Note the parentheses around the tactic: this is needed for the example because by binds more tightly than THEN.
COMMENTS
Use of by can be more convenient than IMP_RES_TAC and RES_TAC when they would generate many useless assumptions.
SEEALSO
subgoal, suffices_by, SUBGOAL_THEN, IMP_RES_TAC, RES_TAC, STRIP_ASSUME_TAC
HOL  Kananaskis-13