Commit 2024-12-12 08:11 b18b0c87

View on Github →

chore: deprecate upstreamed theorem List.cons_subperm_of_mem (#19904) Deprecates List.cons_subperm_of_mem, which was upstreamed to Batteries as List.cons_subperm_of_not_mem_of_mem in https://github.com/leanprover-community/batteries/pull/89. The upstream version is in fact stronger, as it does not have a Nodup l₁ parameter. This duplication was found by tryAtEachStep.

Estimated changes

Modified Mathlib/Data/List/Perm/Subperm.lean

modified theorem List.cons_subperm_of_mem