mathlib3

23f30a30 - fix(topology/vector_bundle): squeeze simp, remove non-terminal simp (#14357)

fix(topology/vector_bundle): squeeze simp, remove non-terminal simp (#14357) For some reason I had to mention `trivialization.coe_coe` explicitly, even though it is in `mfld_simps` (maybe because another simp lemma would otherwise apply first?)