From b593cd2f2f6839893243d8a49d07f8fab6f8988a Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 11 Feb 2024 11:41:50 -0800 Subject: [PATCH 1/3] =?UTF-8?q?refactor:=20prefer=20`s=20=E2=88=A9=20.`=20?= =?UTF-8?q?when=20passing=20to=20a=20subset=20of=20`s`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This is partial work to make `Subtype.val '' .` and `s ∩ .` be consistently used as adjoint operators for passing to and from a "subspace". --- .../InnerProductSpace/Projection.lean | 2 +- Mathlib/Data/Set/Image.lean | 27 ++++++++++-------- Mathlib/Data/Set/Intervals/Image.lean | 28 +++++++++---------- Mathlib/Geometry/Manifold/IntegralCurve.lean | 2 +- Mathlib/GroupTheory/Subgroup/Basic.lean | 2 +- .../MeasureTheory/Constructions/Polish.lean | 2 +- .../MeasureTheory/MeasurableSpace/Basic.lean | 2 +- .../MeasureTheory/Measure/AEMeasurable.lean | 1 + .../MeasureTheory/Measure/OuterMeasure.lean | 6 ++-- Mathlib/MeasureTheory/Measure/Restrict.lean | 2 +- .../GradedAlgebra/HomogeneousIdeal.lean | 4 ++- Mathlib/Topology/Connected/Basic.lean | 4 +-- Mathlib/Topology/Constructions.lean | 4 +-- Mathlib/Topology/ContinuousOn.lean | 6 ++-- Mathlib/Topology/Separation.lean | 4 +-- Mathlib/Topology/Sober.lean | 2 +- 16 files changed, 53 insertions(+), 45 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index c5193ad34a7ae..76b450b989f9b 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -1444,7 +1444,7 @@ theorem maximal_orthonormal_iff_orthogonalComplement_eq_bot (hv : Orthonormal obtain ⟨l, hl, rfl⟩ : ∃ l ∈ Finsupp.supported 𝕜 𝕜 ((↑) ⁻¹' v : Set u), (Finsupp.total (↥u) E 𝕜 (↑)) l = y := by rw [← Finsupp.mem_span_image_iff_total] - simp [huv, inter_eq_self_of_subset_left, hy] + simp [huv, inter_eq_self_of_subset_right, hy] exact hu.inner_finsupp_eq_zero hxv' hl #align maximal_orthonormal_iff_orthogonal_complement_eq_bot maximal_orthonormal_iff_orthogonalComplement_eq_bot diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean index 30b9e3c7da44a..cf75f0e482bf3 100644 --- a/Mathlib/Data/Set/Image.lean +++ b/Mathlib/Data/Set/Image.lean @@ -766,14 +766,17 @@ theorem insert_image_compl_eq_range (f : α → β) (x : α) : insert (f x) (f ' rw [← image_insert_eq, insert_eq, union_compl_self, image_univ] #align set.insert_image_compl_eq_range Set.insert_image_compl_eq_range -theorem image_preimage_eq_inter_range {f : α → β} {t : Set β} : f '' (f ⁻¹' t) = t ∩ range f := +theorem image_preimage_eq_range_inter {f : α → β} {t : Set β} : f '' (f ⁻¹' t) = range f ∩ t := ext fun x => - ⟨fun ⟨x, hx, HEq⟩ => HEq ▸ ⟨hx, mem_range_self _⟩, fun ⟨hx, ⟨y, h_eq⟩⟩ => + ⟨fun ⟨x, hx, HEq⟩ => HEq ▸ ⟨mem_range_self _, hx⟩, fun ⟨⟨y, h_eq⟩, hx⟩ => h_eq ▸ mem_image_of_mem f <| show y ∈ f ⁻¹' t by rw [preimage, mem_setOf, h_eq]; exact hx⟩ + +theorem image_preimage_eq_inter_range {f : α → β} {t : Set β} : f '' (f ⁻¹' t) = t ∩ range f := by + rw [image_preimage_eq_range_inter, inter_comm] #align set.image_preimage_eq_inter_range Set.image_preimage_eq_inter_range theorem image_preimage_eq_of_subset {f : α → β} {s : Set β} (hs : s ⊆ range f) : - f '' (f ⁻¹' s) = s := by rw [image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs] + f '' (f ⁻¹' s) = s := by rw [image_preimage_eq_range_inter, inter_eq_self_of_subset_right hs] #align set.image_preimage_eq_of_subset Set.image_preimage_eq_of_subset theorem image_preimage_eq_iff {f : α → β} {s : Set β} : f '' (f ⁻¹' s) = s ↔ s ⊆ range f := @@ -838,7 +841,7 @@ theorem preimage_range_inter {f : α → β} {s : Set β} : f ⁻¹' (range f #align set.preimage_range_inter Set.preimage_range_inter theorem preimage_image_preimage {f : α → β} {s : Set β} : f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s := by - rw [image_preimage_eq_inter_range, preimage_inter_range] + rw [image_preimage_eq_range_inter, preimage_range_inter] #align set.preimage_image_preimage Set.preimage_image_preimage @[simp, mfld_simps] @@ -1398,28 +1401,28 @@ theorem coe_image_univ (s : Set α) : ((↑) : s → α) '' Set.univ = s := #align subtype.coe_image_univ Subtype.coe_image_univ @[simp] -theorem image_preimage_coe (s t : Set α) : ((↑) : s → α) '' (((↑) : s → α) ⁻¹' t) = t ∩ s := - image_preimage_eq_inter_range.trans <| congr_arg _ range_coe +theorem image_preimage_coe (s t : Set α) : ((↑) : s → α) '' (((↑) : s → α) ⁻¹' t) = s ∩ t := + image_preimage_eq_range_inter.trans <| congr_arg (· ∩ t) range_coe #align subtype.image_preimage_coe Subtype.image_preimage_coe -theorem image_preimage_val (s t : Set α) : (Subtype.val : s → α) '' (Subtype.val ⁻¹' t) = t ∩ s := +theorem image_preimage_val (s t : Set α) : (Subtype.val : s → α) '' (Subtype.val ⁻¹' t) = s ∩ t := image_preimage_coe s t #align subtype.image_preimage_val Subtype.image_preimage_val theorem preimage_coe_eq_preimage_coe_iff {s t u : Set α} : - ((↑) : s → α) ⁻¹' t = ((↑) : s → α) ⁻¹' u ↔ t ∩ s = u ∩ s := by + ((↑) : s → α) ⁻¹' t = ((↑) : s → α) ⁻¹' u ↔ s ∩ t = s ∩ u := by rw [← image_preimage_coe, ← image_preimage_coe, coe_injective.image_injective.eq_iff] #align subtype.preimage_coe_eq_preimage_coe_iff Subtype.preimage_coe_eq_preimage_coe_iff -- Porting note: -- @[simp] `simp` can prove this theorem preimage_coe_inter_self (s t : Set α) : - ((↑) : s → α) ⁻¹' (t ∩ s) = ((↑) : s → α) ⁻¹' t := by - rw [preimage_coe_eq_preimage_coe_iff, inter_assoc, inter_self] + ((↑) : s → α) ⁻¹' (s ∩ t) = ((↑) : s → α) ⁻¹' t := by + rw [preimage_coe_eq_preimage_coe_iff, ← inter_assoc, inter_self] #align subtype.preimage_coe_inter_self Subtype.preimage_coe_inter_self theorem preimage_val_eq_preimage_val_iff (s t u : Set α) : - (Subtype.val : s → α) ⁻¹' t = Subtype.val ⁻¹' u ↔ t ∩ s = u ∩ s := + (Subtype.val : s → α) ⁻¹' t = Subtype.val ⁻¹' u ↔ s ∩ t = s ∩ u := preimage_coe_eq_preimage_coe_iff #align subtype.preimage_val_eq_preimage_val_iff Subtype.preimage_val_eq_preimage_val_iff @@ -1434,7 +1437,7 @@ theorem forall_set_subtype {t : Set α} (p : Set α → Prop) : theorem preimage_coe_nonempty {s t : Set α} : (((↑) : s → α) ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty := by - rw [inter_comm, ← image_preimage_coe, image_nonempty] + rw [← image_preimage_coe, image_nonempty] #align subtype.preimage_coe_nonempty Subtype.preimage_coe_nonempty theorem preimage_coe_eq_empty {s t : Set α} : ((↑) : s → α) ⁻¹' t = ∅ ↔ s ∩ t = ∅ := by diff --git a/Mathlib/Data/Set/Intervals/Image.lean b/Mathlib/Data/Set/Intervals/Image.lean index 6c97bec00b4d0..b30a5b7c9bf82 100644 --- a/Mathlib/Data/Set/Intervals/Image.lean +++ b/Mathlib/Data/Set/Intervals/Image.lean @@ -289,27 +289,27 @@ theorem image_subtype_val_Ioi_subset (a : {x // p x}) : @[simp] lemma image_subtype_val_Ici_Iic {a : α} (b : Ici a) : Subtype.val '' Iic b = Icc a b := - (Subtype.image_preimage_val (Ici a) (Iic b.1)).trans Iic_inter_Ici + (Subtype.image_preimage_val (Ici a) (Iic b.1)).trans Ici_inter_Iic @[simp] lemma image_subtype_val_Ici_Iio {a : α} (b : Ici a) : Subtype.val '' Iio b = Ico a b := - (Subtype.image_preimage_val (Ici a) (Iio b.1)).trans Iio_inter_Ici + (Subtype.image_preimage_val (Ici a) (Iio b.1)).trans Ici_inter_Iio @[simp] lemma image_subtype_val_Ici_Ici {a : α} (b : Ici a) : Subtype.val '' Ici b = Ici b.1 := - (Subtype.image_preimage_val (Ici a) (Ici b.1)).trans <| inter_eq_left.2 <| Ici_subset_Ici.2 b.2 + (Subtype.image_preimage_val (Ici a) (Ici b.1)).trans <| inter_eq_right.2 <| Ici_subset_Ici.2 b.2 @[simp] lemma image_subtype_val_Ici_Ioi {a : α} (b : Ici a) : Subtype.val '' Ioi b = Ioi b.1 := - (Subtype.image_preimage_val (Ici a) (Ioi b.1)).trans <| inter_eq_left.2 <| Ioi_subset_Ici b.2 + (Subtype.image_preimage_val (Ici a) (Ioi b.1)).trans <| inter_eq_right.2 <| Ioi_subset_Ici b.2 @[simp] lemma image_subtype_val_Iic_Ici {a : α} (b : Iic a) : Subtype.val '' Ici b = Icc b.1 a := - Subtype.image_preimage_val (Iic a) (Ici b.1) + (Subtype.image_preimage_val _ _).trans <| inter_comm _ _ @[simp] lemma image_subtype_val_Iic_Ioi {a : α} (b : Iic a) : Subtype.val '' Ioi b = Ioc b.1 a := - Subtype.image_preimage_val (Iic a) (Ioi b.1) + (Subtype.image_preimage_val _ _).trans <| inter_comm _ _ @[simp] lemma image_subtype_val_Iic_Iic {a : α} (b : Iic a) : Subtype.val '' Iic b = Iic b.1 := @@ -321,23 +321,23 @@ lemma image_subtype_val_Iic_Iio {a : α} (b : Iic a) : Subtype.val '' Iio b = Ii @[simp] lemma image_subtype_val_Ioi_Ici {a : α} (b : Ioi a) : Subtype.val '' Ici b = Ici b.1 := - (Subtype.image_preimage_val (Ioi a) (Ici b.1)).trans <| inter_eq_left.2 <| Ici_subset_Ioi.2 b.2 + (Subtype.image_preimage_val (Ioi a) (Ici b.1)).trans <| inter_eq_right.2 <| Ici_subset_Ioi.2 b.2 @[simp] lemma image_subtype_val_Ioi_Iic {a : α} (b : Ioi a) : Subtype.val '' Iic b = Ioc a b := - (Subtype.image_preimage_val (Ioi a) (Iic b.1)).trans Iic_inter_Ioi + (Subtype.image_preimage_val (Ioi a) (Iic b.1)).trans Ioi_inter_Iic @[simp] lemma image_subtype_val_Ioi_Ioi {a : α} (b : Ioi a) : Subtype.val '' Ioi b = Ioi b.1 := - (Subtype.image_preimage_val (Ioi a) (Ioi b.1)).trans <| inter_eq_left.2 <| Ioi_subset_Ioi b.2.le + (Subtype.image_preimage_val (Ioi a) (Ioi b.1)).trans <| inter_eq_right.2 <| Ioi_subset_Ioi b.2.le @[simp] lemma image_subtype_val_Ioi_Iio {a : α} (b : Ioi a) : Subtype.val '' Iio b = Ioo a b := - (Subtype.image_preimage_val (Ioi a) (Iio b.1)).trans Iio_inter_Ioi + (Subtype.image_preimage_val (Ioi a) (Iio b.1)).trans Ioi_inter_Iio @[simp] lemma image_subtype_val_Iio_Ici {a : α} (b : Iio a) : Subtype.val '' Ici b = Ico b.1 a := - Subtype.image_preimage_val (Iio a) (Ici b.1) + (Subtype.image_preimage_val _ _).trans <| inter_comm _ _ @[simp] lemma image_subtype_val_Iio_Iic {a : α} (b : Iio a) : Subtype.val '' Iic b = Iic b.1 := @@ -345,7 +345,7 @@ lemma image_subtype_val_Iio_Iic {a : α} (b : Iio a) : Subtype.val '' Iic b = Ii @[simp] lemma image_subtype_val_Iio_Ioi {a : α} (b : Iio a) : Subtype.val '' Ioi b = Ioo b.1 a := - Subtype.image_preimage_val (Iio a) (Ioi b.1) + (Subtype.image_preimage_val _ _).trans <| inter_comm _ _ @[simp] lemma image_subtype_val_Iio_Iio {a : α} (b : Iio a) : Subtype.val '' Iio b = Iio b.1 := @@ -355,13 +355,13 @@ private lemma image_subtype_val_Ixx_Ixi {p q r : α → α → Prop} {a b : α} (h : ∀ {x}, r c x → p a x) : Subtype.val '' {y : {x // p a x ∧ q x b} | r c.1 y.1} = {y : α | r c.1 y ∧ q y b} := (Subtype.image_preimage_val {x | p a x ∧ q x b} {y | r c.1 y}).trans <| by - ext; simp (config := { contextual := true }) [h] + ext; simp (config := { contextual := true }) [@and_comm (r _ _), h] private lemma image_subtype_val_Ixx_Iix {p q r : α → α → Prop} {a b : α} (c : {x // p a x ∧ q x b}) (h : ∀ {x}, r x c → q x b) : Subtype.val '' {y : {x // p a x ∧ q x b} | r y.1 c.1} = {y : α | p a y ∧ r y c.1} := (Subtype.image_preimage_val {x | p a x ∧ q x b} {y | r y c.1}).trans <| by - ext; simp (config := { contextual := true }) [@and_comm (p _ _), h] + ext; simp (config := { contextual := true}) [h] @[simp] lemma image_subtype_val_Icc_Ici {a b : α} (c : Icc a b) : Subtype.val '' Ici c = Icc c.1 b := diff --git a/Mathlib/Geometry/Manifold/IntegralCurve.lean b/Mathlib/Geometry/Manifold/IntegralCurve.lean index e37dfabdaf9ff..5fc9745b67c42 100644 --- a/Mathlib/Geometry/Manifold/IntegralCurve.lean +++ b/Mathlib/Geometry/Manifold/IntegralCurve.lean @@ -444,7 +444,7 @@ theorem isIntegralCurveOn_Ioo_eqOn_of_contMDiff (ht₀ : t₀ ∈ Ioo a b) ⟨t₀, ⟨ht₀, ⟨h, ht₀⟩⟩⟩ · -- is this really the most convenient way to pass to subtype topology? -- TODO: shorten this when better API around subtype topology exists - rw [hs, ← Subtype.image_preimage_val, ← Subtype.image_preimage_val, + rw [hs, inter_comm, ← Subtype.image_preimage_val, inter_comm, ← Subtype.image_preimage_val, image_subset_image_iff Subtype.val_injective, preimage_setOf_eq] intros t ht rw [mem_preimage, ← closure_subtype] at ht diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean index 3c57459235d4e..a637e1974625a 100644 --- a/Mathlib/GroupTheory/Subgroup/Basic.lean +++ b/Mathlib/GroupTheory/Subgroup/Basic.lean @@ -1679,7 +1679,7 @@ theorem mem_subgroupOf {H K : Subgroup G} {h : K} : h ∈ H.subgroupOf K ↔ (h @[to_additive (attr := simp)] theorem subgroupOf_map_subtype (H K : Subgroup G) : (H.subgroupOf K).map K.subtype = H ⊓ K := - SetLike.ext' <| Subtype.image_preimage_coe _ _ + SetLike.ext' <| by refine Subtype.image_preimage_coe _ _ |>.trans ?_; apply Set.inter_comm #align subgroup.subgroup_of_map_subtype Subgroup.subgroupOf_map_subtype #align add_subgroup.add_subgroup_of_map_subtype AddSubgroup.addSubgroupOf_map_subtype diff --git a/Mathlib/MeasureTheory/Constructions/Polish.lean b/Mathlib/MeasureTheory/Constructions/Polish.lean index ef4908a785719..97ccc10b70f3b 100644 --- a/Mathlib/MeasureTheory/Constructions/Polish.lean +++ b/Mathlib/MeasureTheory/Constructions/Polish.lean @@ -589,7 +589,7 @@ if and only if the intesection with `Set.range f` is measurable. -/ theorem measurableSet_preimage_iff_inter_range {f : X → Y} [SecondCountableTopology (range f)] (hf : Measurable f) (hr : MeasurableSet (range f)) {s : Set Y} : MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f) := by - rw [hf.measurableSet_preimage_iff_preimage_val, + rw [hf.measurableSet_preimage_iff_preimage_val, inter_comm, ← (MeasurableEmbedding.subtype_coe hr).measurableSet_image, Subtype.image_preimage_coe] #align measurable.measurable_set_preimage_iff_inter_range Measurable.measurableSet_preimage_iff_inter_range diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean index e9dc7f409ced9..9c60d666fec3b 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean @@ -612,7 +612,7 @@ theorem MeasurableSet.subtype_image {s : Set α} {t : Set s} (hs : MeasurableSet MeasurableSet t → MeasurableSet (((↑) : s → α) '' t) := by rintro ⟨u, hu, rfl⟩ rw [Subtype.image_preimage_coe] - exact hu.inter hs + exact hs.inter hu #align measurable_set.subtype_image MeasurableSet.subtype_image @[measurability] diff --git a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean index 0cebd49896375..7ee2fdd8c4700 100644 --- a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean +++ b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean @@ -412,6 +412,7 @@ lemma MeasureTheory.NullMeasurable.aemeasurable {f : α → β} refine measurable_generateFrom fun s hs ↦ .of_subtype_image ?_ rw [preimage_comp, Subtype.image_preimage_coe] convert (hTm s hs).diff hvm using 1 + rw [inter_comm] refine Set.ext fun x ↦ and_congr_left fun hxv ↦ ⟨fun hx ↦ ?_, fun hx ↦ hTf s hs hx⟩ exact by_contra fun hx' ↦ hxv <| mem_biUnion hs ⟨hUf s hs hx, hx'⟩ diff --git a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean index c034f0e8a0583..e7fbe81167fa3 100644 --- a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean @@ -551,9 +551,10 @@ def restrict (s : Set α) : OuterMeasure α →ₗ[ℝ≥0∞] OuterMeasure α : (map (↑)).comp (comap ((↑) : s → α)) #align measure_theory.outer_measure.restrict MeasureTheory.OuterMeasure.restrict +-- TODO (kmill): change `m (t ∩ s)` to `m (s ∩ t)` @[simp] theorem restrict_apply (s t : Set α) (m : OuterMeasure α) : restrict s m t = m (t ∩ s) := by - simp [restrict] + simp [restrict, inter_comm t] #align measure_theory.outer_measure.restrict_apply MeasureTheory.OuterMeasure.restrict_apply @[mono] @@ -796,11 +797,12 @@ theorem map_ofFunction {β} {f : α → β} (hf : Injective f) : simp [hf.preimage_image] #align measure_theory.outer_measure.map_of_function MeasureTheory.OuterMeasure.map_ofFunction +-- TODO (kmill): change `m (t ∩ s)` to `m (s ∩ t)` theorem restrict_ofFunction (s : Set α) (hm : Monotone m) : restrict s (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun t => m (t ∩ s)) (by simp; simp [m_empty]) := by rw [restrict] - simp only [LinearMap.comp_apply] + simp only [inter_comm _ s, LinearMap.comp_apply] rw [comap_ofFunction _ (Or.inl hm)] simp only [map_ofFunction Subtype.coe_injective, Subtype.image_preimage_coe] #align measure_theory.outer_measure.restrict_of_function MeasureTheory.OuterMeasure.restrict_ofFunction diff --git a/Mathlib/MeasureTheory/Measure/Restrict.lean b/Mathlib/MeasureTheory/Measure/Restrict.lean index 8a5b7cc6fad59..44f5a10874458 100644 --- a/Mathlib/MeasureTheory/Measure/Restrict.lean +++ b/Mathlib/MeasureTheory/Measure/Restrict.lean @@ -810,7 +810,7 @@ theorem MeasurableSet.nullMeasurableSet_subtype_coe {t : Set s} (hs : NullMeasur { t : Set s | ∃ s' : Set α, MeasurableSet s' ∧ (↑) ⁻¹' s' = t } _ _ _ _ ht · rintro t' ⟨s', hs', rfl⟩ rw [Subtype.image_preimage_coe] - exact hs'.nullMeasurableSet.inter hs + exact hs.inter (hs'.nullMeasurableSet) · simp only [image_empty, nullMeasurableSet_empty] · intro t' simp only [← range_diff_image Subtype.coe_injective, Subtype.range_coe_subtype, setOf_mem_eq] diff --git a/Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean b/Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean index d93bb4da58870..1406c8e2f137a 100644 --- a/Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean +++ b/Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean @@ -182,7 +182,9 @@ theorem Ideal.homogeneous_span (s : Set A) (h : ∀ x ∈ s, Homogeneous 𝒜 x) is the largest homogeneous ideal of `A` contained in `I`. -/ def Ideal.homogeneousCore : HomogeneousIdeal 𝒜 := ⟨Ideal.homogeneousCore' 𝒜 I, - Ideal.homogeneous_span _ _ fun _ h => (Subtype.image_preimage_coe _ _ ▸ h).2⟩ + Ideal.homogeneous_span _ _ fun _ h => by + have := Subtype.image_preimage_coe (setOf (Homogeneous 𝒜)) (I : Set A) + exact (cast congr(_ ∈ $this) h).1⟩ #align ideal.homogeneous_core Ideal.homogeneousCore theorem Ideal.homogeneousCore_mono : Monotone (Ideal.homogeneousCore 𝒜) := diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index f7be221644597..3a4e27f1d3d8a 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -640,14 +640,14 @@ theorem IsPreconnected.subset_connectedComponentIn {x : α} {F : Set α} (hs : I (hxs : x ∈ s) (hsF : s ⊆ F) : s ⊆ connectedComponentIn F x := by have : IsPreconnected (((↑) : F → α) ⁻¹' s) := by refine' inducing_subtype_val.isPreconnected_image.mp _ - rwa [Subtype.image_preimage_coe, inter_eq_left.mpr hsF] + rwa [Subtype.image_preimage_coe, inter_eq_right.mpr hsF] have h2xs : (⟨x, hsF hxs⟩ : F) ∈ (↑) ⁻¹' s := by rw [mem_preimage] exact hxs have := this.subset_connectedComponent h2xs rw [connectedComponentIn_eq_image (hsF hxs)] refine' Subset.trans _ (image_subset _ this) - rw [Subtype.image_preimage_coe, inter_eq_left.mpr hsF] + rw [Subtype.image_preimage_coe, inter_eq_right.mpr hsF] #align is_preconnected.subset_connected_component_in IsPreconnected.subset_connectedComponentIn theorem IsConnected.subset_connectedComponent {x : α} {s : Set α} (H1 : IsConnected s) diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index c1f3086b73e8a..93db5ed4eaf34 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/Mathlib/Topology/Constructions.lean @@ -1706,12 +1706,12 @@ variable [TopologicalSpace X] {s : Set X} {t : Set s} theorem IsOpen.trans (ht : IsOpen t) (hs : IsOpen s) : IsOpen (t : Set X) := by rcases isOpen_induced_iff.mp ht with ⟨s', hs', rfl⟩ rw [Subtype.image_preimage_coe] - exact hs'.inter hs + exact hs.inter hs' theorem IsClosed.trans (ht : IsClosed t) (hs : IsClosed s) : IsClosed (t : Set X) := by rcases isClosed_induced_iff.mp ht with ⟨s', hs', rfl⟩ rw [Subtype.image_preimage_coe] - convert hs'.inter hs + exact hs.inter hs' end Monad diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean index fc1ada06af943..35608c7e7ba53 100644 --- a/Mathlib/Topology/ContinuousOn.lean +++ b/Mathlib/Topology/ContinuousOn.lean @@ -669,7 +669,7 @@ theorem continuousOn_iff' {f : α → β} {s : Set α} : simp only [Subtype.preimage_coe_eq_preimage_coe_iff] constructor <;> · rintro ⟨u, ou, useq⟩ - exact ⟨u, ou, useq.symm⟩ + exact ⟨u, ou, by simpa only [Set.inter_comm, eq_comm] using useq⟩ rw [continuousOn_iff_continuous_restrict, continuous_def]; simp only [this] #align continuous_on_iff' continuousOn_iff' @@ -694,7 +694,7 @@ theorem continuousOn_iff_isClosed {f : α → β} {s : Set α} : have : ∀ t, IsClosed (s.restrict f ⁻¹' t) ↔ ∃ u : Set α, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s := by intro t rw [isClosed_induced_iff, Set.restrict_eq, Set.preimage_comp] - simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm] + simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm, Set.inter_comm s] rw [continuousOn_iff_continuous_restrict, continuous_iff_isClosed]; simp only [this] #align continuous_on_iff_is_closed continuousOn_iff_isClosed @@ -1325,7 +1325,7 @@ theorem continuousOn_piecewise_ite {s s' t : Set α} {f f' : α → β} [∀ x, theorem frontier_inter_open_inter {s t : Set α} (ht : IsOpen t) : frontier (s ∩ t) ∩ t = frontier s ∩ t := by - simp only [← Subtype.preimage_coe_eq_preimage_coe_iff, + simp only [Set.inter_comm _ t, ← Subtype.preimage_coe_eq_preimage_coe_iff, ht.isOpenMap_subtype_val.preimage_frontier_eq_frontier_preimage continuous_subtype_val, Subtype.preimage_coe_inter_self] #align frontier_inter_open_inter frontier_inter_open_inter diff --git a/Mathlib/Topology/Separation.lean b/Mathlib/Topology/Separation.lean index a70718f0a6e9c..8b35dd91ad526 100644 --- a/Mathlib/Topology/Separation.lean +++ b/Mathlib/Topology/Separation.lean @@ -2376,12 +2376,12 @@ theorem loc_compact_Haus_tot_disc_of_zero_dim [TotallyDisconnectedSpace H] : refine' ⟨f0, _⟩ · have : Set.range ((↑) : u → H) = interior s := by rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe] - apply Set.inter_eq_self_of_subset_left interior_subset + apply Set.inter_eq_self_of_subset_right interior_subset rw [this] apply isOpen_interior have f2 : IsOpen v := VisClopen.2.preimage continuous_subtype_val have f3 : ((↑) : s → H) '' V = ((↑) : u → H) '' v := by - rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_left V_sub] + rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_right V_sub] rw [f3] apply f1.isOpenMap v f2 refine' ⟨(↑) '' V, VisClopen', by simp [Vx], Subset.trans _ sU⟩ diff --git a/Mathlib/Topology/Sober.lean b/Mathlib/Topology/Sober.lean index efc29ef2d7623..ca936d6f93dfa 100644 --- a/Mathlib/Topology/Sober.lean +++ b/Mathlib/Topology/Sober.lean @@ -236,7 +236,7 @@ theorem quasiSober_of_open_cover (S : Set (Set α)) (hS : ∀ s : S, IsOpen (s : rw [← image_singleton, ← closure_image_closure continuous_subtype_val, H.genericPoint_spec.def] refine' (subset_closure_inter_of_isPreirreducible_of_isOpen h.2 (hS ⟨U, hU⟩) ⟨x, hx, hU'⟩).trans (closure_mono _) - rw [← Subtype.image_preimage_coe] + rw [inter_comm t, ← Subtype.image_preimage_coe] exact Set.image_subset _ subset_closure #align quasi_sober_of_open_cover quasiSober_of_open_cover From 76fbdb05d8a953b73b09ef58bc767b00a46e34f7 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 13 Feb 2024 09:28:45 -0800 Subject: [PATCH 2/3] review --- Mathlib/Data/Set/Image.lean | 8 ++++++-- Mathlib/GroupTheory/Subgroup/Basic.lean | 1 + 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean index cf75f0e482bf3..4f6717c7ccbf7 100644 --- a/Mathlib/Data/Set/Image.lean +++ b/Mathlib/Data/Set/Image.lean @@ -1414,11 +1414,15 @@ theorem preimage_coe_eq_preimage_coe_iff {s t u : Set α} : rw [← image_preimage_coe, ← image_preimage_coe, coe_injective.image_injective.eq_iff] #align subtype.preimage_coe_eq_preimage_coe_iff Subtype.preimage_coe_eq_preimage_coe_iff +theorem preimage_coe_self_inter (s t : Set α) : + ((↑) : s → α) ⁻¹' (s ∩ t) = ((↑) : s → α) ⁻¹' t := by + rw [preimage_coe_eq_preimage_coe_iff, ← inter_assoc, inter_self] + -- Porting note: -- @[simp] `simp` can prove this theorem preimage_coe_inter_self (s t : Set α) : - ((↑) : s → α) ⁻¹' (s ∩ t) = ((↑) : s → α) ⁻¹' t := by - rw [preimage_coe_eq_preimage_coe_iff, ← inter_assoc, inter_self] + ((↑) : s → α) ⁻¹' (t ∩ s) = ((↑) : s → α) ⁻¹' t := by + rw [inter_comm, preimage_coe_self_inter] #align subtype.preimage_coe_inter_self Subtype.preimage_coe_inter_self theorem preimage_val_eq_preimage_val_iff (s t u : Set α) : diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean index a637e1974625a..82418b9e0c995 100644 --- a/Mathlib/GroupTheory/Subgroup/Basic.lean +++ b/Mathlib/GroupTheory/Subgroup/Basic.lean @@ -1677,6 +1677,7 @@ theorem mem_subgroupOf {H K : Subgroup G} {h : K} : h ∈ H.subgroupOf K ↔ (h #align subgroup.mem_subgroup_of Subgroup.mem_subgroupOf #align add_subgroup.mem_add_subgroup_of AddSubgroup.mem_addSubgroupOf +-- TODO(kmill): use `K ⊓ H` order for RHS to match `Subtype.image_preimage_coe` @[to_additive (attr := simp)] theorem subgroupOf_map_subtype (H K : Subgroup G) : (H.subgroupOf K).map K.subtype = H ⊓ K := SetLike.ext' <| by refine Subtype.image_preimage_coe _ _ |>.trans ?_; apply Set.inter_comm From ab3ac8c92a26ce03c0c19936b0b68c3f75a86de6 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 13 Feb 2024 09:29:33 -0800 Subject: [PATCH 3/3] fix --- Mathlib/Topology/ContinuousOn.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean index 35608c7e7ba53..884de1d96436b 100644 --- a/Mathlib/Topology/ContinuousOn.lean +++ b/Mathlib/Topology/ContinuousOn.lean @@ -1327,7 +1327,7 @@ theorem frontier_inter_open_inter {s t : Set α} (ht : IsOpen t) : frontier (s ∩ t) ∩ t = frontier s ∩ t := by simp only [Set.inter_comm _ t, ← Subtype.preimage_coe_eq_preimage_coe_iff, ht.isOpenMap_subtype_val.preimage_frontier_eq_frontier_preimage continuous_subtype_val, - Subtype.preimage_coe_inter_self] + Subtype.preimage_coe_self_inter] #align frontier_inter_open_inter frontier_inter_open_inter theorem continuousOn_fst {s : Set (α × β)} : ContinuousOn Prod.fst s :=