mathlib3

de8990d5 - Template for `disjoint_prod_add` with `sorry`