From 0cf005e48ca1b0ae19aaf9d94335c4e30520ab4f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 20 Jan 2024 21:19:37 +0100 Subject: [PATCH] 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 | 6 +++--- SphereEversion/Global/OneJetSec.lean | 8 ++++---- SphereEversion/Global/Relation.lean | 6 +++--- SphereEversion/Global/TwistOneJetSec.lean | 4 ++-- SphereEversion/Local/OneJet.lean | 10 +++++----- SphereEversion/Local/Relation.lean | 4 ++-- SphereEversion/ToMathlib/Equivariant.lean | 2 +- SphereEversion/ToMathlib/Topology/LocallyFinite.lean | 1 + SphereEversion/ToMathlib/Topology/Support.lean | 12 ------------ lake-manifest.json | 6 +++--- 10 files changed, 24 insertions(+), 35 deletions(-) diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index 7fe259b8..05858def 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/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] diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index e6dcee98..576f2d9c 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -51,7 +51,7 @@ 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 @@ -59,7 +59,7 @@ instance : FunLike (OneJetSec I M I' M') M fun _ ↦ OneJetBundle I M I' M' wher 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 diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index 60b4b3a9..28e88660 100644 --- a/SphereEversion/Global/Relation.lean +++ b/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 diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean index 0375a568..a5699195 100644 --- a/SphereEversion/Global/TwistOneJetSec.lean +++ b/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 diff --git a/SphereEversion/Local/OneJet.lean b/SphereEversion/Local/OneJet.lean index 1c328bbc..6abc3bf8 100644 --- a/SphereEversion/Local/OneJet.lean +++ b/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,7 +152,7 @@ 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) @@ -160,7 +160,7 @@ instance : FunLike (FamilyJetSec E F P) P fun _ => JetSec E F where φ_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) : diff --git a/SphereEversion/Local/Relation.lean b/SphereEversion/Local/Relation.lean index 4b543e62..b7ceece1 100644 --- a/SphereEversion/Local/Relation.lean +++ b/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 diff --git a/SphereEversion/ToMathlib/Equivariant.lean b/SphereEversion/ToMathlib/Equivariant.lean index e7f13375..b1cccd32 100644 --- a/SphereEversion/ToMathlib/Equivariant.lean +++ b/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 diff --git a/SphereEversion/ToMathlib/Topology/LocallyFinite.lean b/SphereEversion/ToMathlib/Topology/LocallyFinite.lean index 93461b9b..340bb373 100644 --- a/SphereEversion/ToMathlib/Topology/LocallyFinite.lean +++ b/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 diff --git a/SphereEversion/ToMathlib/Topology/Support.lean b/SphereEversion/ToMathlib/Topology/Support.lean index f85cd716..809357d3 100644 --- a/SphereEversion/ToMathlib/Topology/Support.lean +++ b/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 - diff --git a/lake-manifest.json b/lake-manifest.json index 65992e85..11748ecc 100644 --- a/lake-manifest.json +++ b/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,