Commit 2025-09-11 00:51 c2a2f499

View on Github →

chore: deprime induction in Data.List (for real) (#29313) Including removing the Tactic.Cases import in Data.List.Indexes.

Estimated changes

Modified Mathlib/Data/List/Chain.lean

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Data/List/Destutter.lean

Modified Mathlib/Data/List/DropRight.lean

Modified Mathlib/Data/List/Duplicate.lean

Modified Mathlib/Data/List/Indexes.lean

Modified Mathlib/Data/List/Infix.lean

Modified Mathlib/Data/List/Lemmas.lean

Modified Mathlib/Data/List/Lex.lean

Modified Mathlib/Data/List/MinMax.lean

Modified Mathlib/Data/List/NodupEquivFin.lean

Modified Mathlib/Data/List/OfFn.lean

Modified Mathlib/Data/List/Permutation.lean

Modified Mathlib/Data/List/Pi.lean

Modified Mathlib/Data/List/Prime.lean

Modified Mathlib/Data/List/ProdSigma.lean

Modified Mathlib/Data/List/Range.lean

Modified Mathlib/Data/List/ReduceOption.lean

Modified Mathlib/Data/List/Rotate.lean

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/Data/List/SplitOn.lean

Modified Mathlib/Data/List/Sublists.lean

modified theorem List.revzip_sublists'

modified theorem List.revzip_sublists

Modified Mathlib/Data/List/Zip.lean