Bump mathlib again.

Two lemmas renamed, one lemma merged to mathlib, one change of imports.
FunLike was named to DFunLike, with a convenient abbrev in mathlib4#9833,
which we are using as well.

SphereEversion/Global/OneJetBundle.lean

@@ -107,7 +107,7 @@ local notation "FJ¹MM'" => (OneJetSpace I I' : M × M' → Type _)
 
 variable (I I')
 
-instance (p : M × M') : FunLike (OneJetSpace I I' p) (TangentSpace I p.1) (fun _ ↦ TangentSpace I' p.2) where
+instance (p : M × M') : FunLike (OneJetSpace I I' p) (TangentSpace I p.1) (TangentSpace I' p.2) where
   coe := fun φ ↦ φ.toFun
   coe_injective' := fun _ _ h ↦ ContinuousLinearMap.ext (congrFun h)
 
@@ -237,7 +237,7 @@ theorem oneJetBundle_chart_source (x₀ : J¹MM') :
     PartialEquiv.prod_source,
     PartialHomeomorph.coe_coe,
     Trivialization.coe_coe,
-    PartialHomeomorph.refl_localEquiv,
+    PartialHomeomorph.refl_partialEquiv,
     PartialEquiv.refl_source,
     prodChartedSpace_chartAt,
     PartialHomeomorph.prod_toPartialEquiv,
@@ -304,7 +304,7 @@ theorem oneJetBundle_chart_target (x₀ : J¹MM') :
   rw [FiberBundle.chartedSpace_chartAt]
   simp only [prodChartedSpace_chartAt,
     PartialHomeomorph.trans_toPartialEquiv, PartialHomeomorph.prod_toPartialEquiv,
-    PartialHomeomorph.refl_localEquiv, PartialEquiv.trans_target, PartialEquiv.prod_target,
+    PartialHomeomorph.refl_partialEquiv, PartialEquiv.trans_target, PartialEquiv.prod_target,
     PartialEquiv.refl_target]
   erw [hom_trivializationAt_target]
   simp only [trivializationAt_pullBack_baseSet, TangentBundle.trivializationAt_baseSet]

SphereEversion/Global/OneJetSec.lean

@@ -51,15 +51,15 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 
 attribute [pp_dot] OneJetSec.bs OneJetSec.ϕ
 
-instance : FunLike (OneJetSec I M I' M') M fun _ ↦ OneJetBundle I M I' M' where
+instance : FunLike (OneJetSec I M I' M') M (OneJetBundle I M I' M') where
   coe := fun S x ↦ OneJetBundle.mk x (S.bs x) (S.ϕ x)
   coe_injective' := by
     intro S T h
     dsimp at h
     ext x
     simpa using (Bundle.TotalSpace.mk.inj (congrFun h x)).1
     have := heq_eq_eq _ _ ▸ (Bundle.TotalSpace.mk.inj (congrFun h x)).2
-    exact congrFun (congrArg FunLike.coe this) _
+    exact congrFun (congrArg DFunLike.coe this) _
 
 variable {I M I' M'}
 
@@ -179,7 +179,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [Top
     Smooth (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) fun p : N × M ↦
       OneJetBundle.mk p.2 (bs p.1 p.2) (ϕ p.1 p.2)
 
-instance : FunLike (FamilyOneJetSec I M I' M' J N) N fun _ ↦ OneJetSec I M I' M' where
+instance : FunLike (FamilyOneJetSec I M I' M' J N) N (OneJetSec I M I' M') where
   coe := fun S t ↦
     { bs := S.bs t
       ϕ := S.ϕ t
@@ -284,6 +284,6 @@ end FamilyOneJetSec
 def HtpyOneJetSec :=
   FamilyOneJetSec I M I' M' 𝓘(ℝ, ℝ) ℝ
 
-example : FunLike (HtpyOneJetSec I M I' M') ℝ fun _ ↦ OneJetSec I M I' M' := by infer_instance
+example : FunLike (HtpyOneJetSec I M I' M') ℝ (OneJetSec I M I' M') := by infer_instance
 
 end Real

SphereEversion/Global/Relation.lean

@@ -66,7 +66,7 @@ variable {R : RelMfld I M I' M'}
 structure FormalSol (R : RelMfld I M I' M') extends OneJetSec I M I' M' where
   is_sol' : ∀ x : M, toOneJetSec x ∈ R
 
-instance (R : RelMfld I M I' M') : FunLike (FormalSol R) M fun _ => OneJetBundle I M I' M'  where
+instance (R : RelMfld I M I' M') : FunLike (FormalSol R) M (OneJetBundle I M I' M')  where
   coe := fun F ↦ F.toOneJetSec
   coe_injective' := by
     intro F G h
@@ -150,7 +150,7 @@ end FormalSol
 
 open scoped Manifold Bundle
 
-/- Porting note: the following four statement are defeq to existing assumption but not found by TC
+/- Porting note: the following four statements are defeq to existing assumption but not found by TC
 search. There was no problem in Lean 3. -/
 
 instance (σ : OneJetBundle I M I' M') :
@@ -218,7 +218,7 @@ structure FamilyFormalSol (R : RelMfld I M I' M') extends
   FamilyOneJetSec I M I' M' J N where
   is_sol' : ∀ (t : N) (x : M), toFamilyOneJetSec t x ∈ R
 
-instance : FunLike (FamilyFormalSol J N R) N fun _ ↦ FormalSol R where
+instance : FunLike (FamilyFormalSol J N R) N (FormalSol R) where
   coe := fun S n ↦ ⟨S.toFamilyOneJetSec n, S.is_sol' n⟩
   coe_injective' := by
     intro S T

SphereEversion/Global/TwistOneJetSec.lean

@@ -89,7 +89,7 @@ structure OneJetEuclSec where
 
 variable {I M V}
 
-instance : FunLike (OneJetEuclSec I M V) M fun _  ↦ J¹[𝕜, E, I, M, V] where
+instance : DFunLike (OneJetEuclSec I M V) M fun _  ↦ J¹[𝕜, E, I, M, V] where
   coe := OneJetEuclSec.toFun
   coe_injective' := by
     intro S T h
@@ -187,7 +187,7 @@ structure FamilyOneJetEuclSec where
   is_sec' : ∀ p, (toFun p).1 = p.2
   smooth' : Smooth (J.prod I) (I.prod 𝓘(ℝ, E →L[ℝ] V)) toFun
 
-instance : FunLike (FamilyOneJetEuclSec I M V J N) (N × M) fun _  ↦ J¹[ℝ, E, I, M, V] where
+instance : FunLike (FamilyOneJetEuclSec I M V J N) (N × M) J¹[ℝ, E, I, M, V] where
   coe := FamilyOneJetEuclSec.toFun
   coe_injective' := by
     intro S T h

SphereEversion/Local/OneJet.lean

@@ -62,7 +62,7 @@ namespace JetSec
 
 variable {E F}
 
-instance : FunLike (JetSec E F) E fun _ ↦ F × (E →L[ℝ] F) where
+instance : FunLike (JetSec E F) E (F × (E →L[ℝ] F)) where
   coe 𝓕 := fun x => (𝓕.f x, 𝓕.φ x)
   coe_injective' := by
     rintro ⟨⟩ ⟨⟩ h; congr
@@ -78,7 +78,7 @@ theorem coe_apply (𝓕 : JetSec E F) (x : E) : 𝓕 x = (𝓕.f x, 𝓕.φ x) :
   rfl
 
 theorem ext' {𝓕 𝓕' : JetSec E F} (h : ∀ x, 𝓕 x = 𝓕' x) : 𝓕 = 𝓕' :=
-  FunLike.ext _ _ h
+  DFunLike.ext _ _ h
 
 /-! ## Holonomic sections-/
 
@@ -123,7 +123,7 @@ theorem IsPartHolonomicAt.sup (𝓕 : JetSec E F) {E' E'' : Submodule ℝ E} {x
 theorem isPartHolonomicAt_top {𝓕 : JetSec E F} {x : E} :
     IsPartHolonomicAt 𝓕 ⊤ x ↔ IsHolonomicAt 𝓕 x := by
   simp only [IsPartHolonomicAt, Submodule.mem_top, forall_true_left, IsHolonomicAt]
-  simp only [← funext_iff, FunLike.ext_iff]
+  simp only [← funext_iff, DFunLike.ext_iff]
 
 @[simp]
 theorem isPartHolonomicAt_bot (𝓕 : JetSec E F) : IsPartHolonomicAt 𝓕 ⊥ = fun _ => True := by
@@ -152,15 +152,15 @@ variable {E F P}
 
 namespace FamilyJetSec
 
-instance : FunLike (FamilyJetSec E F P) P fun _ => JetSec E F where
+instance : FunLike (FamilyJetSec E F P) P (JetSec E F) where
   coe S t :=
     { f := S.f t
       f_diff := S.f_diff.comp (contDiff_const.prod contDiff_id)
       φ := S.φ t
       φ_diff := S.φ_diff.comp (contDiff_const.prod contDiff_id) }
   coe_injective' := by
     rintro ⟨⟩ ⟨⟩ h
-    simp only [funext_iff, FunLike.ext_iff, JetSec.mk_apply, Prod.ext_iff] at h
+    simp only [funext_iff, DFunLike.ext_iff, JetSec.mk_apply, Prod.ext_iff] at h
     congr <;> ext <;> simp [h]
 
 @[simp] theorem mk_apply_apply (f : P → E → F) (f_diff φ φ_diff t x) :

SphereEversion/Local/Relation.lean

@@ -69,7 +69,7 @@ def _root_.JetSec.IsFormalSol.formalSol {𝓕 : JetSec E F} {R : RelLoc E F} (h
     FormalSol R :=
   { 𝓕 with is_sol := h }
 
-instance (R : RelLoc E F) : FunLike (FormalSol R) E (fun _ ↦ F × (E →L[ℝ] F)) :=
+instance (R : RelLoc E F) : FunLike (FormalSol R) E (F × (E →L[ℝ] F)) :=
   ⟨fun 𝓕 x => (𝓕.f x, 𝓕.φ x),
    by
      intros 𝓕 𝓕' h
@@ -118,7 +118,7 @@ def HtpyFormalSol.toHtpyJetSec {R : RelLoc E F} (𝓕 : R.HtpyFormalSol) : HtpyJ
 
 open RelLoc
 
-instance (R : RelLoc E F) : FunLike (FamilyFormalSol P R) P fun _ => JetSec E F :=
+instance (R : RelLoc E F) : FunLike (FamilyFormalSol P R) P (JetSec E F) :=
   ⟨fun S => S.toFamilyJetSec,
     by
       intros S S' h

SphereEversion/ToMathlib/Equivariant.lean

@@ -262,7 +262,7 @@ instance : EquivLike EquivariantEquiv ℝ ℝ where
 
 @[ext]
 theorem ext {e₁ e₂ : EquivariantEquiv} (h : ∀ x, e₁ x = e₂ x) : e₁ = e₂ :=
-  FunLike.ext e₁ e₂ h
+  DFunLike.ext e₁ e₂ h
 
 @[simp]
 theorem symm_symm (e : EquivariantEquiv) : e.symm.symm = e := by

SphereEversion/ToMathlib/Topology/LocallyFinite.lean

@@ -1,4 +1,5 @@
 import Mathlib.Algebra.SMulWithZero
+import Mathlib.GroupTheory.GroupAction.Pi
 import Mathlib.Topology.LocallyFinite
 
 open Function Set

SphereEversion/ToMathlib/Topology/Support.lean

@@ -21,15 +21,3 @@ theorem tsupport_smul_right {α : Type _} [TopologicalSpace α] {M : Type _} {R
   exact inter_subset_right _ _
 
 end
-
-section
-
-variable {ι X : Type _} [TopologicalSpace X]
-
-@[to_additive]
-theorem locallyFinite_mulSupport_iff {M : Type _} [CommMonoid M] {f : ι → X → M} :
-    (LocallyFinite fun i => mulSupport <| f i) ↔ LocallyFinite fun i => mulTSupport <| f i :=
-  ⟨LocallyFinite.closure, fun H => H.subset fun _ => subset_closure⟩
-
-end
-

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "ca91956e8d5c311e00d6a69eb93d5eb5eef9b37d",
+   "rev": "1972e073b3e6bc0776ad5b544bfa7db7fc3f7c36",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "2ae78a474ddf0a39bc2afb9f9f284d2e64f48a70",
+   "rev": "1c638703ed1c0c42aed2687acbeda67cec801454",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "ef9852fc942cc8a5812ad62d4ff0006db96b1754",
+   "rev": "e3c20cbbbbe7a771a4579587bc2326669e992ae1",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,