Commit 2022-11-07 20:49 eb883535

View on Github →

feat: generalize_proofs tactic (#447)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/GeneralizeProofs.lean

added structure Mathlib.Tactic.GeneralizeProofs.State

Created test/GeneralizeProofs.lean

added def List.nthLe