Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-18 21:51 9407b033

View on Github →

chore(logic/equiv/basic): split into two files (#17038) A fairly easy split of logic.equiv.basic into logic.equiv.defs (containing the stuff with very little prerequisites, and which suffices for many other files), and logic.equiv.basic (the stuff that requires other imports from around logic.*). logic.equiv.basic is still a ~1500 line file, so I'd like to split it further shortly.

Estimated changes

Modified src/algebra/free.lean

Modified src/algebra/group/type_tags.lean

Modified src/algebra/group/with_one.lean

Modified src/algebra/opposites.lean

Modified src/category_theory/functor/fully_faithful.lean

Modified src/category_theory/types.lean

Modified src/combinatorics/derangements/basic.lean

Modified src/control/equiv_functor.lean

Modified src/control/monad/basic.lean

Modified src/control/monad/writer.lean

Modified src/control/traversable/equiv.lean

Modified src/data/erased.lean

Modified src/data/opposite.lean

Modified src/data/part.lean

Modified src/logic/embedding.lean

Modified src/logic/equiv/basic.lean

deleted def equiv.Pi_subsingleton

deleted theorem equiv.apply_eq_iff_eq

deleted theorem equiv.apply_eq_iff_eq_symm_apply

deleted theorem equiv.apply_symm_apply

deleted def equiv.arrow_congr'

deleted theorem equiv.arrow_congr'_refl

deleted theorem equiv.arrow_congr'_symm

deleted theorem equiv.arrow_congr'_trans

deleted def equiv.arrow_congr

deleted theorem equiv.arrow_congr_comp

deleted theorem equiv.arrow_congr_refl

deleted theorem equiv.arrow_congr_symm

deleted theorem equiv.arrow_congr_trans

deleted def equiv.arrow_punit_equiv_punit

deleted def equiv.arrow_punit_of_is_empty

deleted theorem equiv.bijective_comp

deleted theorem equiv.cast_apply

deleted theorem equiv.cast_eq_iff_heq

deleted theorem equiv.cast_refl

deleted theorem equiv.cast_symm

deleted theorem equiv.cast_trans

deleted theorem equiv.coe_fn_injective

deleted theorem equiv.coe_fn_mk

deleted theorem equiv.coe_fn_symm_mk

deleted theorem equiv.coe_refl

deleted theorem equiv.coe_trans

deleted theorem equiv.comp_bijective

deleted theorem equiv.comp_injective

deleted theorem equiv.comp_surjective

deleted theorem equiv.comp_symm_eq

deleted def equiv.conj

deleted theorem equiv.conj_comp

deleted theorem equiv.conj_refl

deleted theorem equiv.conj_symm

deleted theorem equiv.conj_trans

deleted def equiv.empty_arrow_equiv_punit

deleted theorem equiv.eq_comp_symm

deleted theorem equiv.eq_symm_apply

deleted theorem equiv.eq_symm_comp

deleted def equiv.equiv_congr

deleted theorem equiv.equiv_congr_apply_apply

deleted theorem equiv.equiv_congr_refl

deleted theorem equiv.equiv_congr_refl_left

deleted theorem equiv.equiv_congr_refl_right

deleted theorem equiv.equiv_congr_symm

deleted theorem equiv.equiv_congr_trans

deleted def equiv.equiv_empty

deleted def equiv.equiv_empty_equiv

deleted def equiv.equiv_of_is_empty

deleted def equiv.equiv_of_unique

deleted def equiv.equiv_pempty

deleted def equiv.equiv_punit

deleted theorem equiv.ext

deleted theorem equiv.ext_iff

deleted def equiv.false_arrow_equiv_punit

deleted def equiv.fun_unique

deleted theorem equiv.injective_comp

deleted theorem equiv.inv_fun_as_coe

deleted theorem equiv.left_inverse_symm

deleted theorem equiv.nonempty_congr

deleted def equiv.of_iff

deleted def equiv.pempty_arrow_equiv_punit

deleted theorem equiv.perm.coe_subsingleton

deleted theorem equiv.perm.ext

deleted theorem equiv.perm.ext_iff

deleted def equiv.perm.sigma_congr_right

deleted theorem equiv.perm.sigma_congr_right_refl

deleted theorem equiv.perm.sigma_congr_right_symm

deleted theorem equiv.perm.sigma_congr_right_trans

deleted theorem equiv.perm.subsingleton_eq_refl

deleted def equiv.perm

deleted def equiv.perm_congr

deleted theorem equiv.perm_congr_apply

deleted theorem equiv.perm_congr_def

deleted theorem equiv.perm_congr_refl

deleted theorem equiv.perm_congr_symm

deleted theorem equiv.perm_congr_symm_apply

deleted theorem equiv.perm_congr_trans

deleted def equiv.prop_equiv_pempty

deleted def equiv.prop_equiv_punit

deleted def equiv.psigma_congr_right

deleted theorem equiv.psigma_congr_right_refl

deleted theorem equiv.psigma_congr_right_symm

deleted theorem equiv.psigma_congr_right_trans

deleted def equiv.psigma_equiv_sigma

deleted def equiv.psigma_equiv_sigma_plift

deleted def equiv.psigma_equiv_subtype

deleted def equiv.punit_arrow_equiv

deleted def equiv.punit_equiv_punit

deleted theorem equiv.refl_apply

deleted theorem equiv.refl_symm

deleted theorem equiv.refl_trans

deleted theorem equiv.right_inverse_symm

deleted theorem equiv.self_comp_symm

deleted theorem equiv.self_trans_symm

deleted def equiv.sigma_assoc

deleted def equiv.sigma_congr

deleted def equiv.sigma_congr_left'

deleted def equiv.sigma_congr_left

deleted def equiv.sigma_congr_right

deleted theorem equiv.sigma_congr_right_refl

deleted theorem equiv.sigma_congr_right_symm

deleted theorem equiv.sigma_congr_right_trans

deleted def equiv.sigma_equiv_prod

deleted def equiv.sigma_equiv_prod_of_equiv

deleted def equiv.sigma_plift_equiv_subtype

deleted def equiv.sigma_ulift_plift_equiv_subtype

deleted def equiv.simps.symm_apply

deleted theorem equiv.subsingleton_congr

deleted theorem equiv.surjective_comp

deleted theorem equiv.symm_apply_apply

deleted theorem equiv.symm_apply_eq

deleted theorem equiv.symm_comp_eq

deleted theorem equiv.symm_comp_self

deleted theorem equiv.symm_symm

deleted theorem equiv.symm_symm_apply

deleted theorem equiv.symm_trans_apply

deleted theorem equiv.symm_trans_self

deleted theorem equiv.to_fun_as_coe

deleted theorem equiv.trans_apply

deleted theorem equiv.trans_assoc

deleted theorem equiv.trans_refl

deleted def equiv.true_arrow_equiv

deleted structure equiv

deleted theorem quot.congr_mk

deleted theorem quotient.congr_mk

Created src/logic/equiv/defs.lean

added def equiv.Pi_subsingleton

added theorem equiv.apply_eq_iff_eq

added theorem equiv.apply_eq_iff_eq_symm_apply

added theorem equiv.apply_symm_apply

added def equiv.arrow_congr'

added theorem equiv.arrow_congr'_refl

added theorem equiv.arrow_congr'_symm

added theorem equiv.arrow_congr'_trans

added def equiv.arrow_congr

added theorem equiv.arrow_congr_comp

added theorem equiv.arrow_congr_refl

added theorem equiv.arrow_congr_symm

added theorem equiv.arrow_congr_trans

added def equiv.arrow_punit_equiv_punit

added def equiv.arrow_punit_of_is_empty

added theorem equiv.bijective_comp

added theorem equiv.cast_apply

added theorem equiv.cast_eq_iff_heq

added theorem equiv.cast_refl

added theorem equiv.cast_symm

added theorem equiv.cast_trans

added theorem equiv.coe_fn_injective

added theorem equiv.coe_fn_mk

added theorem equiv.coe_fn_symm_mk

added theorem equiv.coe_refl

added theorem equiv.coe_trans

added theorem equiv.comp_bijective

added theorem equiv.comp_injective

added theorem equiv.comp_surjective

added theorem equiv.comp_symm_eq

added def equiv.conj

added theorem equiv.conj_comp

added theorem equiv.conj_refl

added theorem equiv.conj_symm

added theorem equiv.conj_trans

added def equiv.empty_arrow_equiv_punit

added theorem equiv.eq_comp_symm

added theorem equiv.eq_symm_apply

added theorem equiv.eq_symm_comp

added def equiv.equiv_congr

added theorem equiv.equiv_congr_apply_apply

added theorem equiv.equiv_congr_refl

added theorem equiv.equiv_congr_refl_left

added theorem equiv.equiv_congr_refl_right

added theorem equiv.equiv_congr_symm

added theorem equiv.equiv_congr_trans

added def equiv.equiv_empty

added def equiv.equiv_empty_equiv

added def equiv.equiv_of_is_empty

added def equiv.equiv_of_unique

added def equiv.equiv_pempty

added def equiv.equiv_punit

added theorem equiv.ext

added theorem equiv.ext_iff

added def equiv.false_arrow_equiv_punit

added def equiv.fun_unique

added theorem equiv.injective_comp

added theorem equiv.inv_fun_as_coe

added theorem equiv.left_inverse_symm

added theorem equiv.nonempty_congr

added def equiv.of_iff

added def equiv.pempty_arrow_equiv_punit

added theorem equiv.perm.coe_subsingleton

added theorem equiv.perm.ext

added theorem equiv.perm.ext_iff

added def equiv.perm.sigma_congr_right

added theorem equiv.perm.sigma_congr_right_refl

added theorem equiv.perm.sigma_congr_right_symm

added theorem equiv.perm.sigma_congr_right_trans

added theorem equiv.perm.subsingleton_eq_refl

added def equiv.perm

added def equiv.perm_congr

added theorem equiv.perm_congr_apply

added theorem equiv.perm_congr_def

added theorem equiv.perm_congr_refl

added theorem equiv.perm_congr_symm

added theorem equiv.perm_congr_symm_apply

added theorem equiv.perm_congr_trans

added def equiv.prop_equiv_pempty

added def equiv.prop_equiv_punit

added def equiv.psigma_congr_right

added theorem equiv.psigma_congr_right_refl

added theorem equiv.psigma_congr_right_symm

added theorem equiv.psigma_congr_right_trans

added def equiv.psigma_equiv_sigma

added def equiv.psigma_equiv_sigma_plift

added def equiv.psigma_equiv_subtype

added def equiv.punit_arrow_equiv

added def equiv.punit_equiv_punit

added theorem equiv.refl_apply

added theorem equiv.refl_symm

added theorem equiv.refl_trans

added theorem equiv.right_inverse_symm

added theorem equiv.self_comp_symm

added theorem equiv.self_trans_symm

added def equiv.sigma_assoc

added def equiv.sigma_congr

added def equiv.sigma_congr_left'

added def equiv.sigma_congr_left

added def equiv.sigma_congr_right

added theorem equiv.sigma_congr_right_refl

added theorem equiv.sigma_congr_right_symm

added theorem equiv.sigma_congr_right_trans

added def equiv.sigma_equiv_prod

added def equiv.sigma_equiv_prod_of_equiv

added def equiv.sigma_plift_equiv_subtype

added def equiv.sigma_ulift_plift_equiv_subtype

added def equiv.simps.symm_apply

added theorem equiv.subsingleton_congr

added theorem equiv.surjective_comp

added theorem equiv.symm_apply_apply

added theorem equiv.symm_apply_eq

added theorem equiv.symm_comp_eq

added theorem equiv.symm_comp_self

added theorem equiv.symm_symm

added theorem equiv.symm_symm_apply

added theorem equiv.symm_trans_apply

added theorem equiv.symm_trans_self

added theorem equiv.to_fun_as_coe

added theorem equiv.trans_apply

added theorem equiv.trans_assoc

added theorem equiv.trans_refl

added def equiv.true_arrow_equiv

added structure equiv

added theorem quot.congr_mk

added theorem quotient.congr_mk

Modified src/logic/equiv/fin.lean

Modified src/logic/equiv/fintype.lean

Modified src/logic/equiv/functor.lean

Modified src/logic/equiv/local_equiv.lean

Modified src/logic/equiv/set.lean

Modified src/logic/equiv/transfer_instance.lean

Modified src/order/bounded_order.lean

Modified src/order/synonym.lean

Modified src/tactic/equiv_rw.lean

Modified src/tactic/norm_swap.lean

Modified test/norm_swap.lean

Modified test/simp_result.lean