∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} {E₃ : Type u_4} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : NormedAddCommGroup E₃] [inst_4 : NormedSpace 𝕜 E₃] {H : Type u_6} {G : Type u_8}
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E₁ H}
  {J : ModelWithCorners 𝕜 E₃ G} {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsImmersion I J n f → Topology.IsEmbedding f → Manifold.IsSmoothEmbedding I J n f