Mathlib.Tactic.GeneralizeProofs