mathlib3

4a5799e1 - feat(data/equiv/basic): subtype_prod_equiv_prod (#2717)