mathlib3
3ac609b9 - chore(topology/continuous_function/compact): relax typeclass assumptions for metric space structure on C(X, Y) (#8717)
