# mathlibdocumentation

tactic.generalize_proofs

# generalize_proofs#

A simple tactic to find and replace all occurrences of proof terms in the context and goal with new variables.

meta def tactic.generalize_proofs (ns : list name) (loc : interactive.loc) :

Generalize proofs in the goal, naming them with the provided list.

Generalize proofs in the goal, naming them with the provided list.

For example:

example : list.nth_le [1, 2] 1 dec_trivial = 2 :=
begin
-- ⊢ [1, 2].nth_le 1 _ = 2
generalize_proofs h,
-- h : 1 < [1, 2].length
-- ⊢ [1, 2].nth_le 1 h = 2
end