mathlib3

477338d2 - refactor(data/subtype): organise in namespaces, use variables, add two simp-lemmas (#760)