Commit 2024-08-20 02:02 e0c470ac

View on Github →

chore: remove nthLe (#15965) From #15958.

Estimated changes

Modified Mathlib/Data/List/Basic.lean

added theorem List.dropWhile_get_zero_not

deleted theorem List.dropWhile_nthLe_zero_not

modified theorem List.eq_cons_of_length_one

deleted theorem List.ext_nthLe

added theorem List.get_cons

added theorem List.get_tail

deleted theorem List.mem_iff_nthLe

deleted def List.nthLe

deleted theorem List.nthLe_append_right

deleted theorem List.nthLe_cons

deleted theorem List.nthLe_cons_aux

deleted theorem List.nthLe_cons_length

deleted theorem List.nthLe_get?

deleted theorem List.nthLe_map'

deleted theorem List.nthLe_map

deleted theorem List.nthLe_map_rev

deleted theorem List.nthLe_mem

deleted theorem List.nthLe_of_mem

deleted theorem List.nthLe_pmap

deleted theorem List.nthLe_reverse'

deleted theorem List.nthLe_reverse

deleted theorem List.nthLe_singleton

deleted theorem List.nthLe_succ_scanl

deleted theorem List.nthLe_tail

deleted theorem List.nthLe_zero_scanl

modified theorem List.takeWhile_eq_nil_iff

Modified Mathlib/Data/List/Cycle.lean

modified theorem List.next_get

deleted theorem List.next_nthLe

added theorem List.prev_get

deleted theorem List.prev_nthLe

Modified Mathlib/Data/List/DropRight.lean

Modified Mathlib/Data/List/Forall2.lean

deleted theorem List.Forall₂.nthLe

deleted theorem List.forall₂_iff_nthLe

deleted theorem List.forall₂_of_length_eq_of_nthLe

Modified Mathlib/Data/List/Indexes.lean

added theorem List.get_mapIdx

deleted theorem List.nthLe_mapIdx

Modified Mathlib/Data/List/Infix.lean

deleted theorem List.nth_le_inits

deleted theorem List.nth_le_tails

Modified Mathlib/Data/List/InsertNth.lean

deleted theorem List.nthLe_insertNth_add_succ

deleted theorem List.nthLe_insertNth_of_lt

deleted theorem List.nthLe_insertNth_self

Modified Mathlib/Data/List/Join.lean

deleted theorem List.drop_take_succ_eq_cons_nthLe

Modified Mathlib/Data/List/Nodup.lean

deleted theorem List.Nodup.nthLe_inj_iff

deleted theorem List.nodup_iff_nthLe_inj

Modified Mathlib/Data/List/NodupEquivFin.lean

deleted theorem List.duplicate_iff_exists_distinct_nthLe

Modified Mathlib/Data/List/OfFn.lean

deleted theorem List.nthLe_ofFn'

deleted theorem List.nthLe_ofFn

deleted theorem List.ofFn_nthLe

Modified Mathlib/Data/List/Pairwise.lean

deleted theorem List.pairwise_iff_nthLe

Modified Mathlib/Data/List/Perm.lean

deleted theorem List.nthLe_permutations'Aux

Modified Mathlib/Data/List/Range.lean

added theorem List.getElem_range'_1

deleted theorem List.nthLe_finRange

deleted theorem List.nthLe_range'

deleted theorem List.nthLe_range'_1

deleted theorem List.nthLe_range

Modified Mathlib/Data/List/Rotate.lean

added theorem List.get_rotate_one

deleted theorem List.nthLe_rotate'

deleted theorem List.nthLe_rotate

deleted theorem List.nthLe_rotate_one

Modified Mathlib/Data/List/Sort.lean

deleted theorem List.Sorted.rel_nthLe_of_le

deleted theorem List.Sorted.rel_nthLe_of_lt

Modified Mathlib/Data/List/Zip.lean

deleted theorem List.nthLe_zip

deleted theorem List.nthLe_zipWith

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

deleted theorem Equiv.Perm.nthLe_toList

deleted theorem Equiv.Perm.toList_nthLe_zero

Modified Mathlib/GroupTheory/Perm/List.lean

deleted theorem List.formPerm_apply_lt

deleted theorem List.formPerm_apply_nthLe

deleted theorem List.formPerm_apply_nthLe_length

deleted theorem List.formPerm_apply_nthLe_zero

deleted theorem List.formPerm_pow_apply_nthLe