mathlib

83d44a3d - hack(manifold): disable subsingleton instances to speed up simp (#5779)

hack(manifold): disable subsingleton instances to speed up simp (#5779) Simp takes an enormous amount of time in manifold code looking for subsingleton instances (and in fact probably in the whole library, but manifolds are particularly simp-heavy). We disable two such instances in the `manifold` locale, to get serious speedups (for instance, `times_cont_mdiff_on.times_cont_mdiff_on_tangent_map_within` goes down from 27s to 10s on my computer). This is *not* a proper fix. But it already makes a serious difference in this part of the library.. Zulip discussion at https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223001979