Remove

Author: grunweg

Mathlib/Geometry/Manifold/ImmersedPoint.lean

@@ -58,34 +58,6 @@ variable {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
   {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n M']
 variable {f : M → M'} {x : M} {n : WithTop ℕ∞}
 
--- TODO: move to the right place!
-/-- If `f : E → F` has injective differential at `x`, it is differentiable at `x`. -/
-lemma differentiableAt_of_fderiv_injective {f : E → F} {x : E} (hf : Injective (fderiv 𝕜 f x)) :
-    DifferentiableAt 𝕜 f x := by
-  replace hf : LinearMap.ker (fderiv 𝕜 f x).toLinearMap = ⊥ := by
-    rw [LinearMap.ker_eq_bot]; exact hf
-  by_cases h: Subsingleton E
-  · exact differentiable_of_subsingleton.differentiableAt
-  · by_contra h'
-    have : (⊥ : Submodule 𝕜 E) = ⊤ := by
-      simp [fderiv_zero_of_not_differentiableAt h', ← hf]
-    have : Subsingleton (Submodule 𝕜 E) := subsingleton_of_bot_eq_top this
-    simp_all only [Submodule.subsingleton_iff]
-
--- TODO: move to e.g. ContMDiff.Basic
-/-- If `f : M → M'` has injective differential at `x`, it is `MDifferentiable` at `x`. -/
-lemma mdifferentiableAt_of_mfderiv_injective {f : M → M'} (hf : Injective (mfderiv I I' f x)) :
-    MDifferentiableAt I I' f x := by
-  replace hf : LinearMap.ker (mfderiv I I' f x).toLinearMap = ⊥ := by
-    rw [LinearMap.ker_eq_bot]; exact hf
-  by_cases h: Subsingleton E
-  · exact mdifferentiable_of_subsingleton.mdifferentiableAt
-  · by_contra h'
-    have : (⊥ : Submodule 𝕜 (TangentSpace I x)) = ⊤ := by
-      simp [mfderiv_zero_of_not_mdifferentiableAt h', ← hf]
-    have : Subsingleton (Submodule 𝕜 E) := subsingleton_of_bot_eq_top this
-    simp_all only [Submodule.subsingleton_iff]
-
 variable (I I' f x) in
 /-- We say a map `f : M → M` splits at `x` if `mfderiv I I' f x` splits,
 i.e. has a continuous left inverse. -/