Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-03 19:01 d2d8742b

View on Github →

chore(logic/equiv/basic): Generalize Type to Sort (#18543) This backports a change that was already made in mathlib4. Indeed, mathport complains that the change was made, see the comments in https://github.com/leanprover-community/mathlib3port/blob/e3a205b1f51e409563e9e4294f41dd4df61f578a/Mathbin/Logic/Equiv/Basic.lean#L1729-L1735 By backporting this, we can deal with the fallout up-front rather than during porting.

Estimated changes

Modified src/combinatorics/configuration.lean

Modified src/data/list/defs.lean

modified def list.foldl_with_index

modified def list.foldl_with_index_aux

modified def list.foldr_with_index

modified def list.foldr_with_index_aux

Modified src/logic/basic.lean

modified theorem eq_iff_eq_cancel_left

modified theorem eq_iff_eq_cancel_right

Modified src/logic/equiv/basic.lean

modified def equiv.subtype_equiv_prop

modified def equiv.subtype_subtype_equiv_subtype_exists

modified def equiv.subtype_subtype_equiv_subtype_inter

modified theorem function.injective.map_swap

Modified src/logic/nonempty.lean

modified theorem function.surjective.nonempty