Commit 2022-09-12 10:41 dd1ecc5d

View on Github →

chore: bump to 2022-09-11 (#406)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Array/Basic.lean

modified theorem Array.getElem_ofFn

deleted theorem Array.size_mkEmpty

modified theorem Array.size_ofFn

modified theorem Array.size_ofFn_loop

deleted theorem List.toArray_data

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.Fin.exists_iff

deleted theorem List.append_eq_cons_iff

deleted theorem List.append_eq_has_append

deleted theorem List.append_eq_nil

deleted theorem List.append_inj'

deleted theorem List.append_inj

deleted theorem List.append_inj_left'

deleted theorem List.append_inj_left

deleted theorem List.append_inj_right'

deleted theorem List.append_inj_right

deleted theorem List.append_left_inj

deleted theorem List.append_ne_nil_of_left_ne_nil

deleted theorem List.append_ne_nil_of_ne_nil_left

deleted theorem List.append_ne_nil_of_ne_nil_right

deleted theorem List.append_right_inj

deleted theorem List.append_subset_iff

deleted theorem List.bind_map

deleted theorem List.cons_eq_append_iff

deleted theorem List.cons_inj

deleted theorem List.cons_ne_nil

deleted theorem List.cons_ne_self

deleted theorem List.cons_subset

deleted theorem List.empty_eq

deleted theorem List.eq_nil_iff_forall_not_mem

deleted theorem List.eq_nil_of_subset_nil

deleted theorem List.eq_of_mem_replicate

deleted theorem List.eq_of_mem_singleton

deleted theorem List.eq_or_ne_mem_of_mem

modified theorem List.erasep_cons_of_neg

modified theorem List.erasep_cons_of_pos

modified theorem List.erasep_map

deleted theorem List.exists_cons_of_ne_nil

deleted theorem List.exists_mem_cons_iff

modified theorem List.exists_mem_cons_of_exists

deleted theorem List.exists_mem_of_length_pos

deleted theorem List.exists_mem_of_ne_nil

deleted theorem List.exists_of_mem_bind

deleted theorem List.exists_of_mem_join

deleted theorem List.exists_of_mem_map

modified theorem List.exists_or_eq_self_of_erasep

deleted theorem List.forall_mem_append

deleted theorem List.forall_mem_cons

deleted theorem List.forall_mem_map_iff

deleted theorem List.forall_mem_nil

deleted theorem List.forall_mem_singleton

deleted theorem List.get?_eq_get

deleted theorem List.get?_eq_none_iff

deleted theorem List.get?_eq_some

deleted theorem List.get?_len_le

deleted theorem List.get?_mem

deleted theorem List.get?_of_mem

deleted theorem List.get?_zero

deleted theorem List.getLast_append

deleted theorem List.getLast_concat

deleted theorem List.getLast_cons

deleted theorem List.get_cons_drop

deleted theorem List.get_mem

deleted theorem List.get_of_mem

deleted theorem List.head_eq_of_cons_eq

deleted theorem List.join_cons

deleted theorem List.join_nil

deleted theorem List.length_eq_one

deleted theorem List.length_eq_zero

deleted theorem List.length_pos_iff_exists_mem

deleted theorem List.length_pos_iff_ne_nil

deleted theorem List.length_pos_of_mem

deleted theorem List.length_pos_of_ne_nil

deleted theorem List.length_singleton

deleted theorem List.map_eq_append_split

deleted theorem List.map_eq_nil

deleted theorem List.map_subset

deleted theorem List.mem_bind

deleted theorem List.mem_bind_of_mem

deleted theorem List.mem_constructor

deleted theorem List.mem_filter

deleted theorem List.mem_iff_get

deleted theorem List.mem_iff_get?

deleted theorem List.mem_join

deleted theorem List.mem_join_of_mem

deleted theorem List.mem_map

deleted theorem List.mem_map_of_mem

deleted theorem List.mem_of_mem_cons_of_mem

deleted theorem List.mem_replicate

deleted theorem List.mem_reverse

deleted theorem List.mem_reverseAux

deleted theorem List.mem_singleton

deleted theorem List.mem_singleton_self

deleted theorem List.ne_nil_of_length_pos

deleted theorem List.ne_nil_of_mem

deleted theorem List.nil_eq_append_iff

modified theorem List.not_exists_mem_nil

deleted theorem List.or_exists_of_exists_mem_cons

deleted theorem List.replicate_succ

deleted theorem List.singleton_append

deleted theorem List.subset_append_of_subset_left

deleted theorem List.subset_append_of_subset_right

deleted theorem List.subset_def

deleted theorem List.tail_eq_of_cons_eq

deleted theorem List.take_append_drop

Modified Mathlib/Data/List/Card.lean

Deleted Mathlib/Data/List/Defs.lean

deleted def List.Chain'

deleted inductive List.Chain

deleted inductive List.Forall₂

deleted def List.Nodup

deleted inductive List.Pairwise

deleted def List.allSome

deleted def List.count

deleted def List.countp

deleted def List.disjoint

deleted def List.eraseDup

deleted def List.erasep

deleted def List.extractp

deleted def List.fillNones

deleted def List.find

deleted def List.findIdx?

deleted def List.findIdxs

deleted def List.foldlIdx

deleted def List.foldlIdxAux

deleted def List.foldrIdx

deleted def List.foldrIdxAux

deleted def List.getRest

deleted def List.ilast'

deleted def List.indexOf?

deleted def List.indexesOf

deleted def List.indexesValues

deleted def List.inits

deleted def List.insertNth

deleted def List.isInfix

deleted def List.isPrefix

deleted def List.isSuffix

deleted def List.last'

deleted def List.lookmap

deleted def List.mapWithComplement

deleted def List.mapWithPrefixSuffix

deleted def List.mapWithPrefixSuffixAux

deleted def List.map₂Left'

deleted def List.map₂Left

deleted def List.map₂Right'

deleted def List.map₂Right

deleted def List.mmap'

deleted def List.mmap'Diag

deleted def List.mmap

deleted def List.mmapFilter

deleted def List.mmapUpperTriangle

deleted def List.modifyHead

deleted def List.modifyLast

deleted def List.modifyNth

deleted def List.modifyNthTail

deleted def List.ofFn

deleted def List.ofFnAux

deleted def List.ofFnNthVal

deleted def List.partitionMap

deleted def List.product

deleted def List.pwFilter

deleted def List.range'

deleted def List.reduceOption

deleted def List.revzip

deleted def List.rotate'

deleted def List.rotate

deleted def List.scanl

deleted def List.scanr

deleted def List.scanrAux

deleted def List.sections

deleted def List.slice

deleted def List.splitAt

deleted def List.splitAtD

deleted def List.splitOn

deleted def List.splitOnP

deleted def List.splitOnPAux

deleted def List.sublists'

deleted def List.sublists'Aux

deleted def List.sublists

deleted def List.sublistsAux

deleted def List.sublistsAux₁

deleted def List.tails

deleted def List.takeD

deleted def List.takeList

deleted def List.toChunks

deleted def List.toChunksAux

deleted def List.transpose

deleted def List.transposeAux

deleted def List.zipLeft'

deleted def List.zipLeft

deleted def List.zipRight'

deleted def List.zipRight

deleted def List.zipWith₃

deleted def List.zipWith₄

deleted def List.zipWith₅

Modified Mathlib/Data/List/Perm.lean

Modified Mathlib/Logic/Basic.lean

added theorem Or.imp3

added theorem and_or_imp

added theorem imp_iff_or_not

added theorem imp_iff_right_iff

added theorem not_ne_iff

added theorem or_congr_left'

added theorem or_congr_right'

Modified Mathlib/Logic/Equiv/MfldSimpsAttr.lean

Modified Mathlib/Logic/Nonempty.lean

deleted theorem nonempty_empty

Modified Mathlib/Tactic/Cases.lean

Modified Mathlib/Tactic/PermuteGoals.lean

Modified lean-toolchain

Modified lean_packages/manifest.json

Modified test/cases.lean