From 5af36d12e8e0e1bbb9211788c394425ec79b6a17 Mon Sep 17 00:00:00 2001
From: Hannah Scholz <hannah@scholzbande.de>
Date: Sat, 19 Oct 2024 18:41:31 +0200
Subject: [PATCH] added lemmas about 'exists' and 'and' commuting

---
 Mathlib/Order/BoundedOrder.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/Mathlib/Order/BoundedOrder.lean b/Mathlib/Order/BoundedOrder.lean
index a28c66b0685a2..7c89768bd45e6 100644
--- a/Mathlib/Order/BoundedOrder.lean
+++ b/Mathlib/Order/BoundedOrder.lean
@@ -503,6 +503,11 @@ theorem exists_ge_and_iff_exists {P : α → Prop} {x₀ : α} (hP : Monotone P)
     (∃ x, x₀ ≤ x ∧ P x) ↔ ∃ x, P x :=
   ⟨fun h => h.imp fun _ h => h.2, fun ⟨x, hx⟩ => ⟨x ⊔ x₀, le_sup_right, hP le_sup_left hx⟩⟩
 
+lemma exists_and_iff_of_monotone {P Q : α → Prop} (hP : Monotone P) (hQ : Monotone Q) :
+    ((∃ x, P x) ∧ ∃ x, Q x) ↔ (∃ x, P x ∧ Q x) :=
+  ⟨fun ⟨⟨x, hPx⟩, ⟨y, hQx⟩⟩ ↦ ⟨x ⊔ y, ⟨hP le_sup_left hPx, hQ le_sup_right hQx⟩⟩,
+    fun ⟨x, hPx, hQx⟩ ↦ ⟨⟨x, hPx⟩, ⟨x, hQx⟩⟩⟩
+
 end SemilatticeSup
 
 section SemilatticeInf
@@ -513,6 +518,11 @@ theorem exists_le_and_iff_exists {P : α → Prop} {x₀ : α} (hP : Antitone P)
     (∃ x, x ≤ x₀ ∧ P x) ↔ ∃ x, P x :=
   exists_ge_and_iff_exists <| hP.dual_left
 
+lemma exists_and_iff_of_antitone {P Q : α → Prop} (hP : Antitone P) (hQ : Antitone Q) :
+    ((∃ x, P x) ∧ ∃ x, Q x) ↔ (∃ x, P x ∧ Q x) :=
+  ⟨fun ⟨⟨x, hPx⟩, ⟨y, hQx⟩⟩ ↦ ⟨x ⊓ y, ⟨hP inf_le_left hPx, hQ inf_le_right hQx⟩⟩,
+    fun ⟨x, hPx, hQx⟩ ↦ ⟨⟨x, hPx⟩, ⟨x, hQx⟩⟩⟩
+
 end SemilatticeInf
 
 end Logic