mathlib3

feat(logic,data/equiv,prod): various lemmas

#1224

Merged