From f94dd660e5d3567d83def67decefae373ecb09a4 Mon Sep 17 00:00:00 2001
From: Hannah Scholz <hannah@scholzbande.de>
Date: Tue, 22 Oct 2024 14:15:53 +0000
Subject: [PATCH] feat: 'and' and 'exist' commute for Antitone or Monotone
 properties (#17947)

---
 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