mathlib

2bf44d31 - refactor(*): rename metric_space_subtype to subtype.metric_space (#817)