mathlib3
f7654b3f - feat(tactic/generalizes): tactic for generalizing over multiple expressions (#2982)

Commit
5 years ago
feat(tactic/generalizes): tactic for generalizing over multiple expressions (#2982) This commit adds a tactic `generalizes` which works like `generalize` but for multiple expressions at once. The tactic is more powerful than calling `generalize` multiple times since this usually fails when there are dependencies between the expressions. By contrast, `generalizes` handles at least some such situations. Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Author
Parents
Loading