From 46e6944ebe520dfa3737fd684c9b21d411d84932 Mon Sep 17 00:00:00 2001 From: Winston Yin Date: Wed, 24 Jan 2024 10:06:42 +0000 Subject: [PATCH] chore: rename `StructureGroupoid.eq_on_source'` to `StructureGroupoid.mem_of_eqOnSource'` (#9802) Since it refers to `PartialEquiv.EqOnSource`, the correct naming scheme should not be snake case `eq_on_source`. I also added `mem_of_` because that's the target of the lemma, while `EqOnSource` is just a hypothesis. There are no added lemmas or docstrings in this PR. It's all just renaming. --- Mathlib/Geometry/Manifold/ChartedSpace.lean | 37 ++++++++++--------- .../Manifold/LocalInvariantProperties.lean | 2 +- .../Manifold/SmoothManifoldWithCorners.lean | 8 ++-- .../VectorBundle/FiberwiseLinear.lean | 2 +- scripts/nolints.json | 2 +- 5 files changed, 26 insertions(+), 25 deletions(-) diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean index bd7cde8528d69..caee3bc6596df 100644 --- a/Mathlib/Geometry/Manifold/ChartedSpace.lean +++ b/Mathlib/Geometry/Manifold/ChartedSpace.lean @@ -167,7 +167,7 @@ structure StructureGroupoid (H : Type u) [TopologicalSpace H] where id_mem' : PartialHomeomorph.refl H ∈ members locality' : ∀ e : PartialHomeomorph H H, (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members - eq_on_source' : ∀ e e' : PartialHomeomorph H H, e ∈ members → e' ≈ e → e' ∈ members + mem_of_eqOnSource' : ∀ e e' : PartialHomeomorph H H, e ∈ members → e' ≈ e → e' ∈ members #align structure_groupoid StructureGroupoid variable [TopologicalSpace H] @@ -198,8 +198,8 @@ instance : Inf (StructureGroupoid H) := refine And.intro hs.left (And.intro hs.right.left ?_) · exact hs.right.right.left · exact hs.right.right.right) - (eq_on_source' := fun e e' he hee' => - ⟨G.eq_on_source' e e' he.left hee', G'.eq_on_source' e e' he.right hee'⟩)⟩ + (mem_of_eqOnSource' := fun e e' he hee' => + ⟨G.mem_of_eqOnSource' e e' he.left hee', G'.mem_of_eqOnSource' e e' he.right hee'⟩)⟩ instance : InfSet (StructureGroupoid H) := ⟨fun S => StructureGroupoid.mk @@ -223,10 +223,10 @@ instance : InfSet (StructureGroupoid H) := intro x hex rcases he x hex with ⟨s, hs⟩ exact ⟨s, ⟨hs.left, ⟨hs.right.left, hs.right.right i hi⟩⟩⟩) - (eq_on_source' := by + (mem_of_eqOnSource' := by simp only [mem_iInter] intro e e' he he'e - exact fun i hi => i.eq_on_source' e e' (he i hi) he'e)⟩ + exact fun i hi => i.mem_of_eqOnSource' e e' (he i hi) he'e)⟩ theorem StructureGroupoid.trans (G : StructureGroupoid H) {e e' : PartialHomeomorph H H} (he : e ∈ G) (he' : e' ∈ G) : e ≫ₕ e' ∈ G := @@ -247,10 +247,10 @@ theorem StructureGroupoid.locality (G : StructureGroupoid H) {e : PartialHomeomo G.locality' e h #align structure_groupoid.locality StructureGroupoid.locality -theorem StructureGroupoid.eq_on_source (G : StructureGroupoid H) {e e' : PartialHomeomorph H H} +theorem StructureGroupoid.mem_of_eqOnSource (G : StructureGroupoid H) {e e' : PartialHomeomorph H H} (he : e ∈ G) (h : e' ≈ e) : e' ∈ G := - G.eq_on_source' e e' he h -#align structure_groupoid.eq_on_source StructureGroupoid.eq_on_source + G.mem_of_eqOnSource' e e' he h +#align structure_groupoid.eq_on_source StructureGroupoid.mem_of_eqOnSource /-- Partial order on the set of groupoids, given by inclusion of the members of the groupoid. -/ instance StructureGroupoid.partialOrder : PartialOrder (StructureGroupoid H) := @@ -308,7 +308,7 @@ def idGroupoid (H : Type u) [TopologicalSpace H] : StructureGroupoid H where · exfalso rw [mem_setOf_eq] at hs rwa [hs] at x's - eq_on_source' e e' he he'e := by + mem_of_eqOnSource' e e' he he'e := by cases' he with he he · left have : e = e' := by @@ -379,7 +379,7 @@ def Pregroupoid.groupoid (PG : Pregroupoid H) : StructureGroupoid H where convert hs.2 using 1 dsimp [PartialHomeomorph.restr] rw [s_open.interior_eq] - eq_on_source' e e' he ee' := by + mem_of_eqOnSource' e e' he ee' := by constructor · apply PG.congr e'.open_source ee'.2 simp only [ee'.1, he.1] @@ -405,11 +405,11 @@ theorem groupoid_of_pregroupoid_le (PG₁ PG₂ : Pregroupoid H) exact ⟨h _ _ he.1, h _ _ he.2⟩ #align groupoid_of_pregroupoid_le groupoid_of_pregroupoid_le -theorem mem_pregroupoid_of_eq_on_source (PG : Pregroupoid H) {e e' : PartialHomeomorph H H} +theorem mem_pregroupoid_of_eqOnSource (PG : Pregroupoid H) {e e' : PartialHomeomorph H H} (he' : e ≈ e') (he : PG.property e e.source) : PG.property e' e'.source := by rw [← he'.1] exact PG.congr e.open_source he'.eqOn.symm he -#align mem_pregroupoid_of_eq_on_source mem_pregroupoid_of_eq_on_source +#align mem_pregroupoid_of_eq_on_source mem_pregroupoid_of_eqOnSource /-- The pregroupoid of all partial maps on a topological space `H`. -/ @[reducible] @@ -489,7 +489,7 @@ def idRestrGroupoid : StructureGroupoid H where rw [hs.interior_eq] exact hxs simpa only [mfld_simps] using PartialHomeomorph.EqOnSource.eqOn hes' hes - eq_on_source' := by + mem_of_eqOnSource' := by rintro e e' ⟨s, hs, hse⟩ hee' exact ⟨s, hs, Setoid.trans hee' hse⟩ #align id_restr_groupoid idRestrGroupoid @@ -515,7 +515,7 @@ theorem closedUnderRestriction_iff_id_le (G : StructureGroupoid H) : · intro _i apply StructureGroupoid.le_iff.mpr rintro e ⟨s, hs, hes⟩ - refine' G.eq_on_source _ hes + refine' G.mem_of_eqOnSource _ hes convert closedUnderRestriction' G.id_mem hs -- Porting note: was -- change s = _ ∩ _ @@ -1041,7 +1041,7 @@ theorem StructureGroupoid.compatible_of_mem_maximalAtlas {e e' : PartialHomeomor _ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e' := by rw [trans_assoc] _ ≈ e.symm.restr s ≫ₕ e' := by rw [trans_of_set']; apply refl _ ≈ (e.symm ≫ₕ e').restr s := by rw [restr_trans] - exact G.eq_on_source C (Setoid.symm D) + exact G.mem_of_eqOnSource C (Setoid.symm D) #align structure_groupoid.compatible_of_mem_maximal_atlas StructureGroupoid.compatible_of_mem_maximalAtlas variable (G) @@ -1105,7 +1105,7 @@ theorem singleton_hasGroupoid (h : e.source = Set.univ) (G : StructureGroupoid H intro e' e'' he' he'' rw [e.singletonChartedSpace_mem_atlas_eq h e' he', e.singletonChartedSpace_mem_atlas_eq h e'' he''] - refine' G.eq_on_source _ e.symm_trans_self + refine' G.mem_of_eqOnSource _ e.symm_trans_self have hle : idRestrGroupoid ≤ G := (closedUnderRestriction_iff_id_le G).mp (by assumption) exact StructureGroupoid.le_iff.mp hle _ (idRestrGroupoid_mem _) } #align local_homeomorph.singleton_has_groupoid PartialHomeomorph.singleton_hasGroupoid @@ -1163,7 +1163,8 @@ protected instance instHasGroupoid [ClosedUnderRestriction G] : HasGroupoid s G rw [hc.symm, mem_singleton_iff] at he rw [hc'.symm, mem_singleton_iff] at he' rw [he, he'] - refine' G.eq_on_source _ (subtypeRestr_symm_trans_subtypeRestr s (chartAt H x) (chartAt H x')) + refine' G.mem_of_eqOnSource _ + (subtypeRestr_symm_trans_subtypeRestr s (chartAt H x) (chartAt H x')) apply closedUnderRestriction' · exact G.compatible (chart_mem_atlas _ _) (chart_mem_atlas _ _) · exact isOpen_inter_preimage_symm (chartAt _ _) s.2 @@ -1277,7 +1278,7 @@ def Structomorph.trans (e : Structomorph G M M') (e' : Structomorph G M' M'') : _ ≈ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr s := by simp only [EqOnSource.restr, trans_assoc, _root_.refl] _ ≈ F₂ := by simp only [feq, _root_.refl] - have : F₂ ∈ G := G.eq_on_source A (Setoid.symm this) + have : F₂ ∈ G := G.mem_of_eqOnSource A (Setoid.symm this) exact this } #align structomorph.trans Structomorph.trans diff --git a/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean b/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean index fa9d37d3ceb3f..c14a92da4d404 100644 --- a/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean +++ b/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean @@ -709,7 +709,7 @@ theorem HasGroupoid.comp (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').open_source refine' ⟨_, hs.inter φ.open_source, _, _⟩ · simp only [hx, hφ_dom, mfld_simps] - · refine' G₁.eq_on_source (closedUnderRestriction' hφG₁ hs) _ + · refine' G₁.mem_of_eqOnSource (closedUnderRestriction' hφG₁ hs) _ rw [PartialHomeomorph.restr_source_inter] refine' PartialHomeomorph.Set.EqOn.restr_eqOn_source (hφ.mono _) mfld_set_tac } diff --git a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean index 8960721caf5bb..b5a692212bd60 100644 --- a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean +++ b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean @@ -620,7 +620,7 @@ theorem symm_trans_mem_contDiffGroupoid (e : PartialHomeomorph M H) : e.symm.trans e ∈ contDiffGroupoid n I := haveI : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target := PartialHomeomorph.symm_trans_self _ - StructureGroupoid.eq_on_source _ (ofSet_mem_contDiffGroupoid n I e.open_target) this + StructureGroupoid.mem_of_eqOnSource _ (ofSet_mem_contDiffGroupoid n I e.open_target) this #align symm_trans_mem_cont_diff_groupoid symm_trans_mem_contDiffGroupoid variable {E' H' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] @@ -650,7 +650,7 @@ instance : ClosedUnderRestriction (contDiffGroupoid n I) := (by apply StructureGroupoid.le_iff.mpr rintro e ⟨s, hs, hes⟩ - apply (contDiffGroupoid n I).eq_on_source' _ _ _ hes + apply (contDiffGroupoid n I).mem_of_eqOnSource' _ _ _ hes exact ofSet_mem_contDiffGroupoid n I hs) end contDiffGroupoid @@ -780,7 +780,7 @@ theorem symm_trans_mem_analyticGroupoid (e : PartialHomeomorph M H) : e.symm.trans e ∈ analyticGroupoid I := haveI : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target := PartialHomeomorph.symm_trans_self _ - StructureGroupoid.eq_on_source _ (ofSet_mem_analyticGroupoid I e.open_target) this + StructureGroupoid.mem_of_eqOnSource _ (ofSet_mem_analyticGroupoid I e.open_target) this /-- The analytic groupoid is closed under restriction. -/ instance : ClosedUnderRestriction (analyticGroupoid I) := @@ -788,7 +788,7 @@ instance : ClosedUnderRestriction (analyticGroupoid I) := (by apply StructureGroupoid.le_iff.mpr rintro e ⟨s, hs, hes⟩ - apply (analyticGroupoid I).eq_on_source' _ _ _ hes + apply (analyticGroupoid I).mem_of_eqOnSource' _ _ _ hes exact ofSet_mem_analyticGroupoid I hs) /-- The analytic groupoid on a boundaryless charted space modeled on a complete vector space diff --git a/Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean b/Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean index be5a9ba48a19f..634312ae9f13f 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean @@ -288,7 +288,7 @@ def smoothFiberwiseLinear : StructureGroupoid (B × F) where intro e he obtain ⟨U, hU, h⟩ := SmoothFiberwiseLinear.locality_aux₁ e he exact SmoothFiberwiseLinear.locality_aux₂ e U hU h - eq_on_source' := by + mem_of_eqOnSource' := by simp only [mem_aux] rintro e e' ⟨φ, U, hU, hφ, h2φ, heφ⟩ hee' exact ⟨φ, U, hU, hφ, h2φ, Setoid.trans hee' heφ⟩ diff --git a/scripts/nolints.json b/scripts/nolints.json index 92166b58b3731..5b4bc92b5ff7a 100644 --- a/scripts/nolints.json +++ b/scripts/nolints.json @@ -1191,4 +1191,4 @@ ["docBlame", "Mathlib.Meta.NormNum.evalMul.core.intArm"], ["docBlame", "Mathlib.Meta.NormNum.evalMul.core.ratArm"], ["unusedArguments", "Combinator.K"], - ["unusedArguments", "Decidable.not_or_iff_and_not"]] \ No newline at end of file + ["unusedArguments", "Decidable.not_or_iff_and_not"]]