diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean
index 788aed17..6bcd2a92 100644
--- a/SphereEversion/Global/Gromov.lean
+++ b/SphereEversion/Global/Gromov.lean
@@ -98,16 +98,16 @@ theorem RelMfld.Ample.satisfiesHPrinciple' (hRample : R.Ample) (hRopen : IsOpen
     intro m
     rcases hε m with ⟨φ, ψ, ⟨e, rfl⟩, hφψ⟩
     have : φ '' ball e 1 ∈ 𝓝 (φ e) := by
-      rw [← φ.openEmbedding.map_nhds_eq]
+      rw [← φ.isOpenEmbedding.map_nhds_eq]
       exact image_mem_map (ball_mem_nhds e zero_lt_one)
     use φ '' (ball e 1), this; clear this
     intro K₁ hK₁ K₀ K₀K₁ K₀_cpct K₁_cpct C f C_closed P₀f fC
     have K₁φ : K₁ ⊆ range φ := SurjOn.subset_range hK₁
     have K₀φ : K₀ ⊆ range φ := K₀K₁.trans interior_subset |>.trans K₁φ
     replace K₀_cpct : IsCompact (φ ⁻¹' K₀) :=
-      φ.openEmbedding.toIsInducing.isCompact_preimage' K₀_cpct K₀φ
+      φ.isOpenEmbedding.toIsInducing.isCompact_preimage' K₀_cpct K₀φ
     replace K₁_cpct : IsCompact (φ ⁻¹' K₁) :=
-      φ.openEmbedding.toIsInducing.isCompact_preimage' K₁_cpct K₁φ
+      φ.isOpenEmbedding.toIsInducing.isCompact_preimage' K₁_cpct K₁φ
     have K₀K₁' : φ ⁻¹' K₀ ⊆ interior (φ ⁻¹' K₁) := by
       rw [← φ.isOpenMap.preimage_interior_eq_interior_preimage φ.continuous]
       gcongr
diff --git a/SphereEversion/Global/LocalizedConstruction.lean b/SphereEversion/Global/LocalizedConstruction.lean
index 01ffad50..1656e7a4 100644
--- a/SphereEversion/Global/LocalizedConstruction.lean
+++ b/SphereEversion/Global/LocalizedConstruction.lean
@@ -54,7 +54,7 @@ theorem OpenSmoothEmbedding.improve_formalSol (φ : OpenSmoothEmbedding 𝓘(ℝ
   have h𝓕C : ∀ᶠ x : EM near L.C, 𝓕.IsHolonomicAt x := by
     rw [eventually_nhdsSet_iff_forall] at hFC ⊢
     intro e he
-    rw [φ.inducing.nhds_eq_comap, eventually_comap]
+    rw [φ.isInducing.nhds_eq_comap, eventually_comap]
     apply (hFC _ he).mono
     rintro x hx e rfl
     exact F.isHolonomicLocalize p hFφψ e hx
diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean
index d8e1024b..a2f5f287 100644
--- a/SphereEversion/Global/SmoothEmbedding.lean
+++ b/SphereEversion/Global/SmoothEmbedding.lean
@@ -128,11 +128,11 @@ end
 
 open Filter
 
-theorem openEmbedding : IsOpenEmbedding f :=
+theorem isOpenEmbedding : IsOpenEmbedding f :=
   isOpenEmbedding_of_continuous_injective_open f.continuous f.injective f.isOpenMap
 
-theorem inducing : IsInducing f :=
-  f.openEmbedding.toIsInducing
+theorem isInducing : IsInducing f :=
+  f.isOpenEmbedding.toIsInducing
 
 theorem forall_near' {P : M → Prop} {A : Set M'} (h : ∀ᶠ m near f ⁻¹' A, P m) :
     ∀ᶠ m' near A ∩ range f, ∀ m, m' = f m → P m := by