mathlib3

dabb41f2 - feat(tactic/{induction,fresh_names}): improve `induction' with` (#7726)

feat(tactic/{induction,fresh_names}): improve `induction' with` (#7726) This commit introduces two improvements to the `with` clauses of the `cases'` and `induction'` tactics: - Users can now write a hyphen instead of a name in the `with` clause. This clears the corresponding hypothesis (and any hypotheses depending on it). - When users give an explicit name in the `with` clause, that name is now used verbatim, even if it shadows an existing hypothesis.