mathlib3 documentation

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.

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

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