On [this line](https://github.com/avigad/mathematics_in_lean_source/blob/8baa112dcb882785255fdcb6aee4cac88a0c4925/MIL/C11_Topology/S02_Metric_Spaces.lean#L343) you use the fact that the product of two compact spaces is compact, which hasn't been stated before.
