Commit 2024-05-05 03:48 7769e81d
View on Github →chore: deprecate redundant lemma List.get?_injective (#12630)
Deprecates List.get?_injective, which is a duplicate of List.gen?_inj in Std: https://github.com/leanprover/std4/blob/80cf5a1f2d8ed48753e8ff783bf0f7b6872bb007/Std/Data/List/Lemmas.lean#L773-L788