feat(order/lattice, data/set): some helper lemmas (#14789)

This PR provides lemmas describing when `s ∪ a = t ∪ a`, in both necessary and iff forms, as well as intersection and lattice versions. 



Co-authored-by: Peter Nelson <apnelson@uwaterloo.ca>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>

src/data/set/basic.lean

@@ -526,6 +526,13 @@ subset.trans h (subset_union_left t u)
 lemma subset_union_of_subset_right {s u : set α} (h : s ⊆ u) (t : set α) : s ⊆ t ∪ u :=
 subset.trans h (subset_union_right t u)
 
+lemma union_eq_union_of_subset_of_subset {s t a : set α} (h1 : s ⊆ t ∪ a) (h2 : t ⊆ s ∪ a) :
+  s ∪ a = t ∪ a :=
+sup_eq_sup_of_le_of_le h1 h2
+
+lemma union_eq_union_iff_subset_subset {s t a : set α} : s ∪ a = t ∪ a ↔ s ⊆ t ∪ a ∧ t ⊆ s ∪ a :=
+sup_eq_sup_iff_le_le
+
 @[simp] theorem union_empty_iff {s t : set α} : s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅ :=
 by simp only [← subset_empty_iff]; exact union_subset_iff
 
@@ -588,6 +595,13 @@ inter_eq_left_iff_subset.mpr
 theorem inter_eq_self_of_subset_right {s t : set α} : t ⊆ s → s ∩ t = t :=
 inter_eq_right_iff_subset.mpr
 
+lemma inter_eq_inter_of_subset_of_subset {s t a : set α} (h1 : t ∩ a ⊆ s) (h2 : s ∩ a ⊆ t) :
+  s ∩ a = t ∩ a :=
+inf_eq_inf_of_le_of_le h1 h2
+
+lemma inter_eq_inter_iff_subset_subset {s t a : set α} : s ∩ a = t ∩ a ↔ t ∩ a ⊆ s ∧ s ∩ a ⊆ t :=
+inf_eq_inf_iff_le_le
+
 @[simp] theorem inter_univ (a : set α) : a ∩ univ = a := inf_top_eq
 
 @[simp] theorem univ_inter (a : set α) : univ ∩ a = a := top_inf_eq

src/order/lattice.lean

@@ -242,6 +242,12 @@ by rw [sup_sup_sup_comm, sup_idem]
 lemma sup_sup_distrib_right (a b c : α) : (a ⊔ b) ⊔ c = (a ⊔ c) ⊔ (b ⊔ c) :=
 by rw [sup_sup_sup_comm, sup_idem]
 
+lemma sup_eq_sup_of_le_of_le (h1 : a ≤ b ⊔ c) (h2 : b ≤ a ⊔ c) : a ⊔ c = b ⊔ c :=
+(sup_le h1 le_sup_right).antisymm (sup_le h2 le_sup_right)
+
+lemma sup_eq_sup_iff_le_le : a ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c :=
+⟨λ h, ⟨h ▸ le_sup_left, h.symm ▸ le_sup_left⟩, λ h, sup_eq_sup_of_le_of_le h.1 h.2⟩
+
 /-- If `f` is monotone, `g` is antitone, and `f ≤ g`, then for all `a`, `b` we have `f a ≤ g b`. -/
 theorem monotone.forall_le_of_antitone {β : Type*} [preorder β] {f g : α → β}
   (hf : monotone f) (hg : antitone g) (h : f ≤ g) (m n : α) :
@@ -395,6 +401,12 @@ lemma inf_inf_distrib_left (a b c : α) : a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ (a ⊓
 lemma inf_inf_distrib_right (a b c : α) : (a ⊓ b) ⊓ c = (a ⊓ c) ⊓ (b ⊓ c) :=
 @sup_sup_distrib_right αᵒᵈ _ _ _ _
 
+lemma inf_eq_inf_of_le_of_le (h1 : b ⊓ c ≤ a) (h2 : a ⊓ c ≤ b) : a ⊓ c = b ⊓ c :=
+@sup_eq_sup_of_le_of_le αᵒᵈ _ _ _ _ h1 h2
+
+lemma inf_eq_inf_iff_le_le : a ⊓ c = b ⊓ c ↔ b ⊓ c ≤ a ∧ a ⊓ c ≤ b :=
+@sup_eq_sup_iff_le_le αᵒᵈ _ _ _ _
+
 theorem semilattice_inf.ext_inf {α} {A B : semilattice_inf α}
   (H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y)
   (x y : α) : (by haveI := A; exact (x ⊓ y)) = x ⊓ y :=