feat: add (m)differentiableAt_of_(m)fderiv_injective (#35284)

and versions for `(m)fderivWithin` versions. This generalises the existing lemmas `(m)differentiableAt_of_isInvertible_(m)fderiv` and friends.

Extracted from #35078; from the path to immersions, embeddings and submanifolds.

Author: grunweg

Mathlib/Analysis/Calculus/FDeriv/Const.lean

@@ -294,22 +294,28 @@ theorem hasFDerivWithinAt_singleton (f : E → F) (x : E) :
   rw [accPt_iff_clusterPt, inf_principal]
   simp [ClusterPt]
 
-@[fun_prop]
+@[fun_prop, nontriviality]
 theorem hasFDerivWithinAt_of_subsingleton [h : Subsingleton E] (f : E → F) (s : Set E) (x : E) :
     HasFDerivWithinAt f (0 : E →L[𝕜] F) s x := by
   obtain rfl | ⟨a, rfl⟩ := s.eq_empty_or_singleton_of_subsingleton
   · simp
   · exact HasFDerivWithinAt.singleton
 
-@[fun_prop]
+@[fun_prop, nontriviality]
 theorem hasFDerivAt_of_subsingleton [h : Subsingleton E] (f : E → F) (x : E) :
     HasFDerivAt f (0 : E →L[𝕜] F) x := by
   rw [← hasFDerivWithinAt_univ, subsingleton_univ.eq_singleton_of_mem (mem_univ x)]
   exact hasFDerivWithinAt_singleton f x
 
+@[nontriviality]
 theorem differentiable_of_subsingleton [Subsingleton E] {f : E → F} : Differentiable 𝕜 f :=
   fun x ↦ (hasFDerivAt_of_subsingleton f x (𝕜 := 𝕜)).differentiableAt
 
+@[nontriviality]
+theorem differentiableWithinAt_of_subsingleton [Subsingleton E] :
+    DifferentiableWithinAt 𝕜 f s x :=
+  (differentiable_of_subsingleton x).differentiableWithinAt
+
 @[fun_prop]
 theorem differentiableOn_singleton : DifferentiableOn 𝕜 f {x} :=
   forall_eq.2 (hasFDerivWithinAt_singleton f x).differentiableWithinAt
@@ -324,18 +330,28 @@ theorem hasFDerivAt_zero_of_eventually_const (c : F) (hf : f =ᶠ[𝓝 x] fun _
 
 end Const
 
-theorem differentiableWithinAt_of_isInvertible_fderivWithin
-    (hf : (fderivWithin 𝕜 f s x).IsInvertible) : DifferentiableWithinAt 𝕜 f s x := by
-  contrapose hf
-  rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
+/-- If `f : E → F` has injective differential within `s` at `x`,
+it is differentiable within `s` at `x`. -/
+lemma differentiableWithinAt_of_fderivWithin_injective (hf : Injective (fderivWithin 𝕜 f s x)) :
+    DifferentiableWithinAt 𝕜 f s x := by
+  nontriviality E
   contrapose! hf
-  rcases ContinuousLinearMap.isInvertible_zero_iff.1 hf with ⟨hE, hF⟩
-  exact (hasFDerivAt_of_subsingleton _ _).differentiableAt.differentiableWithinAt
+  rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
+  exact not_injective_const
 
-theorem differentiableAt_of_isInvertible_fderiv
-    (hf : (fderiv 𝕜 f x).IsInvertible) : DifferentiableAt 𝕜 f x := by
+/-- If `f : E → F` has injective differential at `x`, it is differentiable at `x`. -/
+lemma differentiableAt_of_fderiv_injective (hf : Injective (fderiv 𝕜 f x)) :
+    DifferentiableAt 𝕜 f x := by
   simp only [← differentiableWithinAt_univ, ← fderivWithin_univ] at hf ⊢
-  exact differentiableWithinAt_of_isInvertible_fderivWithin hf
+  exact differentiableWithinAt_of_fderivWithin_injective hf
+
+theorem differentiableWithinAt_of_isInvertible_fderivWithin
+    (hf : (fderivWithin 𝕜 f s x).IsInvertible) : DifferentiableWithinAt 𝕜 f s x :=
+  differentiableWithinAt_of_fderivWithin_injective hf.injective
+
+theorem differentiableAt_of_isInvertible_fderiv
+    (hf : (fderiv 𝕜 f x).IsInvertible) : DifferentiableAt 𝕜 f x :=
+  differentiableAt_of_fderiv_injective hf.injective
 
 /-! ### Support of derivatives -/
 

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

@@ -30,7 +30,7 @@ noncomputable section
 assert_not_exists tangentBundleCore
 
 open scoped Topology Manifold
-open Set Bundle ChartedSpace
+open Function Set Bundle ChartedSpace
 
 section DerivativesProperties
 
@@ -543,26 +543,43 @@ theorem mfderivWithin_zero_of_not_mdifferentiableWithinAt
 theorem mfderiv_zero_of_not_mdifferentiableAt (h : ¬MDifferentiableAt I I' f x) :
     mfderiv I I' f x = 0 := by simp only [mfderiv, h, if_neg, not_false_iff]
 
+@[nontriviality]
 theorem mdifferentiable_of_subsingleton [Subsingleton E] : MDifferentiable I I' f := by
   intro x
   have : Subsingleton H := I.injective.subsingleton
   have : DiscreteTopology M := discreteTopology H M
   simp only [mdifferentiableAt_iff, continuous_of_discreteTopology.continuousAt, true_and]
   exact (hasFDerivAt_of_subsingleton _ _).differentiableAt.differentiableWithinAt
 
-theorem mdifferentiableWithinAt_of_isInvertible_mfderivWithin
-    (hf : (mfderivWithin I I' f s x).IsInvertible) : MDifferentiableWithinAt I I' f s x := by
-  contrapose hf
-  rw [mfderivWithin_zero_of_not_mdifferentiableWithinAt hf]
+@[nontriviality]
+theorem mdifferentiableWithinAt_of_subsingleton [Subsingleton E] :
+    MDifferentiableWithinAt I I' f s x :=
+  (mdifferentiable_of_subsingleton x).mdifferentiableWithinAt
+
+/-- If `f : M → M'` has injective differential at `x` within `s`,
+it is `MDifferentiable` at `x` within `s`. -/
+lemma mdifferentiableWithinAt_of_mfderivWithin_injective
+    (hf : Injective (mfderivWithin I I' f s x)) :
+    MDifferentiableWithinAt I I' f s x := by
+  nontriviality E
+  have : Nontrivial (TangentSpace I x) := inferInstanceAs (Nontrivial E)
   contrapose! hf
-  rcases ContinuousLinearMap.isInvertible_zero_iff.1 hf with ⟨hE, hF⟩
-  have : Subsingleton E := hE
-  exact mdifferentiable_of_subsingleton.mdifferentiableAt.mdifferentiableWithinAt
+  rw [mfderivWithin_zero_of_not_mdifferentiableWithinAt hf]
+  exact not_injective_const
 
-theorem mdifferentiableAt_of_isInvertible_mfderiv
-    (hf : (mfderiv I I' f x).IsInvertible) : MDifferentiableAt I I' f x := by
+/-- 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
   simp only [← mdifferentiableWithinAt_univ, ← mfderivWithin_univ] at hf ⊢
-  exact mdifferentiableWithinAt_of_isInvertible_mfderivWithin hf
+  exact mdifferentiableWithinAt_of_mfderivWithin_injective hf
+
+theorem mdifferentiableWithinAt_of_isInvertible_mfderivWithin
+    (hf : (mfderivWithin I I' f s x).IsInvertible) : MDifferentiableWithinAt I I' f s x :=
+  mdifferentiableWithinAt_of_mfderivWithin_injective hf.injective
+
+theorem mdifferentiableAt_of_isInvertible_mfderiv
+    (hf : (mfderiv I I' f x).IsInvertible) : MDifferentiableAt I I' f x :=
+  mdifferentiableAt_of_mfderiv_injective hf.injective
 
 theorem HasMFDerivWithinAt.mono (h : HasMFDerivWithinAt I I' f t x f') (hst : s ⊆ t) :
     HasMFDerivWithinAt I I' f s x f' :=

Mathlib/Logic/Function/Basic.lean

@@ -81,6 +81,12 @@ protected theorem Bijective.surjective {f : α → β} (hf : Bijective f) : Surj
 theorem not_injective_iff : ¬ Injective f ↔ ∃ a b, f a = f b ∧ a ≠ b := by
   simp only [Injective, not_forall, exists_prop]
 
+@[simp] lemma not_injective_const {α β : Type*} [Nontrivial α] {b : β} :
+    ¬ Injective (fun _ : α ↦ b) := by
+  rw [not_injective_iff]
+  obtain ⟨a₁, a₂, h⟩ := exists_pair_ne α
+  exact ⟨a₁, a₂, rfl, h⟩
+
 /-- If the co-domain `β` of an injective function `f : α → β` has decidable equality, then
 the domain `α` also has decidable equality. -/
 protected def Injective.decidableEq [DecidableEq β] (I : Injective f) : DecidableEq α :=