diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean
index a3ff1705..64b37d89 100644
--- a/SphereEversion/Global/OneJetBundle.lean
+++ b/SphereEversion/Global/OneJetBundle.lean
@@ -155,8 +155,6 @@ instance (x : M × M') : Module 𝕜 (FJ¹MM' x) :=
 
 end
 
-set_option backward.isDefEq.respectTransparency false in
-set_option backward.isDefEq.respectTransparency.instanceSearchTypes false in
 instance : TopologicalSpace J¹MM' := by
   delta OneJetSpace OneJetBundle
   infer_instance
@@ -181,6 +179,10 @@ set_option backward.isDefEq.respectTransparency false in
 set_option backward.isDefEq.respectTransparency.instanceSearchTypes false in
 instance : ChartedSpace HJ J¹MM' := by
   delta OneJetSpace OneJetBundle
+  -- Making `FiberBundle.chartedSpace` apply here means unfolding the `TopologicalSpace J¹MM'`
+  -- instance above, which unification during instance synthesis will not do.
+  -- One potential fix is naming the instance:
+  -- exact FiberBundle.chartedSpace ..
   infer_instance
 
 set_option backward.isDefEq.respectTransparency false in
diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean
index 08cea64e..26a8887b 100644
--- a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean
+++ b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean
@@ -121,12 +121,26 @@ end Hom
 
 section Pullback
 
-/-- We need some instances like this to work with negation on pullbacks -/
 instance {B B'} {E : B → Type*} {f : B' → B} {x : B'} [∀ x', AddCommGroup (E x')] :
-    AddCommGroup ((f *ᵖ E) x) := by delta Bundle.Pullback; infer_instance
+    AddCommGroup ((f *ᵖ E) x) :=
+  inferInstanceAs <| AddCommGroup (E (f x))
 
-instance {B B'} {E : B → Type*} {f : B' → B} {x : B'} [∀ x', Zero (E x')] : Zero ((f *ᵖ E) x) := by
-  delta Bundle.Pullback; infer_instance
+instance {B B'} {E : B → Type*} {f : B' → B} {x : B'} [∀ x', Zero (E x')] : Zero ((f *ᵖ E) x) :=
+  inferInstanceAs <| Zero (E (f x))
+
+instance {B B'} {E : B → Type*} {f : B' → B} {x : B'} [∀ x', TopologicalSpace (E x')]
+    [∀ x', AddCommMonoid (E x')] [∀ x', ContinuousAdd (E x')] : ContinuousAdd ((f *ᵖ E) x) :=
+  inferInstanceAs <| ContinuousAdd (E (f x))
+
+instance {B B'} {E : B → Type*} {f : B' → B} {x : B'} [∀ x', TopologicalSpace (E x')]
+    [∀ x', AddCommGroup (E x')] [∀ x', IsTopologicalAddGroup (E x')] :
+    IsTopologicalAddGroup ((f *ᵖ E) x) :=
+  inferInstanceAs <| IsTopologicalAddGroup (E (f x))
+
+instance {R B B'} [Semiring R] [TopologicalSpace R] {E : B → Type*} {f : B' → B} {x : B'}
+    [∀ x', TopologicalSpace (E x')] [∀ x', AddCommMonoid (E x')] [∀ x', Module R (E x')]
+    [∀ x', ContinuousSMul R (E x')] : ContinuousSMul R ((f *ᵖ E) x) :=
+  inferInstanceAs <| ContinuousSMul R (E (f x))
 
 variable {B F B' K : Type*} {E : B → Type*} {f : K} [TopologicalSpace B']
   [TopologicalSpace (TotalSpace F E)] [TopologicalSpace F] [TopologicalSpace B] [∀ b, Zero (E b)]
diff --git a/lean-toolchain b/lean-toolchain
index 9d74fe15..f0e00b33 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.35.0-rc3
\ No newline at end of file
+leanprover/lean4:v4.35.0-rc3