chore(Geometry/Manifold/MFDeriv): golf using custom elaborators (leanprover-community#36010)

Author: grunweg

Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
 public import Mathlib.Geometry.Manifold.VectorBundle.Tangent
+public import Mathlib.Geometry.Manifold.Notation
 
 /-!
 # Differentiability of models with corners and (extended) charts
@@ -59,27 +60,27 @@ protected theorem hasMFDerivWithinAt {s x} :
     HasMFDerivWithinAt I 𝓘(𝕜, E) I s x (ContinuousLinearMap.id _ _) :=
   I.hasMFDerivAt.hasMFDerivWithinAt
 
-protected theorem mdifferentiableWithinAt {s x} : MDifferentiableWithinAt I 𝓘(𝕜, E) I s x :=
+protected theorem mdifferentiableWithinAt {s x} : MDiffAt[s] I x :=
   I.hasMFDerivWithinAt.mdifferentiableWithinAt
 
-protected theorem mdifferentiableAt {x} : MDifferentiableAt I 𝓘(𝕜, E) I x :=
+protected theorem mdifferentiableAt {x} : MDiffAt I x :=
   I.hasMFDerivAt.mdifferentiableAt
 
-protected theorem mdifferentiableOn {s} : MDifferentiableOn I 𝓘(𝕜, E) I s := fun _ _ =>
+protected theorem mdifferentiableOn {s} : MDiff[s] I := fun _ _ =>
   I.mdifferentiableWithinAt
 
-protected theorem mdifferentiable : MDifferentiable I 𝓘(𝕜, E) I := fun _ => I.mdifferentiableAt
+protected theorem mdifferentiable : MDiff I := fun _ => I.mdifferentiableAt
 
 theorem hasMFDerivWithinAt_symm {x} (hx : x ∈ range I) :
     HasMFDerivWithinAt 𝓘(𝕜, E) I I.symm (range I) x (ContinuousLinearMap.id _ _) :=
   ⟨I.continuousWithinAt_symm,
     (hasFDerivWithinAt_id _ _).congr' (fun _y hy => I.rightInvOn hy.1) ⟨hx, mem_range_self _⟩⟩
 
-theorem mdifferentiableOn_symm : MDifferentiableOn 𝓘(𝕜, E) I I.symm (range I) := fun _x hx =>
+theorem mdifferentiableOn_symm : MDiff[range I] I.symm := fun _x hx =>
   (I.hasMFDerivWithinAt_symm hx).mdifferentiableWithinAt
 
 theorem mdifferentiableWithinAt_symm {z : E} (hz : z ∈ range I) :
-    MDifferentiableWithinAt 𝓘(𝕜, E) I I.symm (range I) z :=
+    MDiffAt[range I] I.symm z :=
   I.mdifferentiableOn_symm z hz
 
 end ModelWithCorners
@@ -91,8 +92,7 @@ section Charts
 variable [IsManifold I 1 M] [IsManifold I' 1 M']
   [IsManifold I'' 1 M''] {e : OpenPartialHomeomorph M H}
 
-theorem mdifferentiableAt_atlas (h : e ∈ atlas H M) {x : M} (hx : x ∈ e.source) :
-    MDifferentiableAt I I e x := by
+theorem mdifferentiableAt_atlas (h : e ∈ atlas H M) {x : M} (hx : x ∈ e.source) : MDiffAt e x := by
   rw [mdifferentiableAt_iff]
   refine ⟨(e.continuousOn x hx).continuousAt (e.open_source.mem_nhds hx), ?_⟩
   have mem :
@@ -110,11 +110,11 @@ theorem mdifferentiableAt_atlas (h : e ∈ atlas H M) {x : M} (hx : x ∈ e.sour
   · simpa only [mfld_simps]
   · apply IsOpen.mem_nhds ((OpenPartialHomeomorph.open_source _).preimage I.continuous_symm) mem.1
 
-theorem mdifferentiableOn_atlas (h : e ∈ atlas H M) : MDifferentiableOn I I e e.source :=
+theorem mdifferentiableOn_atlas (h : e ∈ atlas H M) : MDiff[e.source] e :=
   fun _x hx => (mdifferentiableAt_atlas h hx).mdifferentiableWithinAt
 
 theorem mdifferentiableAt_atlas_symm (h : e ∈ atlas H M) {x : H} (hx : x ∈ e.target) :
-    MDifferentiableAt I I e.symm x := by
+    MDiffAt e.symm x := by
   rw [mdifferentiableAt_iff]
   refine ⟨(e.continuousOn_symm x hx).continuousAt (e.open_target.mem_nhds hx), ?_⟩
   have mem : I x ∈ I.symm ⁻¹' (e.symm ≫ₕ chartAt H (e.symm x)).source ∩ range I := by
@@ -131,7 +131,7 @@ theorem mdifferentiableAt_atlas_symm (h : e ∈ atlas H M) {x : H} (hx : x ∈ e
   · simpa only [mfld_simps]
   · apply IsOpen.mem_nhds ((OpenPartialHomeomorph.open_source _).preimage I.continuous_symm) mem.1
 
-theorem mdifferentiableOn_atlas_symm (h : e ∈ atlas H M) : MDifferentiableOn I I e.symm e.target :=
+theorem mdifferentiableOn_atlas_symm (h : e ∈ atlas H M) : MDiff[e.target] e.symm :=
   fun _x hx => (mdifferentiableAt_atlas_symm h hx).mdifferentiableWithinAt
 
 theorem mdifferentiable_of_mem_atlas (h : e ∈ atlas H M) : e.MDifferentiable I I :=
@@ -151,37 +151,37 @@ include he
 
 nonrec theorem symm : e.symm.MDifferentiable I' I := he.symm
 
-protected theorem mdifferentiableAt {x : M} (hx : x ∈ e.source) : MDifferentiableAt I I' e x :=
+protected theorem mdifferentiableAt {x : M} (hx : x ∈ e.source) : MDiffAt e x :=
   (he.1 x hx).mdifferentiableAt (e.open_source.mem_nhds hx)
 
-theorem mdifferentiableAt_symm {x : M'} (hx : x ∈ e.target) : MDifferentiableAt I' I e.symm x :=
+theorem mdifferentiableAt_symm {x : M'} (hx : x ∈ e.target) : MDiffAt e.symm x :=
   (he.2 x hx).mdifferentiableAt (e.open_target.mem_nhds hx)
 
 theorem symm_comp_deriv {x : M} (hx : x ∈ e.source) :
-    (mfderiv I' I e.symm (e x)).comp (mfderiv I I' e x) =
+    (mfderiv% e.symm (e x)).comp (mfderiv% e x) =
       ContinuousLinearMap.id 𝕜 (TangentSpace I x) := by
-  have : mfderiv I I (e.symm ∘ e) x = (mfderiv I' I e.symm (e x)).comp (mfderiv I I' e x) :=
+  have : mfderiv% (e.symm ∘ e) x = (mfderiv% e.symm (e x)).comp (mfderiv% e x) :=
     mfderiv_comp x (he.mdifferentiableAt_symm (e.map_source hx)) (he.mdifferentiableAt hx)
   rw [← this]
-  have : mfderiv I I (_root_.id : M → M) x = ContinuousLinearMap.id _ _ := mfderiv_id
+  have : mfderiv% (_root_.id : M → M) x = ContinuousLinearMap.id _ _ := mfderiv_id
   rw [← this]
   apply Filter.EventuallyEq.mfderiv_eq
   have : e.source ∈ 𝓝 x := e.open_source.mem_nhds hx
   exact Filter.mem_of_superset this (by mfld_set_tac)
 
 theorem comp_symm_deriv {x : M'} (hx : x ∈ e.target) :
-    (mfderiv I I' e (e.symm x)).comp (mfderiv I' I e.symm x) =
+    (mfderiv% e (e.symm x)).comp (mfderiv% e.symm x) =
       ContinuousLinearMap.id 𝕜 (TangentSpace I' x) :=
   he.symm.symm_comp_deriv hx
 
 /-- The derivative of a differentiable open partial homeomorphism, as a continuous linear
 equivalence between the tangent spaces at `x` and `e x`. -/
 protected def mfderiv (he : e.MDifferentiable I I') {x : M} (hx : x ∈ e.source) :
     TangentSpace I x ≃L[𝕜] TangentSpace I' (e x) :=
-  { mfderiv I I' e x with
-    invFun := mfderiv I' I e.symm (e x)
-    continuous_toFun := (mfderiv I I' e x).cont
-    continuous_invFun := (mfderiv I' I e.symm (e x)).cont
+  { mfderiv% e x with
+    invFun := mfderiv% e.symm (e x)
+    continuous_toFun := (mfderiv% e x).cont
+    continuous_invFun := (mfderiv% e.symm (e x)).cont
     left_inv := fun y => by
       have : (ContinuousLinearMap.id _ _ : TangentSpace I x →L[𝕜] TangentSpace I x) y = y := rfl
       conv_rhs => rw [← this, ← he.symm_comp_deriv hx]
@@ -194,22 +194,22 @@ protected def mfderiv (he : e.MDifferentiable I I') {x : M} (hx : x ∈ e.source
       rw [e.left_inv hx]
       rfl }
 
-theorem mfderiv_bijective {x : M} (hx : x ∈ e.source) : Function.Bijective (mfderiv I I' e x) :=
+theorem mfderiv_bijective {x : M} (hx : x ∈ e.source) : Function.Bijective (mfderiv% e x) :=
   (he.mfderiv hx).bijective
 
-theorem mfderiv_injective {x : M} (hx : x ∈ e.source) : Function.Injective (mfderiv I I' e x) :=
+theorem mfderiv_injective {x : M} (hx : x ∈ e.source) : Function.Injective (mfderiv% e x) :=
   (he.mfderiv hx).injective
 
-theorem mfderiv_surjective {x : M} (hx : x ∈ e.source) : Function.Surjective (mfderiv I I' e x) :=
+theorem mfderiv_surjective {x : M} (hx : x ∈ e.source) : Function.Surjective (mfderiv% e x) :=
   (he.mfderiv hx).surjective
 
-theorem ker_mfderiv_eq_bot {x : M} (hx : x ∈ e.source) : (mfderiv I I' e x).ker = ⊥ :=
+theorem ker_mfderiv_eq_bot {x : M} (hx : x ∈ e.source) : (mfderiv% e x).ker = ⊥ :=
   (he.mfderiv hx).toLinearEquiv.ker
 
-theorem range_mfderiv_eq_top {x : M} (hx : x ∈ e.source) : (mfderiv I I' e x).range = ⊤ :=
+theorem range_mfderiv_eq_top {x : M} (hx : x ∈ e.source) : (mfderiv% e x).range = ⊤ :=
   (he.mfderiv hx).toLinearEquiv.range
 
-theorem range_mfderiv_eq_univ {x : M} (hx : x ∈ e.source) : range (mfderiv I I' e x) = univ :=
+theorem range_mfderiv_eq_univ {x : M} (hx : x ∈ e.source) : range (mfderiv% e x) = univ :=
   (he.mfderiv_surjective hx).range_eq
 
 theorem trans (he' : e'.MDifferentiable I' I'') : (e.trans e').MDifferentiable I I'' := by
@@ -233,23 +233,22 @@ section extChartAt
 variable [IsManifold I 1 M] {s : Set M} {x y : M} {z : E}
 
 theorem hasMFDerivAt_extChartAt (h : y ∈ (chartAt H x).source) :
-    HasMFDerivAt I 𝓘(𝕜, E) (extChartAt I x) y (mfderiv I I (chartAt H x) y :) :=
+    HasMFDerivAt% (extChartAt I x) y (mfderiv% (chartAt H x) y :) :=
   I.hasMFDerivAt.comp y ((mdifferentiable_chart x).mdifferentiableAt h).hasMFDerivAt
 
 theorem hasMFDerivWithinAt_extChartAt (h : y ∈ (chartAt H x).source) :
-    HasMFDerivWithinAt I 𝓘(𝕜, E) (extChartAt I x) s y (mfderiv I I (chartAt H x) y :) :=
+    HasMFDerivAt[s] (extChartAt I x) y (mfderiv% (chartAt H x) y :) :=
   (hasMFDerivAt_extChartAt h).hasMFDerivWithinAt
 
 theorem mdifferentiableAt_extChartAt (h : y ∈ (chartAt H x).source) :
-    MDifferentiableAt I 𝓘(𝕜, E) (extChartAt I x) y :=
+    MDiffAt (extChartAt I x) y :=
   (hasMFDerivAt_extChartAt h).mdifferentiableAt
 
-theorem mdifferentiableOn_extChartAt :
-    MDifferentiableOn I 𝓘(𝕜, E) (extChartAt I x) (chartAt H x).source := fun _y hy =>
-  (hasMFDerivWithinAt_extChartAt hy).mdifferentiableWithinAt
+theorem mdifferentiableOn_extChartAt : MDiff[(chartAt H x).source] (extChartAt I x) :=
+  fun _y hy ↦ (hasMFDerivWithinAt_extChartAt hy).mdifferentiableWithinAt
 
 theorem mdifferentiableWithinAt_extChartAt_symm (h : z ∈ (extChartAt I x).target) :
-    MDifferentiableWithinAt 𝓘(𝕜, E) I (extChartAt I x).symm (range I) z := by
+    MDiffAt[range I] (extChartAt I x).symm z := by
   have Z := I.mdifferentiableWithinAt_symm (extChartAt_target_subset_range x h)
   apply MDifferentiableAt.comp_mdifferentiableWithinAt (I' := I) _ _ Z
   apply mdifferentiableAt_atlas_symm (ChartedSpace.chart_mem_atlas x)
@@ -259,7 +258,7 @@ theorem mdifferentiableWithinAt_extChartAt_symm (h : z ∈ (extChartAt I x).targ
   exact h.2
 
 theorem mdifferentiableOn_extChartAt_symm :
-    MDifferentiableOn 𝓘(𝕜, E) I (extChartAt I x).symm (extChartAt I x).target := by
+    MDiff[(extChartAt I x).target] (extChartAt I x).symm := by
   intro y hy
   exact (mdifferentiableWithinAt_extChartAt_symm hy).mono (extChartAt_target_subset_range x)
 
@@ -268,8 +267,8 @@ theorem mdifferentiableOn_extChartAt_symm :
 Version where the basepoint belongs to `(extChartAt I x).target`. -/
 lemma mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm {x : M}
     {y : E} (hy : y ∈ (extChartAt I x).target) :
-    (mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y)) ∘L
-      (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y) = ContinuousLinearMap.id _ _ := by
+    (mfderiv% (extChartAt I x) ((extChartAt I x).symm y)) ∘L
+      (mfderiv[range I] (extChartAt I x).symm y) = ContinuousLinearMap.id _ _ := by
   have U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range ↑I) y := by
     apply I.uniqueMDiffOn
     exact extChartAt_target_subset_range x hy
@@ -291,8 +290,7 @@ lemma mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm {x : M}
 Version where the basepoint belongs to `(extChartAt I x).source`. -/
 lemma mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm' {x : M}
     {y : M} (hy : y ∈ (extChartAt I x).source) :
-    (mfderiv I 𝓘(𝕜, E) (extChartAt I x) y) ∘L
-      (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) (extChartAt I x y))
+    (mfderiv% (extChartAt I x) y) ∘L (mfderiv[range I] (extChartAt I x).symm (extChartAt I x y))
     = ContinuousLinearMap.id _ _ := by
   have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm
   convert mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm ((extChartAt I x).map_source hy)
@@ -302,17 +300,16 @@ lemma mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm' {x : M}
 Version where the basepoint belongs to `(extChartAt I x).target`. -/
 lemma mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt
     {y : E} (hy : y ∈ (extChartAt I x).target) :
-    (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y) ∘L
-      (mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y))
+    (mfderiv[range I] (extChartAt I x).symm y) ∘L
+      (mfderiv% (extChartAt I x) ((extChartAt I x).symm y))
       = ContinuousLinearMap.id _ _ := by
   have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target hy
   have h''y : (extChartAt I x).symm y ∈ (chartAt H x).source := by
     rwa [← extChartAt_source (I := I)]
   have U' : UniqueMDiffWithinAt I (extChartAt I x).source ((extChartAt I x).symm y) :=
     (isOpen_extChartAt_source x).uniqueMDiffWithinAt h'y
-  have : mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y)
-      = mfderivWithin I 𝓘(𝕜, E) (extChartAt I x) (extChartAt I x).source
-      ((extChartAt I x).symm y) := by
+  have : mfderiv% (extChartAt I x) ((extChartAt I x).symm y)
+      = mfderiv[(extChartAt I x).source] (extChartAt I x) ((extChartAt I x).symm y) := by
     rw [mfderivWithin_eq_mfderiv U']
     exact mdifferentiableAt_extChartAt h''y
   rw [this, ← mfderivWithin_comp_of_eq]; rotate_left
@@ -335,20 +332,19 @@ set_option backward.isDefEq.respectTransparency false in
 Version where the basepoint belongs to `(extChartAt I x).source`. -/
 lemma mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt'
     {y : M} (hy : y ∈ (extChartAt I x).source) :
-    (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) (extChartAt I x y)) ∘L
-      (mfderiv I 𝓘(𝕜, E) (extChartAt I x) y)
+    (mfderiv[range I] (extChartAt I x).symm (extChartAt I x y)) ∘L (mfderiv% (extChartAt I x) y)
       = ContinuousLinearMap.id _ _ := by
   have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm
   convert mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt ((extChartAt I x).map_source hy)
 
 lemma isInvertible_mfderivWithin_extChartAt_symm {y : E} (hy : y ∈ (extChartAt I x).target) :
-    (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y).IsInvertible :=
+    (mfderiv[range I] (extChartAt I x).symm y).IsInvertible :=
   ContinuousLinearMap.IsInvertible.of_inverse
     (mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt hy)
     (mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm hy)
 
 lemma isInvertible_mfderiv_extChartAt {y : M} (hy : y ∈ (extChartAt I x).source) :
-    (mfderiv I 𝓘(𝕜, E) (extChartAt I x) y).IsInvertible := by
+    (mfderiv% (extChartAt I x) y).IsInvertible := by
   have h'y : extChartAt I x y ∈ (extChartAt I x).target := (extChartAt I x).map_source hy
   have Z := ContinuousLinearMap.IsInvertible.of_inverse
     (mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm h'y)
@@ -363,8 +359,8 @@ Use with care as this abuses the defeq `TangentSpace 𝓘(𝕜, E) y = E` for `y
 theorem TangentBundle.continuousLinearMapAt_trivializationAt
     {x₀ x : M} (hx : x ∈ (chartAt H x₀).source) :
     (trivializationAt E (TangentSpace I) x₀).continuousLinearMapAt 𝕜 x =
-      mfderiv I 𝓘(𝕜, E) (extChartAt I x₀) x := by
-  have : MDifferentiableAt I 𝓘(𝕜, E) (extChartAt I x₀) x := mdifferentiableAt_extChartAt hx
+      mfderiv% (extChartAt I x₀) x := by
+  have : MDiffAt (extChartAt I x₀) x := mdifferentiableAt_extChartAt hx
   simp only [extChartAt, OpenPartialHomeomorph.extend, PartialEquiv.coe_trans,
     ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.toFun_eq_coe] at this
   simp [hx, mfderiv, this]
@@ -376,9 +372,8 @@ Use with care as this abuses the defeq `TangentSpace 𝓘(𝕜, E) y = E` for `y
 theorem TangentBundle.symmL_trivializationAt
     {x₀ x : M} (hx : x ∈ (chartAt H x₀).source) :
     (trivializationAt E (TangentSpace I) x₀).symmL 𝕜 x =
-      mfderivWithin 𝓘(𝕜, E) I (extChartAt I x₀).symm (range I) (extChartAt I x₀ x) := by
-  have : MDifferentiableWithinAt 𝓘(𝕜, E) I ((chartAt H x₀).symm ∘ I.symm) (range I)
-      (I (chartAt H x₀ x)) := by
+      mfderiv[range I] (extChartAt I x₀).symm (extChartAt I x₀ x) := by
+  have : MDiffAt[range I] ((chartAt H x₀).symm ∘ I.symm) (I (chartAt H x₀ x)) := by
     simpa using mdifferentiableWithinAt_extChartAt_symm (by simp [hx])
   simp [hx, mfderivWithin, this]
 

Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean

@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel, Floris van Doorn
 module
 
 public import Mathlib.Geometry.Manifold.MFDeriv.Basic
+public import Mathlib.Geometry.Manifold.Notation
 
 /-!
 ### Relations between vector space derivative and manifold derivative
@@ -68,7 +69,7 @@ alias ⟨HasMFDerivAt.hasFDerivAt, HasFDerivAt.hasMFDerivAt⟩ := hasMFDerivAt_i
 /-- For maps between vector spaces, `MDifferentiableWithinAt` and `DifferentiableWithinAt`
 coincide -/
 theorem mdifferentiableWithinAt_iff_differentiableWithinAt :
-    MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x ↔ DifferentiableWithinAt 𝕜 f s x := by
+    MDiffAt[s] f x ↔ DifferentiableWithinAt 𝕜 f s x := by
   simp only [mdifferentiableWithinAt_iff', mfld_simps]
   exact ⟨fun H => H.2, fun H => ⟨H.continuousWithinAt, H⟩⟩
 
@@ -78,7 +79,7 @@ alias ⟨MDifferentiableWithinAt.differentiableWithinAt,
 
 /-- For maps between vector spaces, `MDifferentiableAt` and `DifferentiableAt` coincide -/
 theorem mdifferentiableAt_iff_differentiableAt :
-    MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x ↔ DifferentiableAt 𝕜 f x := by
+    MDiffAt f x ↔ DifferentiableAt 𝕜 f x := by
   simp only [mdifferentiableAt_iff, differentiableWithinAt_univ, mfld_simps]
   exact ⟨fun H => H.2, fun H => ⟨H.continuousAt, H⟩⟩
 
@@ -87,16 +88,15 @@ alias ⟨MDifferentiableAt.differentiableAt, DifferentiableAt.mdifferentiableAt
 
 /-- For maps between vector spaces, `MDifferentiableOn` and `DifferentiableOn` coincide -/
 theorem mdifferentiableOn_iff_differentiableOn :
-    MDifferentiableOn 𝓘(𝕜, E) 𝓘(𝕜, E') f s ↔ DifferentiableOn 𝕜 f s := by
+    MDiff[s] f ↔ DifferentiableOn 𝕜 f s := by
   simp only [MDifferentiableOn, DifferentiableOn,
     mdifferentiableWithinAt_iff_differentiableWithinAt]
 
 alias ⟨MDifferentiableOn.differentiableOn, DifferentiableOn.mdifferentiableOn⟩ :=
   mdifferentiableOn_iff_differentiableOn
 
 /-- For maps between vector spaces, `MDifferentiable` and `Differentiable` coincide -/
-theorem mdifferentiable_iff_differentiable :
-    MDifferentiable 𝓘(𝕜, E) 𝓘(𝕜, E') f ↔ Differentiable 𝕜 f := by
+theorem mdifferentiable_iff_differentiable : MDiff f ↔ Differentiable 𝕜 f := by
   simp only [MDifferentiable, Differentiable, mdifferentiableAt_iff_differentiableAt]
 
 alias ⟨MDifferentiable.differentiable, Differentiable.mdifferentiable⟩ :=
@@ -106,16 +106,16 @@ set_option backward.isDefEq.respectTransparency false in
 /-- For maps between vector spaces, `mfderivWithin` and `fderivWithin` coincide -/
 @[simp]
 theorem mfderivWithin_eq_fderivWithin :
-    mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x = fderivWithin 𝕜 f s x := by
-  by_cases h : MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x
+    mfderiv[s] f x = fderivWithin 𝕜 f s x := by
+  by_cases h : MDiffAt[s] f x
   · simp only [mfderivWithin, h, if_pos, mfld_simps]
   · simp only [mfderivWithin, h, if_neg, not_false_iff]
     rw [mdifferentiableWithinAt_iff_differentiableWithinAt] at h
     exact (fderivWithin_zero_of_not_differentiableWithinAt h).symm
 
 /-- For maps between vector spaces, `mfderiv` and `fderiv` coincide -/
 @[simp]
-theorem mfderiv_eq_fderiv : mfderiv 𝓘(𝕜, E) 𝓘(𝕜, E') f x = fderiv 𝕜 f x := by
+theorem mfderiv_eq_fderiv : mfderiv% f x = fderiv 𝕜 f x := by
   rw [← mfderivWithin_univ, ← fderivWithin_univ]
   exact mfderivWithin_eq_fderivWithin