mathlib3

5bccb515 - refactor(logic/equiv/basic): tweak lemmas on equivalences between `unique` types (#14605)

refactor(logic/equiv/basic): tweak lemmas on equivalences between `unique` types (#14605) This PR does various simple and highly related things: - Rename `equiv_of_unique_of_unique` to `equiv_of_unique` and make its arguments explicit, in order to match the lemma `equiv_of_empty` added in #14604. - Rename `equiv_punit_of_unique` to `equiv_punit` and make its argument explicit to match `equiv_pempty`. - Fix their docstrings (which talked about a `subsingleton` type instead of a `unique` one). - Move them much earlier in the file, together with the lemmas on empty types. - Golf `prop_equiv_punit`.