mathlib3

84b8b0d8 - chore(topology/vector_bundle): fix timeout by optimizing proof (#13026)

chore(topology/vector_bundle): fix timeout by optimizing proof (#13026) This PR speeds up a big and slow definition using `simp only` and `convert` → `refine`. This declaration seems to be on the edge of timing out and some other changes like #11750 tripped it up. Time saved if I run it with timeouts disabled: * master 14.8s → 6.3s * #11750 14.2s → 6.12s