FIND_ASSUM : thm_tactic -> term -> tactic

SYNOPSIS
Apply a theorem-tactic to the the first assumption equal to given term.

DESCRIPTION
The tactic FIND_ASSUM ttac `t` finds the first assumption whose conclusion is t, and applies ttac to it. If there is no such assumption, the call fails.

FAILURE CONDITIONS
Fails if there is no assumption the same as the given term, or if the theorem-tactic itself fails on the assumption.

EXAMPLE
Suppose we set up this goal:
# g `0 = x /\ y = 0 ==> f(x + f(y)) = f(f(f(x) * x * y))`;;
and move the hypotheses into the assumption list:
# e STRIP_TAC;;
val it : goalstack = 1 subgoal (1 total)

0 [`0 = x`]
1 [`y = 0`]

`f (x + f y) = f (f (f x * x * y))`
We can't just use ASM_REWRITE_TAC[] to solve the goal, but we can more directly use the assumptions:
# e(FIND_ASSUM SUBST1_TAC `y = 0` THEN
FIND_ASSUM (SUBST1_TAC o SYM) `0 = x`);;
val it : goalstack = 1 subgoal (1 total)

0 [`0 = x`]
1 [`y = 0`]

`f (0 + f 0) = f (f (f 0 * 0 * 0))`
after which simple rewriting solves the goal: