Commit 2022-11-06 23:41 f7707875

View on Github →

refactor(*): supremum of several recent refactoring PRs (#17381) This is the supremum of

#17376
#17375
#17374
#17362
#17355
#17349
#17347
#17338
#17336 with imports fixed up to accommodate all the overlapping changes to imports.

Estimated changes

Modified src/algebra/big_operators/order.lean

Modified src/algebra/euclidean_domain.lean

Modified src/algebra/gcd_monoid/basic.lean

Modified src/algebra/group/pi.lean

Modified src/algebra/group_power/order.lean

Modified src/algebra/order/field/basic.lean

Modified src/algebra/order/field/defs.lean

Modified src/algebra/order/floor.lean

Created src/algebra/order/group/abs.lean

added theorem abs_abs

added theorem abs_abs_sub_abs_le_abs_sub

added theorem abs_add'

added theorem abs_add

added theorem abs_add_three

added theorem abs_by_cases

added theorem abs_choice

added theorem abs_eq

added theorem abs_eq_abs

added theorem abs_eq_max_neg

added theorem abs_eq_sup_inv

added theorem abs_eq_zero

added theorem abs_le'

added theorem abs_le

added theorem abs_le_abs

added theorem abs_le_abs_of_nonneg

added theorem abs_le_abs_of_nonpos

added theorem abs_le_max_abs_abs

added theorem abs_lt

added theorem abs_max_le_max_abs_abs

added theorem abs_min_le_max_abs_abs

added theorem abs_neg

added theorem abs_nonneg

added theorem abs_nonpos_iff

added theorem abs_of_neg

added theorem abs_of_nonneg

added theorem abs_of_nonpos

added theorem abs_of_pos

added theorem abs_pos

added theorem abs_pos_of_neg

added theorem abs_pos_of_pos

added theorem abs_sub

added theorem abs_sub_abs_le_abs_sub

added theorem abs_sub_comm

added theorem abs_sub_le

added theorem abs_sub_le_iff

added theorem abs_sub_lt_iff

added theorem abs_zero

added theorem add_abs_nonneg

added theorem apply_abs_le_mul_of_one_le'

added theorem apply_abs_le_mul_of_one_le

added theorem dist_bdd_within_interval

added theorem eq_of_abs_sub_eq_zero

added theorem eq_of_abs_sub_nonpos

added theorem eq_or_eq_neg_of_abs_eq

added theorem le_abs'

added theorem le_abs

added theorem le_abs_self

added theorem le_of_abs_le

added theorem lt_abs

added theorem lt_of_abs_lt

added theorem max_sub_min_eq_abs'

added theorem max_sub_min_eq_abs

added theorem min_abs_abs_le_abs_max

added theorem min_abs_abs_le_abs_min

added theorem neg_abs_le_neg

added theorem neg_abs_le_self

added theorem neg_le_abs_self

added theorem neg_le_of_abs_le

added theorem neg_lt_of_abs_lt

added theorem sub_le_of_abs_sub_le_left

added theorem sub_le_of_abs_sub_le_right

added theorem sub_lt_of_abs_sub_lt_left

added theorem sub_lt_of_abs_sub_lt_right

Modified src/algebra/order/group/basic.lean

deleted theorem abs_abs

deleted theorem abs_abs_sub_abs_le_abs_sub

deleted theorem abs_add'

deleted theorem abs_add

deleted theorem abs_add_three

deleted theorem abs_by_cases

deleted theorem abs_choice

deleted theorem abs_eq

deleted theorem abs_eq_abs

deleted theorem abs_eq_max_neg

deleted theorem abs_eq_sup_inv

deleted theorem abs_eq_zero

deleted theorem abs_le'

deleted theorem abs_le

deleted theorem abs_le_abs

deleted theorem abs_le_abs_of_nonneg

deleted theorem abs_le_abs_of_nonpos

deleted theorem abs_le_max_abs_abs

deleted theorem abs_lt

deleted theorem abs_max_le_max_abs_abs

deleted theorem abs_max_sub_max_le_abs

deleted theorem abs_max_sub_max_le_max

deleted theorem abs_min_le_max_abs_abs

deleted theorem abs_min_sub_min_le_max

deleted theorem abs_neg

deleted theorem abs_nonneg

deleted theorem abs_nonpos_iff

deleted theorem abs_of_neg

deleted theorem abs_of_nonneg

deleted theorem abs_of_nonpos

deleted theorem abs_of_pos

deleted theorem abs_pos

deleted theorem abs_pos_of_neg

deleted theorem abs_pos_of_pos

deleted theorem abs_sub

deleted theorem abs_sub_abs_le_abs_sub

deleted theorem abs_sub_comm

deleted theorem abs_sub_le

deleted theorem abs_sub_le_iff

deleted theorem abs_sub_lt_iff

deleted theorem abs_zero

deleted theorem add_abs_nonneg

deleted theorem apply_abs_le_mul_of_one_le'

deleted theorem apply_abs_le_mul_of_one_le

deleted theorem dist_bdd_within_interval

deleted theorem eq_of_abs_sub_eq_zero

deleted theorem eq_of_abs_sub_nonpos

deleted theorem eq_or_eq_neg_of_abs_eq

deleted theorem le_abs'

deleted theorem le_abs

deleted theorem le_abs_self

deleted theorem le_iff_forall_lt_one_mul_le

deleted theorem le_iff_forall_one_lt_le_mul

deleted theorem le_of_abs_le

deleted theorem le_of_forall_lt_one_mul_le

deleted theorem le_of_forall_one_lt_div_le

deleted theorem lt_abs

deleted theorem lt_of_abs_lt

deleted theorem max_div_div_left'

deleted theorem max_div_div_right'

deleted theorem max_inv_inv'

deleted theorem max_one_div_max_inv_one_eq_self

deleted theorem max_sub_max_le_max

deleted theorem max_sub_min_eq_abs'

deleted theorem max_sub_min_eq_abs

deleted theorem min_abs_abs_le_abs_max

deleted theorem min_abs_abs_le_abs_min

deleted theorem min_div_div_left'

deleted theorem min_div_div_right'

deleted theorem min_inv_inv'

deleted theorem neg_abs_le_neg

deleted theorem neg_abs_le_self

deleted theorem neg_le_abs_self

deleted theorem neg_le_of_abs_le

deleted theorem neg_lt_of_abs_lt

deleted theorem sub_le_of_abs_sub_le_left

deleted theorem sub_le_of_abs_sub_le_right

deleted theorem sub_lt_of_abs_sub_lt_left

deleted theorem sub_lt_of_abs_sub_lt_right

deleted theorem with_top.coe_neg

Created src/algebra/order/group/bounds.lean

added theorem is_glb.exists_between_self_add'

added theorem is_glb.exists_between_self_add

added theorem is_lub.exists_between_sub_self'

added theorem is_lub.exists_between_sub_self

Created src/algebra/order/group/densely_ordered.lean

added theorem le_iff_forall_lt_one_mul_le

added theorem le_iff_forall_one_lt_le_mul

added theorem le_of_forall_lt_one_mul_le

added theorem le_of_forall_one_lt_div_le

Created src/algebra/order/group/min_max.lean

added theorem abs_max_sub_max_le_abs

added theorem abs_max_sub_max_le_max

added theorem abs_min_sub_min_le_max

added theorem max_div_div_left'

added theorem max_div_div_right'

added theorem max_inv_inv'

added theorem max_one_div_max_inv_one_eq_self

added theorem max_sub_max_le_max

added theorem min_div_div_left'

added theorem min_div_div_right'

added theorem min_inv_inv'

Created src/algebra/order/group/prod.lean

Created src/algebra/order/group/units.lean

Created src/algebra/order/group/with_top.lean

added theorem with_top.coe_neg

Modified src/algebra/order/hom/ring.lean

Modified src/algebra/order/invertible.lean

Modified src/algebra/order/lattice_group.lean

Modified src/algebra/order/monoid/canonical.lean

Modified src/algebra/order/nonneg/ring.lean

Modified src/algebra/order/pi.lean

Modified src/algebra/order/positive/ring.lean

Created src/algebra/order/ring/abs.lean

added theorem abs_cases

added theorem abs_dvd

added theorem abs_dvd_abs

added theorem abs_dvd_self

added theorem abs_eq_iff_mul_self_eq

added theorem abs_eq_neg_self

added theorem abs_eq_self

added def abs_hom

added theorem abs_le_iff_mul_self_le

added theorem abs_le_one_iff_mul_self_le_one

added theorem abs_lt_iff_mul_self_lt

added theorem abs_mul

added theorem abs_mul_abs_self

added theorem abs_mul_self

added theorem abs_one

added theorem abs_sub_sq

added theorem abs_two

added theorem dvd_abs

added theorem max_zero_add_max_neg_zero_eq_abs_self

added theorem self_dvd_abs

Renamed src/algebra/order/ring.lean to src/algebra/order/ring/basic.lean

deleted theorem abs_cases

deleted theorem abs_dvd

deleted theorem abs_dvd_abs

deleted theorem abs_dvd_self

deleted theorem abs_eq_iff_mul_self_eq

deleted theorem abs_eq_neg_self

deleted theorem abs_eq_self

deleted def abs_hom

deleted theorem abs_le_iff_mul_self_le

deleted theorem abs_le_one_iff_mul_self_le_one

deleted theorem abs_lt_iff_mul_self_lt

deleted theorem abs_mul

deleted theorem abs_mul_abs_self

deleted theorem abs_mul_self

deleted theorem abs_one

deleted theorem abs_sub_sq

deleted theorem abs_two

deleted theorem canonically_ordered_comm_semiring.mul_pos

deleted theorem dvd_abs

deleted theorem max_zero_add_max_neg_zero_eq_abs_self

deleted theorem mul_add_mul_le_mul_add_mul'

deleted theorem mul_add_mul_le_mul_add_mul

deleted theorem mul_add_mul_lt_mul_add_mul'

deleted theorem mul_add_mul_lt_mul_add_mul

deleted theorem mul_tsub

deleted theorem self_dvd_abs

deleted theorem strict_ordered_semiring.to_char_zero

deleted theorem tsub_mul

deleted theorem with_bot.bot_lt_mul

deleted theorem with_bot.bot_mul

deleted theorem with_bot.bot_mul_bot

deleted theorem with_bot.coe_mul

deleted theorem with_bot.mul_bot

deleted theorem with_bot.mul_coe

deleted theorem with_bot.mul_def

deleted theorem with_bot.mul_eq_bot_iff

deleted theorem with_top.coe_mul

deleted theorem with_top.mul_coe

deleted theorem with_top.mul_def

deleted theorem with_top.mul_eq_top_iff

deleted theorem with_top.mul_lt_top

deleted theorem with_top.mul_top

deleted theorem with_top.top_mul

deleted theorem with_top.top_mul_top

deleted theorem with_top.untop'_zero_mul

Created src/algebra/order/ring/canonical.lean

added theorem canonically_ordered_comm_semiring.mul_pos

added theorem mul_add_mul_le_mul_add_mul'

added theorem mul_add_mul_le_mul_add_mul

added theorem mul_add_mul_lt_mul_add_mul'

added theorem mul_add_mul_lt_mul_add_mul

added theorem mul_tsub

added theorem tsub_mul

Renamed src/algebra/order/ring_lemmas.lean to src/algebra/order/ring/lemmas.lean

Created src/algebra/order/ring/nontrivial.lean

added theorem strict_ordered_semiring.to_char_zero

Created src/algebra/order/ring/with_top.lean

added theorem with_bot.bot_lt_mul

added theorem with_bot.bot_mul

added theorem with_bot.bot_mul_bot

added theorem with_bot.coe_mul

added theorem with_bot.mul_bot

added theorem with_bot.mul_coe

added theorem with_bot.mul_def

added theorem with_bot.mul_eq_bot_iff

added theorem with_top.coe_mul

added theorem with_top.mul_coe

added theorem with_top.mul_def

added theorem with_top.mul_eq_top_iff

added theorem with_top.mul_lt_top

added theorem with_top.mul_top

added theorem with_top.top_mul

added theorem with_top.top_mul_top

added theorem with_top.untop'_zero_mul

Modified src/algebra/order/smul.lean

Modified src/algebra/order/upper_lower.lean

Modified src/algebra/order/with_zero.lean

Modified src/algebra/ring/prod.lean

Modified src/algebra/tropical/basic.lean

Modified src/analysis/convex/between.lean

Modified src/category_theory/differential_object.lean

Modified src/category_theory/essentially_small.lean

Modified src/category_theory/limits/shapes/zero_morphisms.lean

Modified src/category_theory/triangulated/basic.lean

Modified src/combinatorics/simple_graph/regularity/energy.lean

Modified src/data/countable/small.lean

Modified src/data/enat/basic.lean

Modified src/data/fin/succ_pred.lean

Modified src/data/fintype/small.lean

Modified src/data/hash_map.lean

Modified src/data/int/basic.lean

Modified src/data/int/order.lean

Modified src/data/int/succ_pred.lean

Modified src/data/list/lattice.lean

Modified src/data/list/min_max.lean

Modified src/data/list/zip.lean

Modified src/data/nat/cast.lean

Modified src/data/nat/order.lean

Modified src/data/nat/pairing.lean

Modified src/data/nat/part_enat.lean

Modified src/data/nat/succ_pred.lean

Modified src/data/nat/with_bot.lean

Modified src/data/ordmap/ordset.lean

Modified src/data/pi/lex.lean

Modified src/data/pnat/basic.lean

deleted theorem nat.nat_pred_succ_pnat

deleted def nat.succ_pnat

deleted theorem nat.succ_pnat_coe

deleted def nat.to_pnat'

deleted theorem nat.to_pnat'_coe

deleted def nat.to_pnat

deleted theorem pnat.coe_eq_one_iff

deleted theorem pnat.coe_injective

deleted theorem pnat.coe_le_coe

deleted theorem pnat.coe_lt_coe

deleted theorem pnat.coe_to_pnat'

deleted def pnat.div

deleted theorem pnat.div_coe

deleted def pnat.div_exact

deleted theorem pnat.eq

deleted theorem pnat.mk_coe

deleted theorem pnat.mk_le_mk

deleted theorem pnat.mk_lt_mk

deleted theorem pnat.mk_one

deleted def pnat.mod

deleted theorem pnat.mod_coe

deleted def pnat.mod_div

deleted def pnat.mod_div_aux

deleted def pnat.nat_pred

deleted theorem pnat.nat_pred_eq_pred

deleted theorem pnat.ne_zero

deleted theorem pnat.not_lt_one

deleted theorem pnat.one_coe

deleted theorem pnat.one_le

deleted theorem pnat.pos

deleted def pnat.strong_induction_on

deleted theorem pnat.succ_pnat_nat_pred

deleted theorem pnat.to_pnat'_coe

deleted def pnat

Created src/data/pnat/defs.lean

added theorem nat.nat_pred_succ_pnat

added def nat.succ_pnat

added theorem nat.succ_pnat_coe

added def nat.to_pnat'

added theorem nat.to_pnat'_coe

added def nat.to_pnat

added theorem pnat.coe_eq_one_iff

added theorem pnat.coe_injective

added theorem pnat.coe_le_coe

added theorem pnat.coe_lt_coe

added theorem pnat.coe_to_pnat'

added def pnat.div

added theorem pnat.div_coe

added def pnat.div_exact

added theorem pnat.eq

added theorem pnat.mk_coe

added theorem pnat.mk_le_mk

added theorem pnat.mk_lt_mk

added theorem pnat.mk_one

added def pnat.mod

added theorem pnat.mod_coe

added def pnat.mod_div

added def pnat.mod_div_aux

added def pnat.nat_pred

added theorem pnat.nat_pred_eq_pred

added theorem pnat.ne_zero

added theorem pnat.not_lt_one

added theorem pnat.one_coe

added theorem pnat.one_le

added theorem pnat.pos

added def pnat.strong_induction_on

added theorem pnat.succ_pnat_nat_pred

added theorem pnat.to_pnat'_coe

added def pnat

Modified src/data/pnat/interval.lean

Modified src/data/rat/defs.lean

Modified src/data/rat/order.lean

Modified src/data/real/cardinality.lean

Modified src/data/set/basic.lean

added theorem set.nat.mem_range_succ

Modified src/data/set/intervals/basic.lean

deleted def order_iso.Ici_bot

deleted def order_iso.Iic_top

deleted theorem order_iso.image_Icc

deleted theorem order_iso.image_Ici

deleted theorem order_iso.image_Ico

deleted theorem order_iso.image_Iic

deleted theorem order_iso.image_Iio

deleted theorem order_iso.image_Ioc

deleted theorem order_iso.image_Ioi

deleted theorem order_iso.image_Ioo

deleted theorem order_iso.preimage_Icc

deleted theorem order_iso.preimage_Ici

deleted theorem order_iso.preimage_Ico

deleted theorem order_iso.preimage_Iic

deleted theorem order_iso.preimage_Iio

deleted theorem order_iso.preimage_Ioc

deleted theorem order_iso.preimage_Ioi

deleted theorem order_iso.preimage_Ioo

deleted theorem set.add_mem_Icc_iff_left

deleted theorem set.add_mem_Icc_iff_right

deleted theorem set.add_mem_Ico_iff_left

deleted theorem set.add_mem_Ico_iff_right

deleted theorem set.add_mem_Ioc_iff_left

deleted theorem set.add_mem_Ioc_iff_right

deleted theorem set.add_mem_Ioo_iff_left

deleted theorem set.add_mem_Ioo_iff_right

deleted theorem set.inv_mem_Icc_iff

deleted theorem set.inv_mem_Ico_iff

deleted theorem set.inv_mem_Ioc_iff

deleted theorem set.inv_mem_Ioo_iff

deleted theorem set.mem_Icc_iff_abs_le

deleted theorem set.nonempty_Ico_sdiff

deleted theorem set.sub_mem_Icc_iff_left

deleted theorem set.sub_mem_Icc_iff_right

deleted theorem set.sub_mem_Ico_iff_left

deleted theorem set.sub_mem_Ico_iff_right

deleted theorem set.sub_mem_Ioc_iff_left

deleted theorem set.sub_mem_Ioc_iff_right

deleted theorem set.sub_mem_Ioo_iff_left

deleted theorem set.sub_mem_Ioo_iff_right

Created src/data/set/intervals/group.lean

added theorem set.add_mem_Icc_iff_left

added theorem set.add_mem_Icc_iff_right

added theorem set.add_mem_Ico_iff_left

added theorem set.add_mem_Ico_iff_right

added theorem set.add_mem_Ioc_iff_left

added theorem set.add_mem_Ioc_iff_right

added theorem set.add_mem_Ioo_iff_left

added theorem set.add_mem_Ioo_iff_right

added theorem set.inv_mem_Icc_iff

added theorem set.inv_mem_Ico_iff

added theorem set.inv_mem_Ioc_iff

added theorem set.inv_mem_Ioo_iff

added theorem set.mem_Icc_iff_abs_le

added theorem set.nonempty_Ico_sdiff

added theorem set.sub_mem_Icc_iff_left

added theorem set.sub_mem_Icc_iff_right

added theorem set.sub_mem_Ico_iff_left

added theorem set.sub_mem_Ico_iff_right

added theorem set.sub_mem_Ioc_iff_left

added theorem set.sub_mem_Ioc_iff_right

added theorem set.sub_mem_Ioo_iff_left

added theorem set.sub_mem_Ioo_iff_right

Modified src/data/set/intervals/ord_connected_component.lean

Created src/data/set/intervals/order_iso.lean

added def order_iso.Ici_bot

added def order_iso.Iic_top

added theorem order_iso.image_Icc

added theorem order_iso.image_Ici

added theorem order_iso.image_Ico

added theorem order_iso.image_Iic

added theorem order_iso.image_Iio

added theorem order_iso.image_Ioc

added theorem order_iso.image_Ioi

added theorem order_iso.image_Ioo

added theorem order_iso.preimage_Icc

added theorem order_iso.preimage_Ici

added theorem order_iso.preimage_Ico

added theorem order_iso.preimage_Iic

added theorem order_iso.preimage_Iio

added theorem order_iso.preimage_Ioc

added theorem order_iso.preimage_Ioi

added theorem order_iso.preimage_Ioo

Modified src/data/set/intervals/unordered_interval.lean

deleted theorem set.abs_sub_le_of_subinterval

deleted theorem set.abs_sub_left_of_mem_interval

deleted theorem set.abs_sub_right_of_mem_interval

deleted theorem set.image_add_const_interval

deleted theorem set.image_const_add_interval

deleted theorem set.image_const_mul_interval

deleted theorem set.image_const_sub_interval

deleted theorem set.image_div_const_interval

deleted theorem set.image_mul_const_interval

deleted theorem set.image_neg_interval

deleted theorem set.image_sub_const_interval

deleted theorem set.preimage_add_const_interval

deleted theorem set.preimage_const_add_interval

deleted theorem set.preimage_const_mul_interval

deleted theorem set.preimage_const_sub_interval

deleted theorem set.preimage_div_const_interval

deleted theorem set.preimage_mul_const_interval

deleted theorem set.preimage_neg_interval

deleted theorem set.preimage_sub_const_interval

Modified src/data/set/pairwise.lean

deleted theorem function.injective_iff_pairwise_ne

deleted theorem pairwise.mono

deleted theorem pairwise.set_pairwise

deleted def pairwise

deleted theorem reflexive.set_pairwise_iff

deleted theorem set.pairwise.imp

deleted theorem set.pairwise.imp_on

deleted theorem set.pairwise.on_injective

deleted theorem set.pairwise_of_forall

Renamed src/data/set/intervals/image_preimage.lean to src/data/set/pointwise/interval.lean

added theorem set.abs_sub_le_of_subinterval

added theorem set.abs_sub_left_of_mem_interval

added theorem set.abs_sub_right_of_mem_interval

added theorem set.image_add_const_interval

modified theorem set.image_affine_Icc'

added theorem set.image_const_add_interval

added theorem set.image_const_mul_interval

added theorem set.image_const_sub_interval

added theorem set.image_div_const_interval

added theorem set.image_mul_const_interval

modified theorem set.image_mul_left_Icc'

modified theorem set.image_mul_left_Icc

modified theorem set.image_mul_left_Ioo

modified theorem set.image_mul_right_Icc'

modified theorem set.image_mul_right_Icc

modified theorem set.image_mul_right_Ioo

added theorem set.image_neg_interval

added theorem set.image_sub_const_interval

modified theorem set.inv_Ioi

modified theorem set.inv_Ioo_0_left

added theorem set.preimage_add_const_interval

added theorem set.preimage_const_add_interval

modified theorem set.preimage_const_mul_Icc

modified theorem set.preimage_const_mul_Icc_of_neg

modified theorem set.preimage_const_mul_Ici

modified theorem set.preimage_const_mul_Ici_of_neg

modified theorem set.preimage_const_mul_Ico

modified theorem set.preimage_const_mul_Ico_of_neg

modified theorem set.preimage_const_mul_Iic

modified theorem set.preimage_const_mul_Iic_of_neg

modified theorem set.preimage_const_mul_Iio

modified theorem set.preimage_const_mul_Iio_of_neg

modified theorem set.preimage_const_mul_Ioc

modified theorem set.preimage_const_mul_Ioc_of_neg

modified theorem set.preimage_const_mul_Ioi

modified theorem set.preimage_const_mul_Ioi_of_neg

modified theorem set.preimage_const_mul_Ioo

modified theorem set.preimage_const_mul_Ioo_of_neg

added theorem set.preimage_const_mul_interval

added theorem set.preimage_const_sub_interval

added theorem set.preimage_div_const_interval

modified theorem set.preimage_mul_const_Icc

modified theorem set.preimage_mul_const_Icc_of_neg

modified theorem set.preimage_mul_const_Ici

modified theorem set.preimage_mul_const_Ici_of_neg

modified theorem set.preimage_mul_const_Ico

modified theorem set.preimage_mul_const_Ico_of_neg

modified theorem set.preimage_mul_const_Iic

modified theorem set.preimage_mul_const_Iic_of_neg

modified theorem set.preimage_mul_const_Iio

modified theorem set.preimage_mul_const_Iio_of_neg

modified theorem set.preimage_mul_const_Ioc

modified theorem set.preimage_mul_const_Ioc_of_neg

modified theorem set.preimage_mul_const_Ioi

modified theorem set.preimage_mul_const_Ioi_of_neg

modified theorem set.preimage_mul_const_Ioo

modified theorem set.preimage_mul_const_Ioo_of_neg

added theorem set.preimage_mul_const_interval

added theorem set.preimage_neg_interval

added theorem set.preimage_sub_const_interval

Modified src/dynamics/periodic_pts.lean

Modified src/group_theory/submonoid/operations.lean

Modified src/group_theory/subsemigroup/operations.lean

Modified src/linear_algebra/affine_space/affine_map.lean

Modified src/linear_algebra/free_module/basic.lean

Modified src/logic/encodable/basic.lean

Modified src/logic/equiv/nat.lean

Created src/logic/pairwise.lean

added theorem function.injective_iff_pairwise_ne

added theorem pairwise.mono

added theorem pairwise.set_pairwise

added def pairwise

added theorem reflexive.set_pairwise_iff

added theorem set.pairwise.imp

added theorem set.pairwise.imp_on

added theorem set.pairwise.on_injective

added theorem set.pairwise_of_forall

Renamed src/logic/small.lean to src/logic/small/basic.lean

Created src/logic/small/list.lean

Modified src/model_theory/basic.lean

Modified src/number_theory/ADE_inequality.lean

Modified src/number_theory/lucas_lehmer.lean

Modified src/order/atoms.lean

Modified src/order/basic.lean

Renamed src/order/bounds.lean to src/order/bounds/basic.lean

deleted theorem is_glb.exists_between_self_add'

deleted theorem is_glb.exists_between_self_add

deleted theorem is_lub.exists_between_sub_self'

deleted theorem is_lub.exists_between_sub_self

deleted theorem order_iso.is_glb_image'

deleted theorem order_iso.is_glb_image

deleted theorem order_iso.is_glb_preimage'

deleted theorem order_iso.is_glb_preimage

deleted theorem order_iso.is_lub_image'

deleted theorem order_iso.is_lub_image

deleted theorem order_iso.is_lub_preimage'

deleted theorem order_iso.is_lub_preimage

deleted theorem order_iso.lower_bounds_image

deleted theorem order_iso.upper_bounds_image

Created src/order/bounds/order_iso.lean

added theorem order_iso.is_glb_image'

added theorem order_iso.is_glb_image

added theorem order_iso.is_glb_preimage'

added theorem order_iso.is_glb_preimage

added theorem order_iso.is_lub_image'

added theorem order_iso.is_lub_image

added theorem order_iso.is_lub_preimage'

added theorem order_iso.is_lub_preimage

added theorem order_iso.lower_bounds_image

added theorem order_iso.upper_bounds_image

Modified src/order/compactly_generated.lean

Modified src/order/complete_lattice.lean

Modified src/order/conditionally_complete_lattice.lean

Modified src/order/filter/at_top_bot.lean

Modified src/order/lattice_intervals.lean

Modified src/order/semiconj_Sup.lean

Modified src/order/succ_pred/interval_succ.lean

Modified src/order/upper_lower.lean

Modified src/ring_theory/hahn_series.lean

Modified src/set_theory/cardinal/basic.lean

Modified src/set_theory/zfc/basic.lean

Modified src/tactic/interval_cases.lean

Modified src/tactic/linarith/lemmas.lean

Modified src/tactic/monotonicity/lemmas.lean

Modified src/testing/slim_check/sampleable.lean

Modified src/topology/algebra/order/basic.lean

Modified src/topology/instances/real.lean

Modified test/finish4.lean

Modified test/library_search/ordered_ring.lean

Modified test/monotonicity.lean

Modified test/nontriviality.lean

Modified test/squeeze.lean