From 905e5294d946c4f1507c406c8a8d3d4ffafceaf2 Mon Sep 17 00:00:00 2001 From: sven-manthe Date: Thu, 7 Mar 2024 06:34:56 +0000 Subject: [PATCH] feat: add simp lemma (#11206) It is already there for inf/sup, now add it to inter/union. Now simp succeeds in cases where previously symm; simp was necessary --- Mathlib/Data/Set/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index f1d8ecb5d1a4c0..5858a0d14d2998 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -954,6 +954,10 @@ theorem subset_inter_iff {s t r : Set α} : r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ @[simp] lemma inter_eq_right : s ∩ t = t ↔ t ⊆ s := inf_eq_right #align set.inter_eq_right_iff_subset Set.inter_eq_right +@[simp] lemma left_eq_inter : s = s ∩ t ↔ s ⊆ t := left_eq_inf + +@[simp] lemma right_eq_inter : t = s ∩ t ↔ t ⊆ s := right_eq_inf + theorem inter_eq_self_of_subset_left {s t : Set α} : s ⊆ t → s ∩ t = s := inter_eq_left.mpr #align set.inter_eq_self_of_subset_left Set.inter_eq_self_of_subset_left