perf: make LocalInvariantProp a structure (#12552)

* Also redefine `MDifferentiableWithinAt` and `MDifferentiableAt` so that they are using `LiftProp[Within]At`.
* This causes a speedup in the old proof of `ContMDiffWithinAt.cle_arrowCongr` by 25%.
* Also give some extra information in the proof of `ContMDiffWithinAt.cle_arrowCongr` to speed it up by another factor of 4.
* A bit of the fallout (e.g. in `hasSmoothAddSelf`) is from Lean unfolding *way* too many definitions to make things definitionally equal. Since `LiftPropWithinAt` is now a structure, the old proofs now break, unless you rewrite with `chartedSpaceSelf_prod`), causing much less defeq-abuse.
* The new lemmas `MDifferentiableWithinAt.differentiableWithinAt_writtenInExtChartAt` and `MDifferentiableAt.differentiableWithinAt_writtenInExtChartAt` have a bit long names. This is to avoid naming clash with the existing `MDifferentiableWithinAt.differentiableWithinAt`. I'm open for other suggestions.

Mathlib/Geometry/Manifold/Algebra/Monoid.lean

@@ -339,7 +339,7 @@ theorem contMDiffWithinAt_finprod (lf : LocallyFinite fun i ↦ mulSupport <| f
 theorem contMDiffWithinAt_finset_prod' (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
     ContMDiffWithinAt I' I n (∏ i in t, f i) s x :=
   Finset.prod_induction f (fun f => ContMDiffWithinAt I' I n f s x) (fun _ _ hf hg => hf.mul hg)
-    contMDiffWithinAt_const h
+    (contMDiffWithinAt_const (c := 1)) h
 #align cont_mdiff_within_at_finset_prod' contMDiffWithinAt_finset_prod'
 #align cont_mdiff_within_at_finset_sum' contMDiffWithinAt_finset_sum'
 
@@ -514,8 +514,10 @@ section
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
   [NormedSpace 𝕜 E]
 
-instance hasSmoothAddSelf : SmoothAdd 𝓘(𝕜, E) E :=
-  ⟨by rw [← modelWithCornersSelf_prod]; exact contDiff_add.contMDiff⟩
+instance hasSmoothAddSelf : SmoothAdd 𝓘(𝕜, E) E := by
+  constructor
+  rw [← modelWithCornersSelf_prod, chartedSpaceSelf_prod]
+  exact contDiff_add.contMDiff
 #align has_smooth_add_self hasSmoothAddSelf
 
 end

Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

@@ -245,8 +245,9 @@ variable {I I'}
 /-! ### Deducing smoothness from higher smoothness -/
 
 theorem ContMDiffWithinAt.of_le (hf : ContMDiffWithinAt I I' n f s x) (le : m ≤ n) :
-    ContMDiffWithinAt I I' m f s x :=
-  ⟨hf.1, hf.2.of_le le⟩
+    ContMDiffWithinAt I I' m f s x := by
+  simp only [ContMDiffWithinAt, LiftPropWithinAt] at hf ⊢
+  exact ⟨hf.1, hf.2.of_le le⟩
 #align cont_mdiff_within_at.of_le ContMDiffWithinAt.of_le
 
 theorem ContMDiffAt.of_le (hf : ContMDiffAt I I' n f x) (le : m ≤ n) : ContMDiffAt I I' m f x :=
@@ -327,8 +328,8 @@ theorem contMDiffWithinAt_iff :
     ContMDiffWithinAt I I' n f s x ↔
       ContinuousWithinAt f s x ∧
         ContDiffWithinAt 𝕜 n (extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm)
-          ((extChartAt I x).symm ⁻¹' s ∩ range I) (extChartAt I x x) :=
-  Iff.rfl
+          ((extChartAt I x).symm ⁻¹' s ∩ range I) (extChartAt I x x) := by
+  simp_rw [ContMDiffWithinAt, liftPropWithinAt_iff']; rfl
 #align cont_mdiff_within_at_iff contMDiffWithinAt_iff
 
 /-- One can reformulate smoothness within a set at a point as continuity within this set at this
@@ -345,8 +346,9 @@ theorem contMDiffWithinAt_iff' :
         ContDiffWithinAt 𝕜 n (extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm)
           ((extChartAt I x).target ∩
             (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
-          (extChartAt I x x) :=
-  and_congr_right fun hc => contDiffWithinAt_congr_nhds <|
+          (extChartAt I x x) := by
+  simp only [ContMDiffWithinAt, liftPropWithinAt_iff']
+  exact and_congr_right fun hc => contDiffWithinAt_congr_nhds <|
     hc.nhdsWithin_extChartAt_symm_preimage_inter_range I I'
 #align cont_mdiff_within_at_iff' contMDiffWithinAt_iff'
 
@@ -355,7 +357,7 @@ point, and smoothness in the corresponding extended chart in the target. -/
 theorem contMDiffWithinAt_iff_target :
     ContMDiffWithinAt I I' n f s x ↔
       ContinuousWithinAt f s x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (extChartAt I' (f x) ∘ f) s x := by
-  simp_rw [ContMDiffWithinAt, LiftPropWithinAt, ← and_assoc]
+  simp_rw [ContMDiffWithinAt, liftPropWithinAt_iff', ← and_assoc]
   have cont :
     ContinuousWithinAt f s x ∧ ContinuousWithinAt (extChartAt I' (f x) ∘ f) s x ↔
         ContinuousWithinAt f s x :=

Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean

@@ -50,7 +50,7 @@ section Module
 
 theorem contMDiffWithinAt_iff_contDiffWithinAt {f : E → E'} {s : Set E} {x : E} :
     ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x := by
-  simp (config := { contextual := true }) only [ContMDiffWithinAt, LiftPropWithinAt,
+  simp (config := { contextual := true }) only [ContMDiffWithinAt, liftPropWithinAt_iff',
     ContDiffWithinAtProp, iff_def, mfld_simps]
   exact ContDiffWithinAt.continuousWithinAt
 #align cont_mdiff_within_at_iff_cont_diff_within_at contMDiffWithinAt_iff_contDiffWithinAt
@@ -235,7 +235,6 @@ theorem ContMDiff.clm_postcomp {f : M → F₂ →L[𝕜] F₃} (hf : ContMDiff
       (fun y ↦ (f y).postcomp F₁ : M → (F₁ →L[𝕜] F₂) →L[𝕜] (F₁ →L[𝕜] F₃)) := fun x ↦
   (hf x).clm_postcomp
 
-set_option maxHeartbeats 400000 in
 theorem ContMDiffWithinAt.cle_arrowCongr {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄}
     {s : Set M} {x : M}
     (hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n (fun x ↦ ((f x).symm : F₂ →L[𝕜] F₁)) s x)
@@ -244,7 +243,7 @@ theorem ContMDiffWithinAt.cle_arrowCongr {f : M → F₁ ≃L[𝕜] F₂} {g : M
       (fun y ↦ (f y).arrowCongr (g y) : M → (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) s x :=
   show ContMDiffWithinAt I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] (F₂ →L[𝕜] F₄)) n
     (fun y ↦ (((f y).symm : F₂ →L[𝕜] F₁).precomp F₄).comp ((g y : F₃ →L[𝕜] F₄).postcomp F₁)) s x
-  from hf.clm_precomp.clm_comp hg.clm_postcomp
+  from hf.clm_precomp (F₃ := F₄) |>.clm_comp <| hg.clm_postcomp (F₁ := F₁)
 
 nonrec theorem ContMDiffAt.cle_arrowCongr {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} {x : M}
     (hf : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n (fun x ↦ ((f x).symm : F₂ →L[𝕜] F₁)) x)

Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

@@ -167,7 +167,7 @@ protected theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N →
       (contDiffWithinAt_ext_coord_change I' (f x₀ (g x₀)) (f x₂ (g x₂)) <|
             PartialEquiv.mem_symm_trans_source _ (mem_extChartAt_source I' (f x₂ (g x₂)))
               h3x₂).differentiableWithinAt le_top
-    have h3f := (h2x₂.mdifferentiableAt le_rfl).2
+    have h3f := (h2x₂.mdifferentiableAt le_rfl).differentiableWithinAt_writtenInExtChartAt
     refine' fderivWithin.comp₃ _ hI' h3f hI _ _ _ _ (I.unique_diff _ <| mem_range_self _)
     · exact fun x _ => mem_range_self _
     · exact fun x _ => mem_range_self _

Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

@@ -161,9 +161,11 @@ this point. (When the property is local and invariant, it will in fact hold usin
 `liftPropWithinAt_indep_chart`). We require continuity in the lifted property, as otherwise one
 single chart might fail to capture the behavior of the function.
 -/
-def LiftPropWithinAt (P : (H → H') → Set H → H → Prop) (f : M → M') (s : Set M) (x : M) : Prop :=
-  ContinuousWithinAt f s x ∧
-    P (chartAt H' (f x) ∘ f ∘ (chartAt H x).symm) ((chartAt H x).symm ⁻¹' s) (chartAt H x x)
+@[mk_iff liftPropWithinAt_iff']
+structure LiftPropWithinAt (P : (H → H') → Set H → H → Prop) (f : M → M') (s : Set M) (x : M) :
+    Prop where
+  continuousWithinAt : ContinuousWithinAt f s x
+  prop : P (chartAt H' (f x) ∘ f ∘ (chartAt H x).symm) ((chartAt H x).symm ⁻¹' s) (chartAt H x x)
 #align charted_space.lift_prop_within_at ChartedSpace.LiftPropWithinAt
 
 /-- Given a property of germs of functions and sets in the model space, then one defines
@@ -183,7 +185,7 @@ def LiftPropAt (P : (H → H') → Set H → H → Prop) (f : M → M') (x : M)
 theorem liftPropAt_iff {P : (H → H') → Set H → H → Prop} {f : M → M'} {x : M} :
     LiftPropAt P f x ↔
       ContinuousAt f x ∧ P (chartAt H' (f x) ∘ f ∘ (chartAt H x).symm) univ (chartAt H x x) := by
-  rw [LiftPropAt, LiftPropWithinAt, continuousWithinAt_univ, preimage_univ]
+  rw [LiftPropAt, liftPropWithinAt_iff', continuousWithinAt_univ, preimage_univ]
 #align charted_space.lift_prop_at_iff ChartedSpace.liftPropAt_iff
 
 /-- Given a property of germs of functions and sets in the model space, then one defines
@@ -217,17 +219,19 @@ theorem liftPropOn_univ : LiftPropOn P g univ ↔ LiftProp P g := by
 #align structure_groupoid.lift_prop_on_univ StructureGroupoid.liftPropOn_univ
 
 theorem liftPropWithinAt_self {f : H → H'} {s : Set H} {x : H} :
-    LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P f s x := Iff.rfl
+    LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P f s x :=
+  liftPropWithinAt_iff' ..
 #align structure_groupoid.lift_prop_within_at_self StructureGroupoid.liftPropWithinAt_self
 
 theorem liftPropWithinAt_self_source {f : H → M'} {s : Set H} {x : H} :
-    LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (chartAt H' (f x) ∘ f) s x := Iff.rfl
+    LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (chartAt H' (f x) ∘ f) s x :=
+  liftPropWithinAt_iff' ..
 #align structure_groupoid.lift_prop_within_at_self_source StructureGroupoid.liftPropWithinAt_self_source
 
 theorem liftPropWithinAt_self_target {f : M → H'} :
     LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧
       P (f ∘ (chartAt H x).symm) ((chartAt H x).symm ⁻¹' s) (chartAt H x x) :=
-  Iff.rfl
+  liftPropWithinAt_iff' ..
 #align structure_groupoid.lift_prop_within_at_self_target StructureGroupoid.liftPropWithinAt_self_target
 
 namespace LocalInvariantProp
@@ -242,6 +246,7 @@ theorem liftPropWithinAt_iff {f : M → M'} :
         P (chartAt H' (f x) ∘ f ∘ (chartAt H x).symm)
           ((chartAt H x).target ∩ (chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source))
           (chartAt H x x) := by
+  rw [liftPropWithinAt_iff']
   refine' and_congr_right fun hf ↦ hG.congr_set _
   exact PartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter hf
     (mem_chart_source H x) (chart_source_mem_nhds H' (f x))
@@ -302,8 +307,10 @@ theorem liftPropWithinAt_indep_chart_aux (he : e ∈ G.maximalAtlas M) (xe : x 
 theorem liftPropWithinAt_indep_chart [HasGroupoid M G] [HasGroupoid M' G']
     (he : e ∈ G.maximalAtlas M) (xe : x ∈ e.source) (hf : f ∈ G'.maximalAtlas M')
     (xf : g x ∈ f.source) :
-    LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ P (f ∘ g ∘ e.symm) (e.symm ⁻¹' s) (e x) :=
-  and_congr_right <|
+    LiftPropWithinAt P g s x ↔
+    ContinuousWithinAt g s x ∧ P (f ∘ g ∘ e.symm) (e.symm ⁻¹' s) (e x) := by
+  simp only [liftPropWithinAt_iff']
+  exact and_congr_right <|
     hG.liftPropWithinAt_indep_chart_aux (chart_mem_maximalAtlas _ _) (mem_chart_source _ _) he xe
       (chart_mem_maximalAtlas _ _) (mem_chart_source _ _) hf xf
 #align structure_groupoid.local_invariant_prop.lift_prop_within_at_indep_chart StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart
@@ -312,7 +319,7 @@ theorem liftPropWithinAt_indep_chart [HasGroupoid M G] [HasGroupoid M' G']
 theorem liftPropWithinAt_indep_chart_source [HasGroupoid M G] (he : e ∈ G.maximalAtlas M)
     (xe : x ∈ e.source) :
     LiftPropWithinAt P g s x ↔ LiftPropWithinAt P (g ∘ e.symm) (e.symm ⁻¹' s) (e x) := by
-  rw [liftPropWithinAt_self_source, LiftPropWithinAt,
+  rw [liftPropWithinAt_self_source, liftPropWithinAt_iff',
     e.symm.continuousWithinAt_iff_continuousWithinAt_comp_right xe, e.symm_symm]
   refine' and_congr Iff.rfl _
   rw [Function.comp_apply, e.left_inv xe, ← Function.comp.assoc,
@@ -324,7 +331,7 @@ theorem liftPropWithinAt_indep_chart_source [HasGroupoid M G] (he : e ∈ G.maxi
 theorem liftPropWithinAt_indep_chart_target [HasGroupoid M' G'] (hf : f ∈ G'.maximalAtlas M')
     (xf : g x ∈ f.source) :
     LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ LiftPropWithinAt P (f ∘ g) s x := by
-  rw [liftPropWithinAt_self_target, LiftPropWithinAt, and_congr_right_iff]
+  rw [liftPropWithinAt_self_target, liftPropWithinAt_iff', and_congr_right_iff]
   intro hg
   simp_rw [(f.continuousAt xf).comp_continuousWithinAt hg, true_and_iff]
   exact hG.liftPropWithinAt_indep_chart_target_aux (mem_chart_source _ _)
@@ -356,7 +363,7 @@ theorem liftPropOn_indep_chart [HasGroupoid M G] [HasGroupoid M' G'] (he : e ∈
 
 theorem liftPropWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
     LiftPropWithinAt P g (s ∩ t) x ↔ LiftPropWithinAt P g s x := by
-  rw [LiftPropWithinAt, LiftPropWithinAt, continuousWithinAt_inter' ht, hG.congr_set]
+  rw [liftPropWithinAt_iff', liftPropWithinAt_iff', continuousWithinAt_inter' ht, hG.congr_set]
   simp_rw [eventuallyEq_set, mem_preimage,
     (chartAt _ x).eventually_nhds' (fun x ↦ x ∈ s ∩ t ↔ x ∈ s) (mem_chart_source _ x)]
   exact (mem_nhdsWithin_iff_eventuallyEq.mp ht).symm.mem_iff
@@ -441,6 +448,7 @@ theorem liftPropOn_congr_iff (h₁ : ∀ y ∈ s, g' y = g y) : LiftPropOn P g'
 theorem liftPropWithinAt_mono_of_mem
     (mono_of_mem : ∀ ⦃s x t⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x)
     (h : LiftPropWithinAt P g s x) (hst : s ∈ 𝓝[t] x) : LiftPropWithinAt P g t x := by
+  simp only [liftPropWithinAt_iff'] at h ⊢
   refine' ⟨h.1.mono_of_mem hst, mono_of_mem _ h.2⟩
   simp_rw [← mem_map, (chartAt H x).symm.map_nhdsWithin_preimage_eq (mem_chart_target H x),
     (chartAt H x).left_inv (mem_chart_source H x), hst]
@@ -542,6 +550,7 @@ theorem liftProp_id (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y) :
 theorem liftPropAt_iff_comp_subtype_val (hG : LocalInvariantProp G G' P) {U : Opens M}
     (f : M → M') (x : U) :
     LiftPropAt P f x ↔ LiftPropAt P (f ∘ Subtype.val) x := by
+  simp only [LiftPropAt, liftPropWithinAt_iff']
   congrm ?_ ∧ ?_
   · simp_rw [continuousWithinAt_univ, U.openEmbedding'.continuousAt_iff]
   · apply hG.congr_iff
@@ -550,6 +559,7 @@ theorem liftPropAt_iff_comp_subtype_val (hG : LocalInvariantProp G G' P) {U : Op
 theorem liftPropAt_iff_comp_inclusion (hG : LocalInvariantProp G G' P) {U V : Opens M} (hUV : U ≤ V)
     (f : V → M') (x : U) :
     LiftPropAt P f (Set.inclusion hUV x) ↔ LiftPropAt P (f ∘ Set.inclusion hUV : U → M') x := by
+  simp only [LiftPropAt, liftPropWithinAt_iff']
   congrm ?_ ∧ ?_
   · simp_rw [continuousWithinAt_univ,
       (TopologicalSpace.Opens.openEmbedding_of_le hUV).continuousAt_iff]

Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean

@@ -88,6 +88,7 @@ variable [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M']
 
 theorem mdifferentiableAt_atlas (h : e ∈ atlas H M) {x : M} (hx : x ∈ e.source) :
     MDifferentiableAt I I e x := by
+  rw [mdifferentiableAt_iff]
   refine' ⟨(e.continuousOn x hx).continuousAt (e.open_source.mem_nhds hx), _⟩
   have mem :
     I ((chartAt H x : M → H) x) ∈ I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range I := by
@@ -111,6 +112,7 @@ theorem mdifferentiableOn_atlas (h : e ∈ atlas H M) : MDifferentiableOn I I e
 
 theorem mdifferentiableAt_atlas_symm (h : e ∈ atlas H M) {x : H} (hx : x ∈ e.target) :
     MDifferentiableAt I I 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
     simp only [hx, mfld_simps]

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

@@ -139,6 +139,7 @@ theorem mdifferentiableWithinAt_iff {f : M → M'} {s : Set M} {x : M} :
       ContinuousWithinAt f s x ∧
         DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
           ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) ((extChartAt I x) x) := by
+  rw [mdifferentiableWithinAt_iff']
   refine' and_congr Iff.rfl (exists_congr fun f' => _)
   rw [inter_comm]
   simp only [HasFDerivWithinAt, nhdsWithin_inter, nhdsWithin_extChartAt_target_eq]
@@ -183,8 +184,9 @@ theorem HasMFDerivWithinAt.mdifferentiableWithinAt (h : HasMFDerivWithinAt I I'
 #align has_mfderiv_within_at.mdifferentiable_within_at HasMFDerivWithinAt.mdifferentiableWithinAt
 
 theorem HasMFDerivAt.mdifferentiableAt (h : HasMFDerivAt I I' f x f') :
-    MDifferentiableAt I I' f x :=
-  ⟨h.1, ⟨f', h.2⟩⟩
+    MDifferentiableAt I I' f x := by
+  rw [mdifferentiableAt_iff]
+  exact ⟨h.1, ⟨f', h.2⟩⟩
 #align has_mfderiv_at.mdifferentiable_at HasMFDerivAt.mdifferentiableAt
 
 @[simp, mfld_simps]
@@ -246,9 +248,9 @@ protected theorem MDifferentiableWithinAt.mfderivWithin (h : MDifferentiableWith
 
 theorem MDifferentiableAt.hasMFDerivAt (h : MDifferentiableAt I I' f x) :
     HasMFDerivAt I I' f x (mfderiv I I' f x) := by
-  refine' ⟨h.1, _⟩
+  refine' ⟨h.continuousAt, _⟩
   simp only [mfderiv, h, if_pos, mfld_simps]
-  exact DifferentiableWithinAt.hasFDerivWithinAt h.2
+  exact DifferentiableWithinAt.hasFDerivWithinAt h.differentiableWithinAt_writtenInExtChartAt
 #align mdifferentiable_at.has_mfderiv_at MDifferentiableAt.hasMFDerivAt
 
 protected theorem MDifferentiableAt.mfderiv (h : MDifferentiableAt I I' f x) :
@@ -281,27 +283,26 @@ theorem mfderivWithin_subset (st : s ⊆ t) (hs : UniqueMDiffWithinAt I s x)
 
 theorem MDifferentiableWithinAt.mono (hst : s ⊆ t) (h : MDifferentiableWithinAt I I' f t x) :
     MDifferentiableWithinAt I I' f s x :=
-  ⟨ContinuousWithinAt.mono h.1 hst,
-    DifferentiableWithinAt.mono h.2 (inter_subset_inter (preimage_mono hst) (Subset.refl _))⟩
+  ⟨ContinuousWithinAt.mono h.1 hst, DifferentiableWithinAt.mono
+    h.differentiableWithinAt_writtenInExtChartAt
+    (inter_subset_inter_left _ (preimage_mono hst))⟩
 #align mdifferentiable_within_at.mono MDifferentiableWithinAt.mono
 
 theorem mdifferentiableWithinAt_univ :
     MDifferentiableWithinAt I I' f univ x ↔ MDifferentiableAt I I' f x := by
-  simp only [MDifferentiableWithinAt, MDifferentiableAt, continuousWithinAt_univ, mfld_simps]
+  simp_rw [MDifferentiableWithinAt, MDifferentiableAt, ChartedSpace.LiftPropAt]
 #align mdifferentiable_within_at_univ mdifferentiableWithinAt_univ
 
 theorem mdifferentiableWithinAt_inter (ht : t ∈ 𝓝 x) :
     MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x := by
-  rw [MDifferentiableWithinAt, MDifferentiableWithinAt, extChartAt_preimage_inter_eq,
-    differentiableWithinAt_inter, continuousWithinAt_inter ht]
-  exact extChartAt_preimage_mem_nhds I ht
+  rw [MDifferentiableWithinAt, MDifferentiableWithinAt,
+    (differentiable_within_at_localInvariantProp I I').liftPropWithinAt_inter ht]
 #align mdifferentiable_within_at_inter mdifferentiableWithinAt_inter
 
 theorem mdifferentiableWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
     MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x := by
-  rw [MDifferentiableWithinAt, MDifferentiableWithinAt, extChartAt_preimage_inter_eq,
-    differentiableWithinAt_inter', continuousWithinAt_inter' ht]
-  exact extChartAt_preimage_mem_nhdsWithin I ht
+  rw [MDifferentiableWithinAt, MDifferentiableWithinAt,
+    (differentiable_within_at_localInvariantProp I I').liftPropWithinAt_inter' ht]
 #align mdifferentiable_within_at_inter' mdifferentiableWithinAt_inter'
 
 theorem MDifferentiableAt.mdifferentiableWithinAt (h : MDifferentiableAt I I' f x) :
@@ -440,15 +441,6 @@ theorem HasMFDerivAt.continuousAt (h : HasMFDerivAt I I' f x f') : ContinuousAt
   h.1
 #align has_mfderiv_at.continuous_at HasMFDerivAt.continuousAt
 
-theorem MDifferentiableWithinAt.continuousWithinAt (h : MDifferentiableWithinAt I I' f s x) :
-    ContinuousWithinAt f s x :=
-  h.1
-#align mdifferentiable_within_at.continuous_within_at MDifferentiableWithinAt.continuousWithinAt
-
-theorem MDifferentiableAt.continuousAt (h : MDifferentiableAt I I' f x) : ContinuousAt f x :=
-  h.1
-#align mdifferentiable_at.continuous_at MDifferentiableAt.continuousAt
-
 theorem MDifferentiableOn.continuousOn (h : MDifferentiableOn I I' f s) : ContinuousOn f s :=
   fun x hx => (h x hx).continuousWithinAt
 #align mdifferentiable_on.continuous_on MDifferentiableOn.continuousOn