mathlib3

54b7f356 - Merge branch 'encode_binary_lemmas' of https://github.com/leanprover-community/mathlib into efficient_mkpair