Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-10-15 01:58 8f4327ae

View on Github →

feat(*): working on list/basic, robusting simp proofs

Estimated changes

Modified algebra/big_operators.lean

added theorem list.prod_repeat

deleted theorem list.prod_replicate

Modified algebra/field.lean

added theorem division_ring.neg_inv

Modified algebra/functions.lean

added theorem lt_max_iff

Modified analysis/ennreal.lean

Modified analysis/limits.lean

Modified analysis/measure_theory/borel_space.lean

Modified analysis/measure_theory/measure_space.lean

Modified analysis/measure_theory/outer_measure.lean

Modified analysis/metric_space.lean

Modified analysis/of_nat.lean

Modified analysis/real.lean

added theorem of_rat_inj

added theorem of_rat_injective

added theorem of_rat_lt

deleted theorem of_rat_lt_of_rat

Modified analysis/topology/continuity.lean

Modified analysis/topology/infinite_sum.lean

Modified analysis/topology/topological_space.lean

Modified analysis/topology/topological_structures.lean

Modified analysis/topology/uniform_space.lean

Modified data/bool.lean

deleted theorem bool.band_eq_ff

deleted theorem bool.band_eq_tt

deleted theorem bool.band_ff

deleted theorem bool.band_self

deleted theorem bool.band_tt

deleted theorem bool.bnot_bnot

deleted theorem bool.bor_eq_ff

deleted theorem bool.bor_eq_tt

deleted theorem bool.bor_ff

modified theorem bool.bor_inl

modified theorem bool.bor_inr

deleted theorem bool.bor_tt

deleted def bool.bxor

deleted theorem bool.bxor_ff

deleted theorem bool.bxor_self

deleted theorem bool.bxor_tt

added theorem bool.coe_sort_ff

added theorem bool.coe_sort_tt

deleted theorem bool.coe_tt

deleted theorem bool.ff_band

deleted theorem bool.ff_bor

deleted theorem bool.ff_bxor

deleted theorem bool.ff_bxor_ff

deleted theorem bool.ff_bxor_tt

deleted theorem bool.or_of_bor_eq

added theorem bool.to_bool_bool

added theorem bool.to_bool_false

added theorem bool.to_bool_true

deleted theorem bool.tt_band

deleted theorem bool.tt_bor

deleted theorem bool.tt_bxor

deleted theorem bool.tt_bxor_ff

deleted theorem bool.tt_bxor_tt

Modified data/encodable.lean

added theorem encode_injective

Modified data/equiv.lean

added def equiv.list_equiv_of_equiv

added def equiv.list_equiv_self_of_equiv_nat

added def equiv.list_nat_equiv_nat

Modified data/finset/basic.lean

added theorem finset.card_range

deleted theorem finset.card_upto

added theorem finset.exists_mem_insert

deleted theorem finset.exists_mem_insert_iff

added theorem finset.exists_nat_subset_range

deleted theorem finset.exists_nat_subset_upto

added theorem finset.forall_mem_insert

deleted theorem finset.forall_mem_insert_iff

deleted theorem finset.lt_of_mem_upto

deleted theorem finset.mem_empty_iff

added theorem finset.mem_erase

deleted theorem finset.mem_erase_iff

added theorem finset.mem_filter

deleted theorem finset.mem_filter_iff

modified theorem finset.mem_insert

deleted theorem finset.mem_insert_iff

added theorem finset.mem_insert_self

modified theorem finset.mem_inter

deleted theorem finset.mem_inter_iff

added theorem finset.mem_inter_of_mem

modified theorem finset.mem_list_of_mem

modified theorem finset.mem_of_mem_list

added theorem finset.mem_range

modified theorem finset.mem_sdiff_iff

modified theorem finset.mem_singleton_self

modified theorem finset.mem_to_finset

deleted theorem finset.mem_to_finset_iff

added theorem finset.mem_to_finset_of_mem

added theorem finset.mem_union

deleted theorem finset.mem_union_iff

deleted theorem finset.mem_upto_iff

deleted theorem finset.mem_upto_of_lt

deleted theorem finset.mem_upto_succ_of_mem_upto

modified theorem finset.not_mem_empty

added theorem finset.not_mem_range_self

deleted theorem finset.not_mem_upto

added def finset.range

added theorem finset.range_subset

added theorem finset.range_succ

added theorem finset.range_zero

deleted def finset.upto

deleted theorem finset.upto_subset_upto_iff

deleted theorem finset.upto_succ

deleted theorem finset.upto_zero

deleted theorem lt_max_iff

Modified data/finset/fold.lean

deleted theorem heq_iff_eq

Modified data/hash_map.lean

modified theorem bucket_array.mem_as_list

modified theorem hash_map.contains_aux_iff

modified theorem hash_map.find_aux_iff

Modified data/list/basic.lean

added theorem list.all_cons

added theorem list.all_iff_forall

added theorem list.all_iff_forall_prop

added theorem list.all_nil

added theorem list.any_cons

added theorem list.any_iff_exists

added theorem list.any_iff_exists_prop

added theorem list.any_nil

added theorem list.any_of_mem

added theorem list.append_inj'

added theorem list.append_inj_left'

added theorem list.append_inj_right'

added theorem list.append_left_cancel

added theorem list.append_right_cancel

deleted theorem list.append_right_inj

added theorem list.append_sublist_append_left

added theorem list.append_sublist_append_of_sublist_right

added theorem list.append_sublist_append_right

added theorem list.chain.iff

added theorem list.chain.iff_mem

added theorem list.chain.imp

added inductive list.chain

added theorem list.chain_cons

added theorem list.chain_iff_pairwise

added theorem list.chain_lt_range'

added theorem list.chain_map

added theorem list.chain_map_of_chain

added theorem list.chain_of_chain_cons

added theorem list.chain_of_chain_map

added theorem list.chain_of_pairwise

added theorem list.chain_singleton

added theorem list.chain_split

added theorem list.chain_succ_range'

modified def list.concat

modified theorem list.concat_eq_append

added theorem list.cons_inj'

modified theorem list.cons_inj

added theorem list.cons_sublist_cons_iff

added theorem list.cons_union

modified def list.count

modified theorem list.count_append

added theorem list.count_eq_one_of_mem

added theorem list.count_le_of_sublist

added theorem list.count_pos

modified theorem list.count_pos_of_mem

added theorem list.count_repeat

added def list.countp

added theorem list.countp_append

added theorem list.countp_cons_of_neg

added theorem list.countp_cons_of_pos

added theorem list.countp_eq_length_filter

added theorem list.countp_le_of_sublist

added theorem list.countp_nil

added theorem list.countp_pos_of_mem

added theorem list.disjoint.symm

added def list.disjoint

added theorem list.disjoint_append_left

added theorem list.disjoint_append_of_disjoint_left

added theorem list.disjoint_append_right

added theorem list.disjoint_comm

added theorem list.disjoint_cons_left

added theorem list.disjoint_cons_right

added theorem list.disjoint_iff_ne

added theorem list.disjoint_left

added theorem list.disjoint_nil_left

added theorem list.disjoint_of_disjoint_append_left_left

added theorem list.disjoint_of_disjoint_append_left_right

added theorem list.disjoint_of_disjoint_append_right_left

added theorem list.disjoint_of_disjoint_append_right_right

added theorem list.disjoint_of_disjoint_cons_left

added theorem list.disjoint_of_disjoint_cons_right

added theorem list.disjoint_of_nodup_append

added theorem list.disjoint_of_subset_left

added theorem list.disjoint_of_subset_right

added theorem list.disjoint_right

added theorem list.disjoint_singleton

added theorem list.eq_nil_iff_forall_not_mem

modified theorem list.eq_nil_of_infix_nil

modified theorem list.eq_nil_of_prefix_nil

modified theorem list.eq_nil_of_suffix_nil

added theorem list.eq_of_infix_of_length_eq

deleted theorem list.eq_of_map_const

added theorem list.eq_of_mem_map_const

added theorem list.eq_of_mem_repeat

added theorem list.eq_of_mem_singleton

added theorem list.eq_of_prefix_of_length_eq

added theorem list.eq_of_sublist_of_length_eq

added theorem list.eq_of_suffix_of_length_eq

added theorem list.eq_or_mem_of_mem_insert

added theorem list.eq_repeat'

added theorem list.eq_repeat

added theorem list.eq_repeat_of_mem

added theorem list.erase_append_left

added theorem list.erase_append_right

added theorem list.erase_cons

added theorem list.erase_cons_head

added theorem list.erase_cons_tail

added def list.erase_dup

added theorem list.erase_dup_append

added theorem list.erase_dup_cons_of_mem'

added theorem list.erase_dup_cons_of_mem

added theorem list.erase_dup_cons_of_not_mem'

added theorem list.erase_dup_cons_of_not_mem

added theorem list.erase_dup_eq_self

added theorem list.erase_dup_nil

added theorem list.erase_dup_sublist

added theorem list.erase_dup_subset

added theorem list.erase_nil

added theorem list.erase_of_not_mem

added theorem list.erase_sublist

added theorem list.erase_subset

added theorem list.exists_erase_eq

added theorem list.exists_mem_cons_iff

added theorem list.exists_mem_cons_of

added theorem list.exists_mem_cons_of_exists

added theorem list.exists_mem_of_countp_pos

added theorem list.exists_mem_of_length_pos

modified theorem list.exists_of_mem_bind

added theorem list.filter_eq_nil

added theorem list.filter_eq_self

added theorem list.filter_filter_map

added theorem list.filter_map_cons_none

added theorem list.filter_map_cons_some

added theorem list.filter_map_eq_filter

added theorem list.filter_map_eq_map

added theorem list.filter_map_filter

added theorem list.filter_map_filter_map

added theorem list.filter_map_map

added theorem list.filter_map_nil

added theorem list.filter_map_some

added theorem list.filter_map_sublist_filter_map

added theorem list.filter_sublist_filter

modified theorem list.filter_subset

modified def list.find

added theorem list.find_cons_of_neg

added theorem list.find_cons_of_pos

added theorem list.find_eq_none

added theorem list.find_mem

added theorem list.find_nil

added theorem list.find_some

added theorem list.foldl1_eq_foldr1

added theorem list.foldl_append

added theorem list.foldl_cons

added theorem list.foldl_eq_foldr

added theorem list.foldl_eq_of_comm_of_assoc

added theorem list.foldl_nil

added theorem list.foldl_reverse

added theorem list.foldr_append

added theorem list.foldr_cons

modified theorem list.foldr_eta

added theorem list.foldr_nil

added theorem list.foldr_reverse

added theorem list.forall_mem_cons'

added theorem list.forall_mem_cons

added theorem list.forall_mem_inter_of_forall_left

added theorem list.forall_mem_inter_of_forall_right

added theorem list.forall_mem_ne

added theorem list.forall_mem_nil

added theorem list.forall_mem_of_forall_mem_cons

added theorem list.forall_mem_of_forall_mem_union_left

added theorem list.forall_mem_of_forall_mem_union_right

added theorem list.forall_mem_pw_filter

added theorem list.forall_mem_union

modified theorem list.head_eq_of_cons_eq

modified theorem list.infix_append

modified theorem list.infix_iff_prefix_suffix

modified theorem list.infix_of_prefix

modified theorem list.infix_of_suffix

modified theorem list.infix_refl

modified def list.inits

added theorem list.insert.def

added theorem list.insert_nil

added theorem list.insert_of_mem

added theorem list.insert_of_not_mem

added theorem list.inter_cons_of_mem

added theorem list.inter_cons_of_not_mem

added theorem list.inter_eq_nil_iff_disjoint

added theorem list.inter_nil

added theorem list.inter_subset_left

added theorem list.inter_subset_right

modified def list.inth

added theorem list.iota_eq_reverse_range'

added theorem list.is_infix.trans

added theorem list.is_prefix.trans

added theorem list.is_suffix.trans

added theorem list.le_count_iff_repeat_sublist

modified theorem list.length_concat

added theorem list.length_erase_of_mem

added theorem list.length_insert_of_mem

added theorem list.length_insert_of_not_mem

added theorem list.length_iota

modified theorem list.length_le_of_infix

added theorem list.length_product

added theorem list.length_range'

added theorem list.length_range

modified theorem list.map_concat

added theorem list.map_const

added theorem list.map_filter_map

added theorem list.map_filter_map_of_inv

added theorem list.map₂_nil

modified theorem list.mem_bind

deleted theorem list.mem_bind_iff

added theorem list.mem_bind_of_mem

added theorem list.mem_erase_dup

added theorem list.mem_erase_iff_of_nodup

added theorem list.mem_erase_of_ne_of_mem

added theorem list.mem_erase_of_nodup

added theorem list.mem_filter

deleted theorem list.mem_filter_iff

added theorem list.mem_filter_map

modified theorem list.mem_filter_of_mem

deleted theorem list.mem_iff_count_pos

modified theorem list.mem_inits

added theorem list.mem_insert_iff

added theorem list.mem_insert_of_mem

added theorem list.mem_insert_self

added theorem list.mem_inter

added theorem list.mem_inter_of_mem_of_mem

added theorem list.mem_iota

modified theorem list.mem_join

deleted theorem list.mem_join_iff

added theorem list.mem_join_of_mem

modified theorem list.mem_map

deleted theorem list.mem_map_iff

added theorem list.mem_map_of_inj

added theorem list.mem_map_of_mem

modified theorem list.mem_of_count_pos

added theorem list.mem_of_mem_erase

modified theorem list.mem_of_mem_filter

added theorem list.mem_of_mem_inter_left

added theorem list.mem_of_mem_inter_right

added theorem list.mem_product

added theorem list.mem_range'

added theorem list.mem_range

modified theorem list.mem_reverse

modified theorem list.mem_singleton

deleted theorem list.mem_singleton_iff

added theorem list.mem_singleton_self

modified theorem list.mem_split

modified theorem list.mem_sublists

modified theorem list.mem_tails

added theorem list.mem_union

added theorem list.mem_union_left

added theorem list.mem_union_right

added theorem list.nil_map₂

added theorem list.nil_product

added theorem list.nil_union

added def list.nodup

added theorem list.nodup_app_comm

added theorem list.nodup_append

added theorem list.nodup_append_of_nodup

added theorem list.nodup_bind

added theorem list.nodup_concat

added theorem list.nodup_cons

added theorem list.nodup_cons_of_nodup

added theorem list.nodup_erase_dup

added theorem list.nodup_erase_eq_filter

added theorem list.nodup_erase_of_nodup

added theorem list.nodup_filter

added theorem list.nodup_filter_map

added theorem list.nodup_iff_count_le_one

added theorem list.nodup_iff_sublist

added theorem list.nodup_insert

added theorem list.nodup_inter_of_nodup

added theorem list.nodup_iota

added theorem list.nodup_join

added theorem list.nodup_map

added theorem list.nodup_map_on

added theorem list.nodup_middle

added theorem list.nodup_nil

added theorem list.nodup_of_nodup_append_left

added theorem list.nodup_of_nodup_append_right

added theorem list.nodup_of_nodup_cons

added theorem list.nodup_of_nodup_map

added theorem list.nodup_of_sublist

added theorem list.nodup_product

added theorem list.nodup_range'

added theorem list.nodup_range

added theorem list.nodup_reverse

added theorem list.nodup_singleton

added theorem list.nodup_union

added theorem list.not_exists_mem_nil

modified theorem list.not_mem_append

added theorem list.not_mem_of_nodup_cons

added theorem list.not_mem_range_self

added theorem list.not_nodup_cons_of_mem

added theorem list.not_nodup_pair

modified theorem list.of_mem_filter

added theorem list.or_exists_of_exists_mem_cons

added theorem list.pairwise.iff

added theorem list.pairwise.iff_mem

added theorem list.pairwise.imp

added inductive list.pairwise

added theorem list.pairwise_app_comm

added theorem list.pairwise_append

added theorem list.pairwise_cons

added theorem list.pairwise_filter

added theorem list.pairwise_filter_map

added theorem list.pairwise_filter_map_of_pairwise

added theorem list.pairwise_filter_of_pairwise

added theorem list.pairwise_gt_iota

added theorem list.pairwise_join

added theorem list.pairwise_lt_range'

added theorem list.pairwise_lt_range

added theorem list.pairwise_map

added theorem list.pairwise_map_of_pairwise

added theorem list.pairwise_middle

added theorem list.pairwise_of_forall

added theorem list.pairwise_of_pairwise_cons

added theorem list.pairwise_of_pairwise_map

added theorem list.pairwise_of_sublist

added theorem list.pairwise_pair

added theorem list.pairwise_pw_filter

added theorem list.pairwise_reverse

added theorem list.pairwise_singleton

modified theorem list.prefix_append

added theorem list.prefix_concat

modified theorem list.prefix_refl

added def list.prod

added def list.product

added theorem list.product_cons

added theorem list.product_nil

added def list.pw_filter

added theorem list.pw_filter_cons_of_neg

added theorem list.pw_filter_cons_of_pos

added theorem list.pw_filter_eq_self

added theorem list.pw_filter_nil

added theorem list.pw_filter_sublist

added theorem list.pw_filter_subset

added def list.range'

added theorem list.range'_append

added theorem list.range'_concat

added theorem list.range'_sublist_right

added theorem list.range'_subset_right

added theorem list.range_core_range'

added theorem list.range_eq_range'

added theorem list.range_sublist

added theorem list.range_subset

added theorem list.rel_of_chain_cons

added theorem list.rel_of_pairwise_cons

added theorem list.repeat_sublist_repeat

added theorem list.repeat_subset_singleton

added theorem list.reverse_cons'

added theorem list.reverse_sublist

added theorem list.reverse_sublist_iff

modified theorem list.scanr_aux_cons

modified theorem list.scanr_cons

modified theorem list.scanr_nil

added theorem list.singleton_disjoint

added theorem list.singleton_sublist

modified theorem list.span_eq_take_drop

added theorem list.sublist_antisymm

modified theorem list.sublist_app_of_sublist_left

modified theorem list.sublist_app_of_sublist_right

modified theorem list.sublist_of_infix

added theorem list.sublist_of_prefix

added theorem list.sublist_of_suffix

added theorem list.sublist_suffix_of_union

modified theorem list.sublists_aux_cons_cons

modified theorem list.sublists_aux_eq_foldl

added theorem list.subset_erase_dup

added theorem list.subset_inter

modified theorem list.suffix_append

added theorem list.suffix_cons

added theorem list.suffix_insert

modified theorem list.suffix_refl

added theorem list.suffix_union_right

modified def list.sum

modified theorem list.tail_eq_of_cons_eq

modified def list.tails

modified theorem list.take_while_append_drop

added theorem list.union_sublist_append

added theorem list.unzip_cons

added theorem list.unzip_nil

added theorem list.zip_cons_cons

added theorem list.zip_nil_left

added theorem list.zip_nil_right

added theorem list.zip_unzip

Deleted data/list/comb.lean

deleted theorem list.all_cons

deleted theorem list.all_eq_tt_iff

deleted theorem list.all_eq_tt_of_forall

deleted theorem list.all_nil

deleted theorem list.any_cons

deleted theorem list.any_eq_tt_iff

deleted theorem list.any_nil

deleted theorem list.any_of_mem

deleted def list.dinj

deleted def list.dinj₁

deleted def list.dmap

deleted theorem list.dmap_cons_of_neg

deleted theorem list.dmap_cons_of_pos

deleted theorem list.dmap_nil

deleted theorem list.eq_of_mem_map_pair₁

deleted theorem list.exists_mem_cons_iff

deleted theorem list.exists_mem_cons_of

deleted theorem list.exists_mem_cons_of_exists

deleted theorem list.exists_of_any_eq_tt

deleted theorem list.exists_of_mem_dmap

deleted def list.flat

deleted theorem list.foldl_append

deleted theorem list.foldl_cons

deleted theorem list.foldl_eq_foldr

deleted theorem list.foldl_eq_of_comm_of_assoc

deleted theorem list.foldl_nil

deleted theorem list.foldl_reverse

deleted theorem list.foldr_append

deleted theorem list.foldr_cons

deleted theorem list.foldr_nil

deleted theorem list.foldr_reverse

deleted theorem list.forall_mem_cons

deleted theorem list.forall_mem_cons_iff

deleted theorem list.forall_mem_eq_tt_of_all_eq_tt

deleted theorem list.forall_mem_nil

deleted theorem list.forall_mem_of_forall_mem_cons

deleted theorem list.length_mapAccumR

deleted theorem list.length_mapAccumR₂

deleted theorem list.length_product

deleted theorem list.length_replicate

deleted def list.mapAccumR

deleted def list.mapAccumR₂

deleted theorem list.map_dmap_of_inv_of_pos

deleted theorem list.map₂_nil1

deleted theorem list.map₂_nil2

deleted theorem list.mem_dmap

deleted theorem list.mem_of_dinj_of_mem_dmap

deleted theorem list.mem_of_mem_map_pair₁

deleted theorem list.mem_of_mem_product_left

deleted theorem list.mem_of_mem_product_right

deleted theorem list.mem_product

deleted theorem list.nil_product

deleted theorem list.not_exists_mem_nil

deleted theorem list.not_mem_dmap_of_dinj_of_not_mem

deleted theorem list.of_forall_mem_cons

deleted theorem list.or_exists_of_exists_mem_cons

deleted def list.product

deleted theorem list.product_cons

deleted theorem list.product_nil

deleted def list.replicate

deleted theorem list.unzip_cons'

deleted theorem list.unzip_cons

deleted theorem list.unzip_nil

deleted theorem list.zip_cons_cons

deleted theorem list.zip_nil_left

deleted theorem list.zip_nil_right

deleted theorem list.zip_unzip

Modified data/list/default.lean

Modified data/list/perm.lean

added theorem list.concat_perm

added theorem list.cons_perm_iff_perm_erase

added theorem list.eq_nil_of_perm_nil

added theorem list.eq_singleton_of_perm

added theorem list.eq_singleton_of_perm_inv

added theorem list.erase_perm_erase

added theorem list.exists_perm_sublist

added theorem list.exists_sublist_perm_of_subset_nodup

added theorem list.foldl_eq_of_perm

added theorem list.foldr_eq_of_perm

added theorem list.mem_iff_mem_of_perm

added theorem list.mem_of_perm

added theorem list.not_perm_nil_cons

deleted theorem list.perm.count_eq_count_of_perm

deleted def list.perm.decidable_perm

deleted def list.perm.decidable_perm_aux

deleted theorem list.perm.eq_nil_of_perm_nil

deleted theorem list.perm.eq_singleton_of_perm

deleted theorem list.perm.eq_singleton_of_perm_inv

modified theorem list.perm.eqv

deleted theorem list.perm.erase_perm_erase_of_perm

deleted theorem list.perm.foldl_eq_of_perm

deleted theorem list.perm.foldr_eq_of_perm

deleted theorem list.perm.length_eq_length_of_perm

deleted theorem list.perm.length_eq_of_qeq

deleted theorem list.perm.mem_cons_of_qeq

deleted theorem list.perm.mem_head_of_qeq

deleted theorem list.perm.mem_iff_mem_of_perm

deleted theorem list.perm.mem_of_perm

deleted theorem list.perm.mem_tail_of_qeq

deleted theorem list.perm.nodup_of_perm_of_nodup

deleted theorem list.perm.not_mem_of_perm

deleted theorem list.perm.not_perm_nil_cons

deleted theorem list.perm.perm_app

deleted theorem list.perm.perm_app_comm

deleted theorem list.perm.perm_app_cons

deleted theorem list.perm.perm_app_inv

deleted theorem list.perm.perm_app_inv_left

deleted theorem list.perm.perm_app_inv_right

deleted theorem list.perm.perm_app_left

deleted theorem list.perm.perm_app_right

deleted theorem list.perm.perm_cons_app

deleted theorem list.perm.perm_cons_app_cons

deleted theorem list.perm.perm_cons_app_simp

deleted theorem list.perm.perm_cons_inv

deleted theorem list.perm.perm_erase

deleted theorem list.perm.perm_erase_dup_of_perm

deleted theorem list.perm.perm_ext

deleted theorem list.perm.perm_filter

deleted theorem list.perm.perm_iff_forall_count_eq_count

deleted theorem list.perm.perm_iff_forall_mem_count_eq_count

deleted theorem list.perm.perm_induction_on

deleted theorem list.perm.perm_insert

deleted theorem list.perm.perm_insert_insert

deleted theorem list.perm.perm_inter

deleted theorem list.perm.perm_inter_left

deleted theorem list.perm.perm_inter_right

deleted theorem list.perm.perm_inv_core

deleted theorem list.perm.perm_map

deleted theorem list.perm.perm_middle

deleted theorem list.perm.perm_middle_simp

deleted theorem list.perm.perm_of_forall_count_eq

deleted theorem list.perm.perm_of_qeq

deleted theorem list.perm.perm_product

deleted theorem list.perm.perm_product_left

deleted theorem list.perm.perm_product_right

deleted theorem list.perm.perm_rev

deleted theorem list.perm.perm_rev_simp

deleted theorem list.perm.perm_union

deleted theorem list.perm.perm_union_left

deleted theorem list.perm.perm_union_right

deleted inductive list.perm.qeq

deleted theorem list.perm.qeq_app

deleted theorem list.perm.qeq_of_mem

deleted theorem list.perm.qeq_split

deleted theorem list.perm.subset_of_mem_of_subset_of_qeq

deleted theorem list.perm.xswap

added theorem list.perm_app

added theorem list.perm_app_comm

added theorem list.perm_app_cons

added theorem list.perm_app_inv_right

added theorem list.perm_app_left

added theorem list.perm_app_left_iff

added theorem list.perm_app_right

added theorem list.perm_bind_left

added theorem list.perm_bind_right

added theorem list.perm_cons

added theorem list.perm_cons_app

added theorem list.perm_cons_app_cons

added theorem list.perm_cons_inv

added theorem list.perm_count

added theorem list.perm_countp

added theorem list.perm_erase

added theorem list.perm_erase_dup_of_perm

added theorem list.perm_ext

added theorem list.perm_filter

added theorem list.perm_filter_map

added theorem list.perm_iff_count

added theorem list.perm_induction_on

added theorem list.perm_insert

added theorem list.perm_insert_swap

added theorem list.perm_inter

added theorem list.perm_inter_left

added theorem list.perm_inter_right

added theorem list.perm_inv_core

added theorem list.perm_length

added theorem list.perm_map

added theorem list.perm_middle

added theorem list.perm_nodup

added theorem list.perm_pairwise

added theorem list.perm_product

added theorem list.perm_product_left

added theorem list.perm_product_right

added theorem list.perm_repeat

added theorem list.perm_union

added theorem list.perm_union_left

added theorem list.perm_union_right

added theorem list.reverse_perm

added theorem list.xswap

Deleted data/list/set.lean

deleted theorem list.cons_union

deleted theorem list.disjoint.symm

deleted def list.disjoint

deleted theorem list.disjoint_append_of_disjoint_left

deleted theorem list.disjoint_comm

deleted theorem list.disjoint_cons_of_not_mem_of_disjoint

deleted theorem list.disjoint_left

deleted theorem list.disjoint_nil_left

deleted theorem list.disjoint_of_disjoint_append_left_left

deleted theorem list.disjoint_of_disjoint_append_left_right

deleted theorem list.disjoint_of_disjoint_append_right_left

deleted theorem list.disjoint_of_disjoint_append_right_right

deleted theorem list.disjoint_of_disjoint_cons_left

deleted theorem list.disjoint_of_disjoint_cons_right

deleted theorem list.disjoint_of_nodup_append

deleted theorem list.disjoint_of_subset_left

deleted theorem list.disjoint_of_subset_right

deleted theorem list.disjoint_right

deleted theorem list.disjoint_singleton

deleted theorem list.dmap_nodup_of_dinj

deleted theorem list.eq_or_mem_of_mem_insert

deleted theorem list.erase_append_left

deleted theorem list.erase_append_right

deleted theorem list.erase_cons_head

deleted theorem list.erase_cons_tail

deleted def list.erase_dup

deleted theorem list.erase_dup_cons_of_mem

deleted theorem list.erase_dup_cons_of_not_mem

deleted theorem list.erase_dup_eq_of_nodup

deleted theorem list.erase_dup_nil

deleted theorem list.erase_dup_sublist

deleted theorem list.erase_dup_subset

deleted theorem list.erase_nil

deleted theorem list.erase_of_not_mem

deleted theorem list.erase_sublist

deleted theorem list.erase_subset

deleted theorem list.forall_mem_insert_of_forall_mem

deleted theorem list.forall_mem_inter_of_forall_left

deleted theorem list.forall_mem_inter_of_forall_right

deleted theorem list.forall_mem_of_forall_mem_union_left

deleted theorem list.forall_mem_of_forall_mem_union_right

deleted theorem list.forall_mem_union

deleted theorem list.insert.def

deleted theorem list.insert_nil

deleted theorem list.insert_of_mem

deleted theorem list.insert_of_not_mem

deleted theorem list.inter_cons_of_mem

deleted theorem list.inter_cons_of_not_mem

deleted theorem list.inter_eq_nil_of_disjoint

deleted theorem list.inter_nil

deleted theorem list.length_erase_of_mem

deleted theorem list.length_erase_of_not_mem

deleted theorem list.length_insert_of_mem

deleted theorem list.length_insert_of_not_mem

deleted theorem list.length_upto

deleted theorem list.lt_of_mem_upto

deleted theorem list.mem_erase_dup

deleted theorem list.mem_erase_iff_of_nodup

deleted theorem list.mem_erase_of_ne_of_mem

deleted theorem list.mem_erase_of_nodup

deleted theorem list.mem_insert_iff

deleted theorem list.mem_insert_of_mem

deleted theorem list.mem_insert_self

deleted theorem list.mem_inter_iff

deleted theorem list.mem_inter_of_mem_of_mem

deleted theorem list.mem_of_mem_erase

deleted theorem list.mem_of_mem_inter_left

deleted theorem list.mem_of_mem_inter_right

deleted theorem list.mem_or_mem_of_mem_union

deleted theorem list.mem_union_iff

deleted theorem list.mem_union_left

deleted theorem list.mem_union_right

deleted theorem list.mem_upto_of_lt

deleted theorem list.mem_upto_succ_of_mem_upto

deleted theorem list.nil_union

deleted inductive list.nodup

deleted theorem list.nodup_app_comm

deleted theorem list.nodup_append

deleted theorem list.nodup_concat

deleted theorem list.nodup_cons

deleted theorem list.nodup_erase_dup

deleted theorem list.nodup_erase_of_nodup

deleted theorem list.nodup_filter

deleted theorem list.nodup_head

deleted theorem list.nodup_insert

deleted theorem list.nodup_inter_of_nodup

deleted theorem list.nodup_map

deleted theorem list.nodup_map_on

deleted theorem list.nodup_middle

deleted theorem list.nodup_nil

deleted theorem list.nodup_of_nodup_append_left

deleted theorem list.nodup_of_nodup_append_right

deleted theorem list.nodup_of_nodup_cons

deleted theorem list.nodup_of_nodup_map

deleted theorem list.nodup_of_sublist

deleted theorem list.nodup_product

deleted theorem list.nodup_singleton

deleted theorem list.nodup_union

deleted theorem list.nodup_upto

deleted theorem list.not_mem_of_nodup_cons

deleted theorem list.not_nodup_cons_of_mem

deleted theorem list.not_nodup_cons_of_not_nodup

deleted theorem list.singleton_disjoint

deleted theorem list.subset_erase_dup

deleted def list.upto

deleted theorem list.upto_ne_nil_of_ne_zero

deleted theorem list.upto_nil

deleted theorem list.upto_step

deleted theorem list.upto_succ

Modified data/list/sort.lean

modified theorem list.eq_of_sorted_of_perm

deleted theorem list.forall_mem_rel_of_sorted_cons

modified def list.insertion_sort

modified def list.ordered_insert

added theorem list.rel_of_sorted_cons

modified def list.sorted

modified theorem list.sorted_cons

modified theorem list.sorted_nil

modified theorem list.sorted_of_sorted_cons

modified theorem list.sorted_singleton

Modified data/nat/pairing.lean

added theorem nat.mkpair_unpair'

Modified data/option.lean

modified def option.filter

added def option.guard

added theorem option.guard_eq_some

modified def option.iget

added theorem option.mem_def

added theorem option.some_inj

Modified data/prod.lean

added theorem prod.swap_left_inverse

added theorem prod.swap_right_inverse

Modified data/rat.lean

Modified data/seq/wseq.lean

Modified data/set/basic.lean

modified theorem set.ball_image_iff

added theorem set.compl_image

modified theorem set.forall_range_iff

modified theorem set.image_eq_preimage_of_inverse

added theorem set.image_preimage_eq

deleted theorem set.image_subset_eq

added theorem set.image_subset_preimage_of_inverse

deleted theorem set.image_union_supset

deleted theorem set.inter_preimage_subset

modified theorem set.mem_image

added theorem set.mem_image_iff_bex

modified theorem set.mem_image_iff_of_inverse

modified theorem set.mem_of_eq_of_mem

modified def set.pairwise_on

deleted theorem set.preimage_diff

modified theorem set.preimage_image_eq

added theorem set.preimage_subset_image_of_inverse

modified theorem set.range_of_surjective

modified theorem set.subset.trans

modified theorem set.subset_preimage_image

deleted theorem set.union_preimage_subset

Modified data/set/countable.lean

modified def set.countable

deleted def set.encodable_of_inj

Modified data/set/enumerate.lean

Deleted data/set/function.lean

deleted theorem set.bij_on.mk

deleted def set.bij_on

deleted theorem set.bij_on_comp

deleted theorem set.bij_on_of_eq_on

deleted theorem set.bij_on_of_inv_on

deleted theorem set.bijective_iff_bij_on_univ

deleted theorem set.eq_on_of_left_inv_of_right_inv

deleted theorem set.image_eq_of_bij_on

deleted theorem set.image_eq_of_maps_to_of_surj_on

deleted theorem set.image_subset_of_maps_to

deleted theorem set.image_subset_of_maps_to_of_subset

deleted def set.inj_on

deleted theorem set.inj_on_comp

deleted theorem set.inj_on_empty

deleted theorem set.inj_on_of_bij_on

deleted theorem set.inj_on_of_eq_on

deleted theorem set.inj_on_of_inj_on_of_subset

deleted theorem set.inj_on_of_left_inv_on

deleted theorem set.injective_iff_inj_on_univ

deleted def set.inv_on

deleted def set.left_inv_on

deleted theorem set.left_inv_on_comp

deleted theorem set.left_inv_on_of_eq_on_left

deleted theorem set.left_inv_on_of_eq_on_right

deleted theorem set.left_inv_on_of_surj_on_right_inv_on

deleted def set.maps_to

deleted theorem set.maps_to_comp

deleted theorem set.maps_to_of_bij_on

deleted theorem set.maps_to_of_eq_on

deleted theorem set.maps_to_univ_univ

deleted def set.right_inv_on

deleted theorem set.right_inv_on_comp

deleted theorem set.right_inv_on_of_eq_on_left

deleted theorem set.right_inv_on_of_eq_on_right

deleted theorem set.right_inv_on_of_inj_on_of_left_inv_on

deleted def set.surj_on

deleted theorem set.surj_on_comp

deleted theorem set.surj_on_of_bij_on

deleted theorem set.surj_on_of_eq_on

deleted theorem set.surj_on_of_right_inv_on

deleted theorem set.surjective_iff_surj_on_univ

Modified data/set/prod.lean

added theorem set.mem_prod

modified theorem set.mem_prod_eq

Modified logic/basic.lean

added theorem and_iff_left_of_imp

added theorem and_iff_right_of_imp

added theorem exists_and_distrib_right

added theorem heq_iff_eq

added theorem sigma.exists

added theorem sigma.forall

added theorem sigma.mk.inj_iff

added theorem subtype.exists

added theorem subtype.forall

Renamed logic/function_inverse.lean to logic/function.lean

added theorem function.injective.eq_iff

added theorem function.injective.has_left_inverse

added theorem function.injective_surj_inv

added theorem function.inv_fun_eq

added theorem function.inv_fun_eq_of_injective_of_right_inverse

added theorem function.inv_fun_on_eq'

added theorem function.inv_fun_on_eq

added theorem function.inv_fun_on_mem

added theorem function.inv_fun_on_neg

added theorem function.inv_fun_on_pos

added theorem function.left_inverse_inv_fun

added theorem function.partial_inv_eq

added theorem function.partial_inv_eq_of_eq

added theorem function.right_inverse_inv_fun

added theorem function.right_inverse_surj_inv

added theorem function.surj_inv_eq

added theorem function.surjective.has_right_inverse

deleted theorem set.has_left_inverse

deleted theorem set.has_right_inverse

deleted theorem set.injective_surj_inv

deleted def set.inv_fun

deleted theorem set.inv_fun_eq

deleted theorem set.inv_fun_eq_of_injective_of_right_inverse

deleted def set.inv_fun_on

deleted theorem set.inv_fun_on_eq'

deleted theorem set.inv_fun_on_eq

deleted theorem set.inv_fun_on_mem

deleted theorem set.inv_fun_on_neg

deleted theorem set.inv_fun_on_pos

deleted theorem set.left_inverse_inv_fun

deleted theorem set.right_inverse_inv_fun

deleted theorem set.right_inverse_surj_inv

deleted def set.surj_inv

deleted theorem set.surj_inv_eq

Modified order/filter.lean

Modified tactic/interactive.lean

Modified tactic/rcases.lean