diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean
index 4833b9ec..86d7e15b 100644
--- a/SphereEversion/Global/Relation.lean
+++ b/SphereEversion/Global/Relation.lean
@@ -626,8 +626,10 @@ def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN where
   smooth_inv := by
     rintro _ ⟨x, rfl⟩
     refine (SmoothAt.oneJetBundle_map ?_ ?_ ?_ smoothAt_id).smoothWithinAt
-    · refine' (φ.smoothAt_inv _).comp ?_ smoothAt_snd; exact mem_range_self _
-    · refine' (ψ.smoothAt_inv _).comp ?_ smoothAt_snd; exact mem_range_self _
+    · refine (φ.smoothAt_inv ?_).comp (φ.transfer ψ x, (φ.transfer ψ x).proj.1) smoothAt_snd
+      exact mem_range_self _
+    · refine (ψ.smoothAt_inv ?_).comp (φ.transfer ψ x, (φ.transfer ψ x).proj.2) smoothAt_snd
+      exact mem_range_self _
     have' :=
       ContMDiffAt.mfderiv (fun _ ↦ φ) (fun x : OneJetBundle IM M IN N ↦ φ.invFun x.1.1)
         (φ.smooth_to.smoothAt.comp _ smoothAt_snd)
diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean
index d333e6aa..7637ab47 100644
--- a/SphereEversion/Local/SphereEversion.lean
+++ b/SphereEversion/Local/SphereEversion.lean
@@ -278,7 +278,7 @@ def locFormalEversionAux : HtpyJetSec E E where
   φ_diff := by
     refine contDiff_iff_contDiffAt.mpr fun x ↦ ?_
     cases' eq_or_ne x.2 0 with hx hx
-    · refine' contDiffAt_const.congr_of_eventuallyEq ?_; exact 0
+    · refine (contDiffAt_const (c := 0)).congr_of_eventuallyEq ?_
       have : (fun x ↦ ‖x‖ ^ 2) ⁻¹' Iio (1 / 4) ∈ 𝓝 (0 : E) := by
         refine IsOpen.mem_nhds ?_ ?_
         · exact isOpen_Iio.preimage (contDiff_norm_sq ℝ (n :=∞)).continuous
@@ -299,8 +299,6 @@ def locFormalEversionAux : HtpyJetSec E E where
       show smoothStep (‖x‖ ^ 2) • locFormalEversionAuxφ ω (smoothStep t) x = 0
       simp_rw [hx, zero_smul]
     refine ContDiffAt.smul ?_ ?_
-    -- Porting note: the next hack wasn't necessary in Lean 3
-    let _ : NormedSpace ℝ E := InnerProductSpace.toNormedSpace
     · exact (smoothStep.smooth.comp <| (contDiff_norm_sq ℝ).comp contDiff_snd).contDiffAt
     · exact (smooth_at_locFormalEversionAuxφ ω (show (Prod.map smoothStep id x).2 ≠ 0 from hx)).comp x
         (smoothStep.smooth.prod_map contDiff_id).contDiffAt