Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-07-23 18:29 5816424b

View on Github →

refactor(*): use 'lemma' iff statement is private

Estimated changes

Modified algebra/lattice/basic.lean

modified theorem lattice.bot_inf_eq

modified theorem lattice.bot_le

modified theorem lattice.bot_sup_eq

modified theorem lattice.bot_unique

modified theorem lattice.eq_bot_iff

modified theorem lattice.eq_top_iff

modified theorem lattice.inf_assoc

modified theorem lattice.inf_bot_eq

modified theorem lattice.inf_comm

modified theorem lattice.inf_eq_top_iff

modified theorem lattice.inf_idem

modified theorem lattice.inf_le_inf

modified theorem lattice.inf_le_left'

modified theorem lattice.inf_le_left

modified theorem lattice.inf_le_left_of_le

modified theorem lattice.inf_le_right'

modified theorem lattice.inf_le_right

modified theorem lattice.inf_le_right_of_le

modified theorem lattice.inf_of_le_left

modified theorem lattice.inf_of_le_right

modified theorem lattice.inf_sup_self

modified theorem lattice.inf_top_eq

modified theorem lattice.le_bot_iff

modified theorem lattice.le_inf

modified theorem lattice.le_inf_iff

modified theorem lattice.le_inf_sup

modified theorem lattice.le_of_inf_eq

modified theorem lattice.le_of_sup_eq

modified theorem lattice.le_sup_left'

modified theorem lattice.le_sup_left

modified theorem lattice.le_sup_left_of_le

modified theorem lattice.le_sup_right'

modified theorem lattice.le_sup_right

modified theorem lattice.le_sup_right_of_le

modified theorem lattice.le_top

modified theorem lattice.neq_bot_of_le_neq_bot

modified theorem lattice.sup_assoc

modified theorem lattice.sup_bot_eq

modified theorem lattice.sup_comm

modified theorem lattice.sup_eq_bot_iff

modified theorem lattice.sup_idem

modified theorem lattice.sup_inf_le

modified theorem lattice.sup_inf_self

modified theorem lattice.sup_le

modified theorem lattice.sup_le_iff

modified theorem lattice.sup_le_sup

modified theorem lattice.sup_of_le_left

modified theorem lattice.sup_of_le_right

modified theorem lattice.sup_top_eq

modified theorem lattice.top_inf_eq

modified theorem lattice.top_le_iff

modified theorem lattice.top_sup_eq

modified theorem lattice.top_unique

modified theorem le_antisymm'

Modified algebra/lattice/boolean_algebra.lean

modified theorem lattice.inf_neg_eq_bot

modified theorem lattice.inf_sup_left

modified theorem lattice.inf_sup_right

modified theorem lattice.le_neg_of_le_neg

modified theorem lattice.le_sup_inf

modified theorem lattice.neg_bot

modified theorem lattice.neg_eq_neg_iff

modified theorem lattice.neg_eq_neg_of_eq

modified theorem lattice.neg_inf

modified theorem lattice.neg_inf_eq_bot

modified theorem lattice.neg_le_iff_neg_le

modified theorem lattice.neg_le_neg

modified theorem lattice.neg_le_neg_iff_le

modified theorem lattice.neg_le_of_neg_le

modified theorem lattice.neg_neg

modified theorem lattice.neg_sup

modified theorem lattice.neg_sup_eq_top

modified theorem lattice.neg_top

modified theorem lattice.neg_unique

modified theorem lattice.sub_eq

modified theorem lattice.sub_eq_left

modified theorem lattice.sup_inf_left

modified theorem lattice.sup_inf_right

modified theorem lattice.sup_neg_eq_top

modified theorem lattice.sup_sub_same

Modified algebra/lattice/bounded_lattice.lean

modified theorem lattice.monotone_and

modified theorem lattice.monotone_or

Modified algebra/lattice/complete_boolean_algebra.lean

modified theorem lattice.inf_Sup_eq

modified theorem lattice.neg_Inf

modified theorem lattice.neg_Sup

modified theorem lattice.neg_infi

modified theorem lattice.neg_supr

modified theorem lattice.sup_Inf_eq

Modified algebra/lattice/complete_lattice.lean

modified theorem lattice.Inf_empty

modified theorem lattice.Inf_eq_infi

modified theorem lattice.Inf_image

modified theorem lattice.Inf_insert

modified theorem lattice.Inf_le

modified theorem lattice.Inf_le_Inf

modified theorem lattice.Inf_le_Sup

modified theorem lattice.Inf_le_iff

modified theorem lattice.Inf_le_of_le

modified theorem lattice.Inf_singleton

modified theorem lattice.Inf_union

modified theorem lattice.Inf_univ

modified theorem lattice.Sup_empty

modified theorem lattice.Sup_eq_supr

modified theorem lattice.Sup_image

modified theorem lattice.Sup_insert

modified theorem lattice.Sup_inter_le

modified theorem lattice.Sup_le

modified theorem lattice.Sup_le_Sup

modified theorem lattice.Sup_singleton

modified theorem lattice.Sup_union

modified theorem lattice.Sup_univ

modified theorem lattice.foo'

modified theorem lattice.foo

modified theorem lattice.infi_and

modified theorem lattice.infi_comm

modified theorem lattice.infi_congr_Prop

modified theorem lattice.infi_const

modified theorem lattice.infi_empty

modified theorem lattice.infi_emptyset

modified theorem lattice.infi_exists

modified theorem lattice.infi_false

modified theorem lattice.infi_inf_eq

modified theorem lattice.infi_infi_eq_left

modified theorem lattice.infi_infi_eq_right

modified theorem lattice.infi_insert

modified theorem lattice.infi_le'

modified theorem lattice.infi_le

modified theorem lattice.infi_le_infi2

modified theorem lattice.infi_le_infi

modified theorem lattice.infi_le_infi_const

modified theorem lattice.infi_le_of_le

modified theorem lattice.infi_or

modified theorem lattice.infi_prod

modified theorem lattice.infi_sigma

modified theorem lattice.infi_singleton

modified theorem lattice.infi_subtype

modified theorem lattice.infi_sum

modified theorem lattice.infi_true

modified theorem lattice.infi_union

modified theorem lattice.infi_unit

modified theorem lattice.infi_univ

modified theorem lattice.le_Inf

modified theorem lattice.le_Inf_inter

modified theorem lattice.le_Sup

modified theorem lattice.le_Sup_iff

modified theorem lattice.le_Sup_of_le

modified theorem lattice.le_infi

modified theorem lattice.le_infi_iff

modified theorem lattice.le_supr'

modified theorem lattice.le_supr

modified theorem lattice.le_supr_of_le

modified theorem lattice.monotone_Inf_of_monotone

modified theorem lattice.monotone_Sup_of_monotone

modified theorem lattice.supr_and

modified theorem lattice.supr_comm

modified theorem lattice.supr_congr_Prop

modified theorem lattice.supr_const

modified theorem lattice.supr_empty

modified theorem lattice.supr_emptyset

modified theorem lattice.supr_exists

modified theorem lattice.supr_false

modified theorem lattice.supr_insert

modified theorem lattice.supr_le

modified theorem lattice.supr_le_iff

modified theorem lattice.supr_le_supr2

modified theorem lattice.supr_le_supr

modified theorem lattice.supr_le_supr_const

modified theorem lattice.supr_or

modified theorem lattice.supr_prod

modified theorem lattice.supr_sigma

modified theorem lattice.supr_singleton

modified theorem lattice.supr_subtype

modified theorem lattice.supr_sum

modified theorem lattice.supr_sup_eq

modified theorem lattice.supr_supr_eq_left

modified theorem lattice.supr_supr_eq_right

modified theorem lattice.supr_true

modified theorem lattice.supr_union

modified theorem lattice.supr_unit

modified theorem lattice.supr_univ

Modified algebra/lattice/filter.lean

modified theorem Union_subset_Union2

modified theorem Union_subset_Union

modified theorem Union_subset_Union_const

modified theorem compl_image_set_of

modified theorem diff_empty

modified theorem diff_neq_empty

modified theorem directed_of_chain

modified theorem directed_on_Union

modified theorem eq_of_sup_eq_inf_eq

modified theorem filter.Inf_sets_eq_finite

modified theorem filter.Inter_mem_sets

modified theorem filter.bind_mono2

modified theorem filter.bind_mono

modified theorem filter.bind_sup

modified theorem filter.binfi_sup_eq

modified theorem filter.empty_in_sets_eq_bot

modified theorem filter.exists_sets_subset_iff

modified theorem filter.exists_ultrafilter

modified theorem filter.filter_eq

modified theorem filter.filter_eq_bot_of_not_nonempty

modified theorem filter.fmap_principal

modified theorem filter.forall_sets_neq_empty_iff_neq_bot

modified theorem filter.image_mem_map

modified theorem filter.inf_principal

modified theorem filter.infi_neq_bot_iff_of_directed

modified theorem filter.infi_neq_bot_of_directed

modified theorem filter.infi_sets_eq'

modified theorem filter.infi_sets_eq

modified theorem filter.infi_sets_induct

modified theorem filter.infi_sup_eq

modified theorem filter.inhabited_of_mem_sets

modified theorem filter.inter_mem_sets

modified theorem filter.join_principal_eq_Sup

modified theorem filter.le_lift'

modified theorem filter.le_map_vmap

modified theorem filter.le_of_ultrafilter

modified theorem filter.le_principal_iff

modified theorem filter.le_vmap_iff_map_le

modified theorem filter.le_vmap_map

modified theorem filter.lift'_cong

modified theorem filter.lift'_id

modified theorem filter.lift'_inf_principal_eq

modified theorem filter.lift'_infi

modified theorem filter.lift'_lift'_assoc

modified theorem filter.lift'_lift_assoc

modified theorem filter.lift'_mono'

modified theorem filter.lift'_mono

modified theorem filter.lift'_neq_bot_iff

modified theorem filter.lift'_principal

modified theorem filter.lift_assoc

modified theorem filter.lift_comm

modified theorem filter.lift_infi'

modified theorem filter.lift_infi

modified theorem filter.lift_lift'_assoc

modified theorem filter.lift_lift'_same_eq_lift'

modified theorem filter.lift_lift'_same_le_lift'

modified theorem filter.lift_lift_same_eq_lift

modified theorem filter.lift_lift_same_le_lift

modified theorem filter.lift_mono'

modified theorem filter.lift_mono

modified theorem filter.lift_neq_bot_iff

modified theorem filter.lift_principal

modified theorem filter.lift_sets_eq

modified theorem filter.map_binfi_eq

modified theorem filter.map_bot

modified theorem filter.map_compose

modified theorem filter.map_eq_bot_iff

modified theorem filter.map_eq_vmap_of_inverse

modified theorem filter.map_id

modified theorem filter.map_infi_eq

modified theorem filter.map_infi_le

modified theorem filter.map_lift'_eq2

modified theorem filter.map_lift'_eq

modified theorem filter.map_lift_eq2

modified theorem filter.map_lift_eq

modified theorem filter.map_mono

modified theorem filter.map_principal

modified theorem filter.map_sup

modified theorem filter.map_swap_vmap_swap_eq

modified theorem filter.map_vmap_le

modified theorem filter.mem_bind_sets

modified theorem filter.mem_bot_sets

modified theorem filter.mem_inf_sets

modified theorem filter.mem_inf_sets_of_left

modified theorem filter.mem_inf_sets_of_right

modified theorem filter.mem_infi_sets

modified theorem filter.mem_join_sets

modified theorem filter.mem_lift'

modified theorem filter.mem_lift'_iff

modified theorem filter.mem_lift

modified theorem filter.mem_lift_iff

modified theorem filter.mem_map

modified theorem filter.mem_of_finite_Union_ultrafilter

modified theorem filter.mem_of_finite_sUnion_ultrafilter

modified theorem filter.mem_or_compl_mem_of_ultrafilter

modified theorem filter.mem_or_mem_of_ultrafilter

modified theorem filter.mem_principal_sets

modified theorem filter.mem_prod_iff

modified theorem filter.mem_prod_same_iff

modified theorem filter.mem_pure

modified theorem filter.mem_return_sets

modified theorem filter.mem_sets_of_neq_bot

modified theorem filter.mem_sup_sets

modified theorem filter.mem_top_sets_iff

modified theorem filter.mem_vmap_of_mem

modified theorem filter.monotone_lift'

modified theorem filter.monotone_lift

modified theorem filter.monotone_map

modified theorem filter.monotone_mem_sets

modified theorem filter.monotone_principal

modified theorem filter.monotone_vmap

modified theorem filter.principal_bind

modified theorem filter.principal_empty

modified theorem filter.principal_eq_bot_iff

modified theorem filter.principal_eq_iff_eq

modified theorem filter.principal_le_lift'

modified theorem filter.principal_mono

modified theorem filter.principal_univ

modified theorem filter.prod_comm

modified theorem filter.prod_inf_prod

modified theorem filter.prod_lift'_lift'

modified theorem filter.prod_lift_lift

modified theorem filter.prod_map_map_eq

modified theorem filter.prod_mem_prod

modified theorem filter.prod_mono

modified theorem filter.prod_neq_bot

modified theorem filter.prod_principal_principal

modified theorem filter.prod_same_eq

modified theorem filter.prod_vmap_vmap_eq

modified theorem filter.return_neq_bot

modified theorem filter.seq_mono

modified theorem filter.sup_join

modified theorem filter.sup_principal

modified theorem filter.supr_join

modified theorem filter.supr_map

modified theorem filter.supr_principal

modified theorem filter.supr_sets_eq

modified theorem filter.ultrafilter_map

modified theorem filter.ultrafilter_of_le

modified theorem filter.ultrafilter_of_spec

modified theorem filter.ultrafilter_of_split

modified theorem filter.ultrafilter_of_ultrafilter

modified theorem filter.ultrafilter_pure

modified theorem filter.ultrafilter_ultrafilter_of

modified theorem filter.ultrafilter_unique

modified theorem filter.univ_mem_sets'

modified theorem filter.univ_mem_sets

modified theorem filter.vimage_mem_vmap

modified theorem filter.vmap_eq_lift'

modified theorem filter.vmap_lift'_eq2

modified theorem filter.vmap_lift'_eq

modified theorem filter.vmap_lift_eq2

modified theorem filter.vmap_lift_eq

modified theorem filter.vmap_map

modified theorem filter.vmap_mono

modified theorem filter.vmap_neq_bot

modified theorem filter.vmap_neq_bot_of_surj

modified theorem filter.vmap_principal

modified theorem filter.vmap_vmap_comp

modified theorem implies_implies_true_iff

modified theorem inf_eq_bot_iff_le_compl

modified theorem lattice.Inf_eq_finite_sets

modified theorem lattice.Sup_le_iff

modified theorem neg_subset_neg_iff_subset

modified theorem not_not_mem_iff

modified theorem prod.fst_swap

modified theorem prod.mk.eta

modified theorem prod.snd_swap

modified theorem prod.swap_prod_mk

modified theorem prod.swap_swap

modified theorem prod.swap_swap_eq

modified theorem pure_seq_eq_map

modified theorem sUnion_eq_Union

modified theorem sUnion_mono

modified theorem set.diff_right_antimono

modified theorem set.fmap_eq_image

modified theorem set.image_eq_vimage_of_inverse

modified theorem set.image_swap_eq_vimage_swap

modified theorem set.image_swap_prod

modified theorem set.mem_image_iff_of_inverse

modified theorem set.mem_prod_eq

modified theorem set.mem_seq_iff

modified theorem set.monotone_inter

modified theorem set.monotone_prod

modified theorem set.monotone_set_of

modified theorem set.prod_image_image_eq

modified theorem set.prod_inter_prod

modified theorem set.prod_mk_mem_set_prod_eq

modified theorem set.prod_mono

modified theorem set.prod_neq_empty_iff

modified theorem set.prod_singleton_singleton

modified theorem set.prod_vimage_eq

modified theorem set.set_of_mem_eq

modified theorem set.vimage_set_of_eq

modified theorem singleton_neq_emptyset

Modified algebra/lattice/fixed_points.lean

modified theorem ge_of_eq

modified theorem lattice.gfp_comp

modified theorem lattice.gfp_eq

modified theorem lattice.gfp_gfp

modified theorem lattice.gfp_induct

modified theorem lattice.gfp_le

modified theorem lattice.le_gfp

modified theorem lattice.le_lfp

modified theorem lattice.lfp_comp

modified theorem lattice.lfp_eq

modified theorem lattice.lfp_induct

modified theorem lattice.lfp_le

modified theorem lattice.lfp_lfp

modified theorem lattice.monotone_gfp

modified theorem lattice.monotone_lfp

Modified algebra/lattice/zorn.lean

modified theorem zorn.chain_chain_closure

modified theorem zorn.chain_closure_closure

modified theorem zorn.chain_closure_empty

modified theorem zorn.chain_closure_succ_fixpoint

modified theorem zorn.chain_closure_succ_fixpoint_iff

modified theorem zorn.chain_closure_total

modified theorem zorn.chain_insert

modified theorem zorn.chain_succ

modified theorem zorn.max_chain_spec

modified theorem zorn.succ_increasing

modified theorem zorn.succ_spec

modified theorem zorn.super_of_not_max

modified theorem zorn.zorn

modified theorem zorn.zorn_weak_order

Modified algebra/order.lean

modified theorem comp_le_comp_left_of_monotone

modified theorem le_dual_eq_le

modified theorem monotone_app

modified theorem monotone_comp

modified theorem monotone_const

modified theorem monotone_id

modified theorem monotone_lam

Modified data/bitvec.lean

modified theorem bitvec.bits_to_nat_to_list

modified theorem bitvec.of_nat_succ

Modified data/bool.lean

modified theorem bool.bxor_assoc

modified theorem bool.bxor_comm

modified theorem bool.bxor_ff

modified theorem bool.bxor_left_comm

modified theorem bool.bxor_self

modified theorem bool.bxor_tt

modified theorem bool.ff_bxor

modified theorem bool.ff_bxor_ff

modified theorem bool.ff_bxor_tt

modified theorem bool.tt_bxor

modified theorem bool.tt_bxor_ff

modified theorem bool.tt_bxor_tt

Modified data/fin.lean

modified theorem eq_of_lt_succ_of_not_lt

modified theorem lt_succ_of_lt

Modified data/hash_map.lean

modified theorem bucket_array.foldl_eq_lem

deleted theorem hash_map.append_of_modify_aux

deleted theorem hash_map.insert_lemma

added theorem hash_map.insert_theorem

deleted theorem hash_map.valid.modify_aux1

deleted theorem hash_map.valid.modify_aux2

deleted theorem hash_map.valid_aux.insert_lemma1

Modified data/int/basic.lean

modified theorem int.neg_add_neg

Modified data/list/basic.lean

modified theorem list.cons_inj

modified theorem list.cons_ne_nil

modified theorem list.count_append

modified theorem list.count_concat

modified theorem list.count_cons'

modified theorem list.count_cons

modified theorem list.count_cons_ge_count

modified theorem list.count_cons_of_ne

modified theorem list.count_cons_self

modified theorem list.count_eq_zero_of_not_mem

modified theorem list.count_nil

modified theorem list.count_pos_of_mem

modified theorem list.count_singleton

modified theorem list.head_eq_of_cons_eq

modified theorem list.index_of_le_length

modified theorem list.index_of_lt_length

modified theorem list.ith_succ

modified theorem list.ith_zero

modified theorem list.last_cons_cons

modified theorem list.last_singleton

modified theorem list.length_taken_le

modified theorem list.mem_iff_count_pos

modified theorem list.mem_of_count_pos

modified theorem list.not_mem_of_count_eq_zero

modified theorem list.not_mem_of_index_of_eq_length

modified theorem list.tail_eq_of_cons_eq

modified theorem list.taken_all

modified theorem list.taken_all_of_ge

modified theorem list.taken_cons

modified theorem list.taken_nil

modified theorem list.taken_zero

Modified data/list/comb.lean

modified theorem list.dmap_cons_of_neg

modified theorem list.dmap_cons_of_pos

modified theorem list.dmap_nil

modified theorem list.exists_of_mem_dmap

modified theorem list.map_dmap_of_inv_of_pos

modified theorem list.mem_dmap

modified theorem list.mem_of_dinj_of_mem_dmap

modified theorem list.not_mem_dmap_of_dinj_of_not_mem

Modified data/list/perm.lean

modified theorem list.perm.perm_insert_insert

modified theorem list.perm.perm_of_qeq

Modified data/list/set.lean

modified theorem list.disjoint.comm

modified theorem list.disjoint_append_of_disjoint_left

modified theorem list.disjoint_cons_of_not_mem_of_disjoint

modified theorem list.disjoint_left

modified theorem list.disjoint_nil_left

modified theorem list.disjoint_nil_right

modified theorem list.disjoint_of_disjoint_append_left_left

modified theorem list.disjoint_of_disjoint_append_left_right

modified theorem list.disjoint_of_disjoint_append_right_left

modified theorem list.disjoint_of_disjoint_append_right_right

modified theorem list.disjoint_of_disjoint_cons_left

modified theorem list.disjoint_of_disjoint_cons_right

modified theorem list.disjoint_of_subset_left

modified theorem list.disjoint_of_subset_right

modified theorem list.disjoint_right

modified theorem list.dmap_nodup_of_dinj

modified theorem list.erase_append_left

modified theorem list.erase_append_right

modified theorem list.erase_cons

modified theorem list.erase_cons_head

modified theorem list.erase_cons_tail

modified theorem list.erase_nil

modified theorem list.erase_of_not_mem

modified theorem list.erase_sublist

modified theorem list.erase_subset

modified theorem list.length_erase_of_mem

modified theorem list.upto_step

Modified data/list/sort.lean

modified theorem nat.lt_succ_iff_le

modified theorem nat.succ_le_succ_iff

Modified data/nat/basic.lean

modified theorem nat.addl_succ_left

modified theorem nat.addl_zero_left

modified theorem nat.one_succ_zero

modified theorem nat.zero_has_zero

Modified data/nat/gcd.lean

modified theorem nat.gcd_eq_one_of_coprime

Modified data/nat/sub.lean

modified theorem nat.dist_pos_of_ne

modified theorem nat.dist_succ_succ

Modified data/num/lemmas.lean

modified theorem num.bitwise_to_nat

modified theorem num.land_to_nat

modified theorem num.ldiff_to_nat

modified theorem num.lor_to_nat

modified theorem num.lxor_to_nat

modified theorem num.shiftl_to_nat

modified theorem num.shiftr_to_nat

modified theorem num.test_bit_to_nat

deleted theorem pos_num.cmp_dec_lemma

added theorem pos_num.cmp_dec_theorem

Modified data/rat.lean

modified theorem linear_order_cases_on_eq

modified theorem linear_order_cases_on_gt

modified theorem linear_order_cases_on_lt

modified theorem mul_nonneg_iff_right_nonneg_of_pos

modified theorem not_antimono

Modified data/seq/computation.lean

modified theorem computation.destruct_map

modified theorem computation.eq_of_bisim

modified theorem computation.lift_rel_rec.lem

modified theorem computation.map_comp

modified theorem computation.map_ret'

modified theorem computation.map_ret

modified theorem computation.map_think'

modified theorem computation.map_think

modified theorem computation.ret_bind

modified theorem computation.return_def

modified theorem computation.think_bind

Modified data/seq/parallel.lean

modified theorem computation.map_parallel

modified theorem computation.parallel_congr_lem

modified theorem computation.terminates_parallel.aux

Modified data/seq/seq.lean

modified theorem seq.append_assoc

modified theorem seq.append_nil

modified theorem seq.coinduction2

modified theorem seq.coinduction

modified theorem seq.cons_append

modified theorem seq.eq_of_bisim

modified theorem seq.eq_or_mem_of_mem_cons

modified theorem seq.exists_of_mem_map

modified theorem seq.join_append

modified theorem seq.join_cons

modified theorem seq.join_cons_cons

modified theorem seq.join_cons_nil

modified theorem seq.join_nil

modified theorem seq.map_comp

modified theorem seq.map_cons

modified theorem seq.map_id

modified theorem seq.map_nil

modified theorem seq.map_nth

modified theorem seq.map_tail

modified theorem seq.mem_cons

modified theorem seq.mem_cons_iff

modified theorem seq.mem_cons_of_mem

modified theorem seq.nil_append

modified theorem seq1.join_cons

modified theorem seq1.join_nil

Modified data/seq/wseq.lean

modified theorem wseq.append_assoc

modified theorem wseq.append_nil

modified theorem wseq.cons_append

modified theorem wseq.destruct_append

modified theorem wseq.destruct_join

modified theorem wseq.destruct_map

modified theorem wseq.exists_of_mem_map

modified theorem wseq.join_append

modified theorem wseq.map_comp

modified theorem wseq.map_cons

modified theorem wseq.map_nil

modified theorem wseq.map_think

modified theorem wseq.nil_append

modified theorem wseq.think_append

Modified data/set/basic.lean

modified theorem set.set_of_false

Modified data/set/finite.lean

modified theorem set.finite_image

modified theorem set.finite_insert

modified theorem set.finite_sUnion

modified theorem set.finite_singleton

modified theorem set.finite_subset

modified theorem set.finite_union

Modified data/stream.lean

modified theorem stream.all_def

modified theorem stream.any_def

modified theorem stream.append_append_stream

modified theorem stream.append_approx_drop

modified theorem stream.append_stream_head_tail

modified theorem stream.approx_succ

modified theorem stream.approx_zero

modified theorem stream.bisim_simple

modified theorem stream.coinduction

modified theorem stream.composition

modified theorem stream.cons_append_stream

modified theorem stream.cons_nth_inits_core

modified theorem stream.const_eq

modified theorem stream.corec'_eq

modified theorem stream.corec_def

modified theorem stream.corec_eq

modified theorem stream.corec_id_f_eq_iterate

modified theorem stream.corec_id_id_eq_const

modified theorem stream.cycle_eq

modified theorem stream.cycle_singleton

modified theorem stream.drop_append_stream

modified theorem stream.drop_const

modified theorem stream.drop_drop

modified theorem stream.drop_map

modified theorem stream.drop_succ

modified theorem stream.drop_zip

modified theorem stream.eq_of_bisim

modified theorem stream.eq_or_mem_of_mem_cons

modified theorem stream.even_cons_cons

modified theorem stream.even_interleave

modified theorem stream.even_tail

modified theorem stream.exists_of_mem_map

modified theorem stream.head_cons

modified theorem stream.head_even

modified theorem stream.head_iterate

modified theorem stream.head_map

modified theorem stream.head_zip

modified theorem stream.homomorphism

modified theorem stream.identity

modified theorem stream.inits_core_eq

modified theorem stream.inits_eq

modified theorem stream.inits_tail

modified theorem stream.interchange

modified theorem stream.interleave_eq

modified theorem stream.interleave_even_odd

modified theorem stream.interleave_tail_tail

modified theorem stream.iterate_eq

modified theorem stream.iterate_id

modified theorem stream.map_append_stream

modified theorem stream.map_cons

modified theorem stream.map_const

modified theorem stream.map_eq

modified theorem stream.map_eq_apply

modified theorem stream.map_id

modified theorem stream.map_iterate

modified theorem stream.map_map

modified theorem stream.map_tail

modified theorem stream.mem_append_stream_left

modified theorem stream.mem_append_stream_right

modified theorem stream.mem_cons

modified theorem stream.mem_cons_of_mem

modified theorem stream.mem_const

modified theorem stream.mem_cycle

modified theorem stream.mem_interleave_left

modified theorem stream.mem_interleave_right

modified theorem stream.mem_map

modified theorem stream.mem_of_mem_even

modified theorem stream.mem_of_mem_odd

modified theorem stream.mem_of_nth_eq

modified theorem stream.nats_eq

modified theorem stream.nil_append_stream

modified theorem stream.nth_approx

modified theorem stream.nth_const

modified theorem stream.nth_drop

modified theorem stream.nth_even

modified theorem stream.nth_inits

modified theorem stream.nth_interleave_left

modified theorem stream.nth_interleave_right

modified theorem stream.nth_map

modified theorem stream.nth_nats

modified theorem stream.nth_odd

modified theorem stream.nth_of_bisim

modified theorem stream.nth_succ

modified theorem stream.nth_succ_iterate

modified theorem stream.nth_tails

modified theorem stream.nth_unfolds_head_tail

modified theorem stream.nth_zero_cons

modified theorem stream.nth_zero_iterate

modified theorem stream.nth_zip

modified theorem stream.odd_eq

modified theorem stream.tail_cons

modified theorem stream.tail_const

modified theorem stream.tail_drop

modified theorem stream.tail_eq_drop

modified theorem stream.tail_even

modified theorem stream.tail_inits

modified theorem stream.tail_interleave

modified theorem stream.tail_iterate

modified theorem stream.tail_map

modified theorem stream.tail_zip

modified theorem stream.tails_eq

modified theorem stream.tails_eq_iterate

deleted theorem stream.take_lemma

added theorem stream.take_theorem

modified theorem stream.unfolds_eq

modified theorem stream.unfolds_head_eq

modified theorem stream.zip_eq

modified theorem stream.zip_inits_tails

Modified data/vector.lean

modified theorem vector.map_cons

modified theorem vector.map_nil

modified theorem vector.to_list_append

modified theorem vector.to_list_cons

modified theorem vector.to_list_drop

modified theorem vector.to_list_length

modified theorem vector.to_list_mk

modified theorem vector.to_list_nil

modified theorem vector.to_list_take

Modified logic/basic.lean

modified theorem eq_iff_le_and_le

modified theorem forall_eq

modified theorem not_imp_iff_not_imp

modified theorem or_imp_iff_and_imp

modified theorem or_of_not_implies'

modified theorem or_of_not_implies

modified theorem prod.exists

modified theorem prod.forall

modified theorem prod.mk.inj_iff

modified theorem set_of_subset_set_of

Modified tactic/converter/binders.lean

modified theorem Inf_image

modified theorem Sup_image

modified theorem mem_image

modified theorem {u

Modified tests/examples.lean

modified theorem mem_set_of

Modified tests/finish2.lean

modified theorem NoMember

Modified topology/continuity.lean

modified theorem closure_prod_eq

modified theorem compact_pi_infinite

modified theorem continuous_Inf_dom

modified theorem continuous_Inf_rng

modified theorem continuous_Prop

modified theorem continuous_bot

modified theorem continuous_coinduced_dom

modified theorem continuous_coinduced_rng

modified theorem continuous_compose

modified theorem continuous_eq_le_coinduced

modified theorem continuous_fst

modified theorem continuous_generated_from

modified theorem continuous_id

modified theorem continuous_iff_induced_le

modified theorem continuous_iff_towards

modified theorem continuous_induced_dom

modified theorem continuous_induced_rng

modified theorem continuous_inf_dom

modified theorem continuous_inf_rng_left

modified theorem continuous_inf_rng_right

modified theorem continuous_infi_dom

modified theorem continuous_infi_rng

modified theorem continuous_inl

modified theorem continuous_inr

modified theorem continuous_prod_mk

modified theorem continuous_snd

modified theorem continuous_subtype_mk

modified theorem continuous_subtype_nhds_cover

modified theorem continuous_subtype_val

modified theorem continuous_sum_rec

modified theorem continuous_sup_dom_left

modified theorem continuous_sup_dom_right

modified theorem continuous_sup_rng

modified theorem continuous_top

modified theorem false_neq_true

modified theorem map_nhds_induced_eq

modified theorem map_nhds_subtype_val_eq

modified theorem nhds_induced_eq_vmap

modified theorem nhds_pi

modified theorem nhds_prod_eq

modified theorem open_induced

modified theorem open_set_prod

modified theorem open_singleton_true

modified theorem prod_eq_generate_from

modified theorem subtype.val_image

modified theorem univ_eq_true_false

Modified topology/topological_space.lean

modified theorem closed_Inter

modified theorem closed_Union_of_locally_finite

modified theorem closed_closure

modified theorem closed_compl_iff_open

modified theorem closed_empty

modified theorem closed_iff_nhds

modified theorem closed_sInter

modified theorem closed_union

modified theorem closed_univ

modified theorem closure_closure

modified theorem closure_compl_eq

modified theorem closure_empty

modified theorem closure_eq_compl_interior_compl

modified theorem closure_eq_iff_closed

modified theorem closure_eq_nhds

modified theorem closure_eq_of_closed

modified theorem closure_minimal

modified theorem closure_mono

modified theorem closure_subset_iff_subset_of_closed

modified theorem closure_union

modified theorem closure_univ

modified theorem compact_adherence_nhdset

modified theorem compact_iff_ultrafilter_le_nhds

modified theorem eq_of_nhds_eq_nhds

modified theorem eq_of_nhds_neq_bot

modified theorem finite_subcover_of_compact

modified theorem generate_from_le

modified theorem interior_compl_eq

modified theorem interior_empty

modified theorem interior_eq_iff_open

modified theorem interior_eq_nhds

modified theorem interior_eq_of_open

modified theorem interior_inter

modified theorem interior_interior

modified theorem interior_maximal

modified theorem interior_mono

modified theorem interior_subset

modified theorem interior_subset_closure

modified theorem interior_union_closed_of_interior_empty

modified theorem interior_univ

modified theorem le_of_nhds_le_nhds

modified theorem map_nhds

modified theorem mem_nhds_sets

modified theorem mem_nhds_sets_iff

modified theorem nhds_mono

modified theorem nhds_neq_bot

modified theorem nhds_sets

modified theorem nhds_supr

modified theorem open_Union

modified theorem open_compl_iff_closed

modified theorem open_diff

modified theorem open_empty

modified theorem open_iff_nhds

modified theorem open_inter

modified theorem open_interior

modified theorem open_sUnion

modified theorem open_univ

modified theorem return_le_nhds

modified theorem subset_closure

modified theorem subset_interior_iff_subset_of_open

modified theorem sup_eq_generate_from

modified theorem supr_eq_generate_from

modified theorem t2_space_top

modified theorem topological_space.nhds_generate_from

modified theorem topological_space_eq

Modified topology/uniform_space.lean

modified theorem Cauchy.monotone_gen

modified theorem Cauchy.pure_cauchy_dense

modified theorem Cauchy.uniform_embedding_pure_cauchy

modified theorem cauchy_downwards

modified theorem cauchy_map

modified theorem cauchy_nhds

modified theorem cauchy_of_totally_bounded_of_ultrafilter

modified theorem cauchy_pure

modified theorem cauchy_vmap

modified theorem closure_eq_inter_uniformity

modified theorem comp_le_uniformity3

modified theorem comp_le_uniformity

modified theorem comp_mem_uniformity_sets

modified theorem comp_symm_of_uniformity

modified theorem compact_of_totally_bounded_closed

modified theorem compact_of_totally_bounded_complete

modified theorem complete_of_closed

modified theorem complete_space_extension

modified theorem complete_space_separation

modified theorem continuous_of_uniform

modified theorem id_comp_rel

modified theorem interior_mem_uniformity

modified theorem le_nhds_iff_adhp_of_cauchy

modified theorem le_nhds_of_cauchy_adhp

modified theorem lift_nhds_left

modified theorem lift_nhds_right

modified theorem mem_nhds_left

modified theorem mem_nhds_right

modified theorem mem_nhds_uniformity_iff

modified theorem monotone_comp_rel

modified theorem nhds_eq_uniformity

modified theorem nhds_eq_uniformity_prod

modified theorem nhds_nhds_eq_uniformity_uniformity_prod

modified theorem nhdset_of_mem_uniformity

modified theorem prod_mk_mem_comp_rel

modified theorem refl_le_uniformity

modified theorem refl_mem_uniformity

modified theorem separated_equiv

modified theorem supr_uniformity

modified theorem swap_id_rel

modified theorem symm_le_uniformity

modified theorem symm_of_uniformity

modified theorem to_topological_space_bot

modified theorem to_topological_space_mono

modified theorem to_topological_space_supr

modified theorem to_topological_space_top

modified theorem to_topological_space_vmap

modified theorem totally_bounded_iff_filter

modified theorem totally_bounded_iff_ultrafilter

modified theorem uniform_continuous_of_embedding

modified theorem uniform_continuous_quotient_mk

modified theorem uniform_continuous_uniformly_extend

modified theorem uniform_continuous_vmap

modified theorem uniform_space_eq

modified theorem uniformity_eq_symm

modified theorem uniformity_eq_uniformity_closure

modified theorem uniformity_eq_uniformity_interior

modified theorem uniformity_le_symm

modified theorem uniformity_lift_le_comp

modified theorem uniformity_lift_le_swap

modified theorem uniformly_extend_of_emb

modified theorem uniformly_extend_spec

modified theorem uniformly_extend_unique

modified theorem vmap_quotient_le_uniformity