mathlib3

9b70cc61 - feat(data/equiv/encodable): add a few lemmas (#11497)

feat(data/equiv/encodable): add a few lemmas (#11497) * add `simp` lemmas `encodable.encode_inj` and `encodable.decode₂_encode`; * add `encodable.decode₂_eq_some`; * avoid non-final `simp` in the proof of `encodable.Union_decode₂_disjoint_on`.