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





leanprover-community/mathlib,leanprover-community/mathlib