Commit 2022-09-08 18:38 6a081f52

View on Github →

chore: bump std4 09-08 (#403) Lots of stuff moved to std4 in this bump, so many files were removed or shrunk dramatically. In order to avoid too much churn, all the renamed theorems in Mathlib.Init.Logic and Mathlib.Logic.Basic have been turned into alias declarations, which we may clean up later.

Estimated changes

modified theorem Int.cast_eq_cast_iff_Nat
deleted theorem List.eq_of_mem_repeat'
deleted theorem List.get_repeat'
added theorem List.get_replicate
modified theorem List.insert_of_mem
modified theorem List.insert_of_not_mem
modified def List.leftpad
modified theorem List.leftpad_prefix
modified theorem List.mem_insert_iff
modified theorem List.mem_insert_of_mem
modified theorem List.mem_insert_self
deleted theorem List.mem_repeat'
added theorem List.mem_replicate
deleted theorem List.repeat'_succ
added theorem List.replicate_succ
modified theorem List.insert_equiv_cons
deleted theorem Nat.le_pred_of_lt
deleted theorem Nat.le_sub_iff_add_le
deleted theorem Nat.le_zero_iff
deleted theorem Nat.lt_succ_iff
deleted theorem Nat.mul_div_le
deleted theorem Nat.sub_lt_self
deleted theorem Nat.succ_eq_one_add
deleted theorem Nat.succ_inj'
deleted def String.repeat'
added def String.replicate
modified theorem String.leftpad_prefix
deleted theorem String.length_repeat'
deleted def List.after
deleted def List.band
deleted def List.bor
deleted def List.findIdx
deleted theorem List.getLast_cons_cons
deleted theorem List.getLast_singleton
deleted theorem List.get_cons_succ
deleted theorem List.get_cons_zero
deleted def List.indexOf
deleted def List.insert
deleted def List.last!
deleted def List.mapIdx
deleted def List.mapIdxAux
deleted def List.mapIdxM
deleted theorem List.mem_cons
deleted theorem List.not_mem_nil
deleted def List.removeNth
deleted def List.repeat'
deleted def List.tail
deleted theorem List.append_bind
deleted theorem List.ball_cons
deleted theorem List.ball_nil
deleted theorem List.bex_cons
deleted theorem List.cons_bind
deleted theorem List.cons_subset_cons
deleted theorem List.length_drop
deleted theorem List.length_le_of_sublist
deleted theorem List.length_map₂
deleted theorem List.length_removeNth
deleted theorem List.length_repeat'
deleted theorem List.length_tail
deleted theorem List.length_take
deleted theorem List.length_take_le
deleted theorem List.map_append
deleted theorem List.map_cons
deleted theorem List.map_id
deleted theorem List.map_map
deleted theorem List.map_nil
deleted theorem List.map_singleton
deleted theorem List.mem_append
deleted theorem List.mem_append_eq
deleted theorem List.mem_append_left
deleted theorem List.mem_append_right
deleted theorem List.mem_cons_eq
deleted theorem List.mem_cons_iff
deleted theorem List.mem_cons_of_mem
deleted theorem List.mem_cons_self
deleted theorem List.mem_nil_iff
deleted theorem List.nil_bind
deleted theorem List.nil_subset
deleted theorem List.not_bex_nil
deleted inductive List.sublist
deleted theorem List.subset.refl
deleted theorem List.subset.trans
deleted theorem List.subset_append_left
deleted theorem List.subset_append_right
deleted theorem List.subset_cons
deleted theorem And.assoc
deleted def And.elim
deleted theorem And.imp
deleted theorem And.left_comm
deleted theorem And.swap
deleted theorem And.symm
deleted theorem Bool.eq_false_or_eq_true
deleted theorem Bool.ff_ne_tt
deleted def Decidable.by_cases
deleted theorem Decidable.not_not_iff
deleted theorem Eq.to_iff
deleted theorem Exists.imp
deleted theorem Iff.elim
modified theorem Iff.elim_left
modified theorem Iff.elim_right
deleted theorem Not.intro
deleted theorem Or.assoc
deleted theorem Or.comm
deleted theorem Or.left_comm
deleted theorem Or.swap
deleted theorem Or.symm
deleted theorem and_assoc
deleted theorem and_comm
deleted theorem and_congr
deleted theorem and_congr_right
deleted theorem and_iff_left
deleted theorem and_iff_right
deleted theorem and_implies
deleted theorem and_not_self
deleted theorem congr_arg
deleted theorem congr_fun
deleted theorem eq_comm
deleted theorem eq_rec_heq
deleted theorem eq_self_iff_true
deleted theorem exists_congr
deleted theorem exists_imp_exists
deleted theorem false_iff_true
deleted theorem false_implies_iff
deleted theorem false_of_true_eq_false
deleted theorem false_of_true_iff_false
deleted theorem forall_congr'
deleted theorem forall_not_of_not_exists
deleted theorem heq_self_iff_true
deleted theorem if_false
deleted theorem if_true
deleted theorem iff_congr
deleted theorem iff_false_intro
deleted theorem iff_not_self
deleted theorem iff_true_intro
deleted theorem imp_congr
deleted theorem imp_congr_ctx
deleted theorem imp_congr_left
deleted theorem imp_congr_right
added theorem imp_of_if_neg
added theorem imp_of_if_pos
deleted theorem implies_of_if_neg
deleted theorem implies_of_if_pos
deleted theorem implies_true_iff
deleted theorem ne_self_iff_false
deleted theorem neq_of_not_iff
deleted theorem non_contradictory_em
deleted theorem non_contradictory_intro
deleted theorem not_and_self
deleted theorem not_false_iff
deleted theorem not_iff_false_intro
deleted theorem not_iff_not_of_iff
deleted theorem not_iff_self
deleted theorem not_of_iff_false
deleted theorem not_of_not_not_not
deleted theorem not_or
deleted theorem not_true
deleted theorem of_iff_true
deleted theorem or_assoc
deleted theorem or_comm
deleted theorem or_congr
deleted theorem or_iff_left_of_imp
deleted theorem or_iff_right_of_imp
deleted theorem plift.down_up
deleted theorem plift.up_down
deleted structure plift
deleted theorem proof_irrel
modified theorem trans_rel_left
modified theorem trans_rel_right
deleted theorem true_eq_false_of_false
deleted theorem true_iff_false
deleted theorem true_implies_iff
deleted theorem ulift.down_up
deleted theorem ulift.up_down
deleted structure ulift.{r,
deleted def insertUnexpander
deleted def singletonUnexpander
deleted theorem And.congr_left_iff
deleted theorem And.congr_right_iff
deleted theorem And.imp_left
deleted theorem And.imp_right
deleted theorem And.right_comm
deleted theorem And.rotate
deleted theorem Decidable.not_and
deleted theorem Decidable.not_imp_self
deleted def Empty.elim
deleted theorem Exists.choose_spec
deleted theorem Exists.nonempty
deleted theorem Not.decidable_imp_symm
deleted def Or.by_cases'
deleted theorem and_congr_left'
deleted theorem and_congr_left
deleted theorem and_congr_right'
deleted theorem and_iff_left_iff_imp
deleted theorem and_iff_left_of_imp
deleted theorem and_iff_right_iff_imp
deleted theorem and_iff_right_of_imp
deleted theorem and_imp
deleted theorem and_not_self_iff
deleted theorem and_or_distrib_left
deleted theorem and_or_distrib_right
deleted theorem and_self_left
deleted theorem and_self_right
modified theorem and_symm_left
modified theorem and_symm_right
deleted theorem apply_dite
deleted theorem apply_ite
deleted theorem beq_eq_false_iff_ne
deleted theorem by_contra
deleted theorem congr_arg2
deleted theorem dec_em
deleted def decidable_of_bool
deleted def decidable_of_iff'
deleted def decidable_of_iff
deleted theorem decide_eq_false_iff_not
deleted theorem decide_eq_true_iff
deleted theorem dite_not
deleted theorem em
deleted theorem eq_iff_iff
deleted theorem eq_rec_constant
deleted theorem exists_and_distrib_left
deleted theorem exists_and_distrib_right
deleted theorem exists_apply_eq_apply
deleted theorem exists_eq'
deleted theorem exists_eq
deleted theorem exists_eq_left'
deleted theorem exists_eq_left
deleted theorem exists_eq_right
deleted theorem exists_eq_right_right'
deleted theorem exists_eq_right_right
deleted theorem exists_false
deleted theorem exists_imp_distrib
deleted theorem exists_imp_exists'
deleted theorem exists_prop
deleted theorem exists₂_congr
deleted theorem exists₃_congr
deleted theorem exists₄_congr
deleted theorem false_ne_true
deleted theorem forall_and_distrib
deleted theorem forall_const
deleted theorem forall_eq'
deleted theorem forall_eq
deleted theorem forall_eq_or_imp
deleted theorem forall_imp
deleted theorem forall_prop_of_true
deleted theorem forall₂_congr
deleted theorem forall₃_congr
deleted theorem forall₄_congr
deleted theorem heq_iff_eq
deleted theorem iff_and_self
deleted theorem iff_def'
deleted theorem iff_def
deleted theorem iff_false_left
deleted theorem iff_false_right
deleted theorem iff_iff_eq
modified theorem iff_iff_not_or_and_or_not
deleted theorem iff_of_eq
deleted theorem iff_self_and
deleted theorem iff_true_left
deleted theorem iff_true_right
deleted theorem imp.swap
deleted theorem imp_and_distrib
deleted theorem imp_false
deleted theorem imp_iff_right
deleted theorem imp_imp_imp
deleted theorem imp_intro
deleted theorem imp_not_comm
deleted theorem imp_not_self
deleted theorem imp_self
deleted theorem imp_true_iff
deleted theorem ite_id
deleted theorem ite_not
deleted theorem ne_comm
deleted theorem not.decidable_imp_symm
deleted theorem not_and'
deleted theorem not_and
deleted theorem not_and_of_not_left
deleted theorem not_and_of_not_or_not
deleted theorem not_and_of_not_right
deleted theorem not_and_self_iff
deleted theorem not_exists
deleted theorem not_exists_of_forall_not
deleted theorem not_forall_of_exists_not
deleted theorem not_imp_of_and_not
deleted theorem not_not_em
deleted theorem not_not_not
deleted theorem not_not_of_not_imp
deleted theorem not_of_not_imp
deleted theorem not_or_distrib
deleted theorem or.right_comm
deleted theorem or_and_distrib_left
deleted theorem or_and_distrib_right
deleted theorem or_congr_left
deleted theorem or_congr_right
deleted theorem or_iff_left_iff_imp
deleted theorem or_iff_right_iff_imp
deleted theorem or_imp_distrib
deleted theorem or_left_comm
modified theorem or_of_or_of_imp_left
modified theorem or_of_or_of_imp_of_imp
modified theorem or_of_or_of_imp_right
deleted theorem or_self_left
deleted theorem or_self_right
deleted theorem peirce'
deleted theorem proof_irrel_heq
modified theorem Prod.swap_le_swap
deleted inductive Lean.Meta.RCases.RCasesPatt
deleted structure A
deleted structure B
deleted structure C
modified theorem Test.bar2_works
modified def Test.foo2
modified theorem Test.foo2_works