[Merged by Bors] - chore(Data/Set): add missing Set.forall_mem_* lemmas

Mathlib/Data/Set/Basic.lean

@@ -498,6 +498,12 @@ theorem subset_eq_empty {s t : Set α} (h : t ⊆ s) (e : s = ∅) : t = ∅ :=
 theorem forall_mem_empty {p : α → Prop} : (∀ x ∈ (∅ : Set α), p x) ↔ True :=
   iff_true_intro fun _ => False.elim
 
+theorem forall_mem_univ {p : α → Prop} : (∀ x ∈ (univ : Set α), p x) ↔ ∀ x, p x :=
+  ⟨fun h x => h x (mem_univ x), fun h x _ => h x⟩
+
+theorem forall_mem_ofPred {p q : α → Prop} : (∀ x ∈ ({x | q x} : Set α), p x) ↔ ∀ x, q x → p x :=
+  .rfl
+
 theorem Nonempty.forall_const (h : s.Nonempty) {p : Prop} : (∀ x ∈ s, p) ↔ p :=
   let ⟨x, hx⟩ := h
   ⟨fun h ↦ h x hx, fun h _ _ ↦ h⟩
@@ -506,6 +512,22 @@ theorem Nonempty.forall_const (h : s.Nonempty) {p : Prop} : (∀ x ∈ s, p) ↔
 theorem forall_mem_const {p : Prop} [Nonempty s] : (∀ x ∈ s, p) ↔ p :=
   (nonempty_coe_sort.mp ‹_›).forall_const
 
+theorem exists_mem_empty {p : α → Prop} : (∃ x ∈ (∅ : Set α), p x) ↔ False :=
+  iff_false_intro fun h => h.elim fun _ => And.left
+
+theorem exists_mem_univ {p : α → Prop} : (∃ x ∈ (univ : Set α), p x) ↔ ∃ x, p x :=
+  ⟨Exists.imp fun _ => And.right, Exists.imp fun x => And.intro (mem_univ x)⟩
+
+theorem exists_mem_ofPred {p q : α → Prop} : (∃ x ∈ ({x | q x} : Set α), p x) ↔ ∃ x, q x ∧ p x :=
+  .rfl
+
+theorem Nonempty.exists_const (h : s.Nonempty) {p : Prop} : (∃ x ∈ s, p) ↔ p :=
+  let ⟨x, hx⟩ := h
+  ⟨fun h ↦ h.elim fun _ => And.right, fun h ↦ ⟨x, hx, h⟩⟩
+
+theorem exists_mem_const {p : Prop} [Nonempty s] : (∃ x ∈ s, p) ↔ p :=
+  (nonempty_coe_sort.mp ‹_›).exists_const
+
 instance (α : Type u) : IsEmpty.{u + 1} (↥(∅ : Set α)) :=
   ⟨fun x => x.2⟩
 
@@ -723,6 +745,14 @@ theorem ssubset_union_left_iff : s ⊂ s ∪ t ↔ ¬ t ⊆ s :=
 theorem ssubset_union_right_iff : t ⊂ s ∪ t ↔ ¬ s ⊆ t :=
   right_lt_sup
 
+theorem forall_mem_union {p : α → Prop} :
+    (∀ x ∈ s ∪ t, p x) ↔ (∀ x ∈ s, p x) ∧ (∀ x ∈ t, p x) := by
+  simp_rw [mem_union, or_imp, forall_and]
+
+theorem exists_mem_union {p : α → Prop} :
+    (∃ x ∈ s ∪ t, p x) ↔ (∃ x ∈ s, p x) ∨ (∃ x ∈ t, p x) := by
+  simp_rw [mem_union, or_and_right, exists_or]
+
 /-! ### Lemmas about intersection -/
 
 theorem inter_def {s₁ s₂ : Set α} : s₁ ∩ s₂ = { a | a ∈ s₁ ∧ a ∈ s₂ } :=
@@ -889,6 +919,14 @@ theorem union_union_union_comm (s t u v : Set α) : s ∪ t ∪ (u ∪ v) = s 
 theorem inter_inter_inter_comm (s t u v : Set α) : s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v) :=
   inf_inf_inf_comm _ _ _ _
 
+theorem forall_mem_inter {p : α → Prop} :
+    (∀ x ∈ s ∩ t, p x) ↔ (∀ x ∈ s, x ∈ t → p x) := by
+  simp_rw [mem_inter_iff, and_imp]
+
+theorem exists_mem_inter {p : α → Prop} :
+    (∃ x ∈ s ∩ t, p x) ↔ (∃ x ∈ s, x ∈ t ∧ p x) := by
+  simp_rw [mem_inter_iff, and_assoc]
+
 /-! ### Lemmas about sets defined as `{x ∈ s | p x}`. -/
 
 section Sep

Mathlib/Data/Set/Insert.lean

@@ -229,6 +229,12 @@ theorem singleton_union : {a} ∪ s = insert a s :=
 theorem union_singleton : s ∪ {a} = insert a s :=
   union_comm _ _
 
+theorem exists_mem_singleton {P : α → Prop} {a : α} :
+    (∃ x ∈ ({a} : Set α), P x) ↔ P a := by grind
+
+theorem forall_mem_singleton {P : α → Prop} {a : α} :
+    (∀ x ∈ ({a} : Set α), P x) ↔ P a := by grind
+
 @[simp]
 theorem singleton_inter_nonempty : ({a} ∩ s).Nonempty ↔ a ∈ s := by
   simp only [Set.Nonempty, mem_inter_iff, mem_singleton_iff, exists_eq_left]

Mathlib/Data/Set/Lattice.lean

@@ -43,6 +43,8 @@ In lemma names,
 * `⋂₀`: `Set.sInter`
 -/
 
+set_option linter.style.longFile 1700
+
 @[expose] public section
 
 open Function Set
@@ -270,6 +272,32 @@ theorem iInter_ofPred (P : ι → α → Prop) : ⋂ i, { x : α | P i x } = { x
 
 @[deprecated (since := "2026-07-09")] alias iInter_setOf := iInter_ofPred
 
+theorem forall_mem_iUnion {p : α → Prop} {f : ι → Set α} :
+    (∀ x ∈ ⋃ i, f i, p x) ↔ (∀ i, ∀ x ∈ f i, p x) := by
+  simp_rw [mem_iUnion, forall_exists_index]
+  apply forall_comm
+
+theorem exists_mem_iUnion {p : α → Prop} {f : ι → Set α} :
+    (∃ x ∈ ⋃ i, f i, p x) ↔ (∃ i, ∃ x ∈ f i, p x) := by
+  grind [mem_iUnion]
+
+theorem forall_mem_iUnion₂ {p : α → Prop} {f : (i : ι) → κ i → Set α} :
+    (∀ x ∈ ⋃ (i) (j), f i j, p x) ↔ (∀ i j, ∀ x ∈ f i j, p x) := by
+  simp_rw [forall_mem_iUnion]
+
+theorem exists_mem_iUnion₂ {p : α → Prop} {f : (i : ι) → κ i → Set α} :
+    (∃ x ∈ ⋃ (i) (j), f i j, p x) ↔ (∃ i j, ∃ x ∈ f i j, p x) := by
+  simp_rw [exists_mem_iUnion]
+
+theorem forall_mem_biUnion {p : α → Prop} {f : ι → Set α} {q : ι → Prop} :
+    (∀ x ∈ ⋃ (i : ι) (_ : q i), f i, p x) ↔ (∀ i, q i → ∀ x ∈ f i, p x) :=
+  forall_mem_iUnion₂
+
+theorem exists_mem_biUnion {p : α → Prop} {f : (i : ι) → Set α} {q : ι → Prop} :
+    (∃ x ∈ ⋃ (i : ι) (_ : q i), f i, p x) ↔ (∃ i, q i ∧ ∃ x ∈ f i, p x) := by
+  rw [exists_mem_iUnion₂]
+  simp_rw [exists_prop]
+
 theorem iUnion_congr_of_surjective {f : ι → Set α} {g : ι₂ → Set α} (h : ι → ι₂) (h1 : Surjective h)
     (h2 : ∀ x, g (h x) = f x) : ⋃ x, f x = ⋃ y, g y :=
   h1.iSup_congr h h2