feat: When a \ b = b \ a (#9109)

and other simple order lemmas

From LeanAPAP and LeanCamCombi

Author: YaelDillies

Mathlib/Order/BooleanAlgebra.lean

@@ -326,6 +326,11 @@ theorem le_sdiff_iff : x ≤ y \ x ↔ x = ⊥ :=
   ⟨fun h => disjoint_self.1 (disjoint_sdiff_self_right.mono_right h), fun h => h.le.trans bot_le⟩
 #align le_sdiff_iff le_sdiff_iff
 
+@[simp] lemma sdiff_eq_right : x \ y = y ↔ x = ⊥ ∧ y = ⊥ := by
+  rw [disjoint_sdiff_self_left.eq_iff]; aesop
+
+lemma sdiff_ne_right : x \ y ≠ y ↔ x ≠ ⊥ ∨ y ≠ ⊥ := sdiff_eq_right.not.trans not_and_or
+
 theorem sdiff_lt_sdiff_right (h : x < y) (hz : z ≤ x) : x \ z < y \ z :=
   (sdiff_le_sdiff_right h.le).lt_of_not_le
     fun h' => h.not_le <| le_sdiff_sup.trans <| sup_le_of_le_sdiff_right h' hz
@@ -771,6 +776,14 @@ theorem himp_le : x ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z :=
   (@le_sdiff αᵒᵈ _ _ _ _).trans <| and_congr_right' $ @Codisjoint_comm _ (_) _ _ _
 #align himp_le himp_le
 
+@[simp] lemma himp_le_iff : x ⇨ y ≤ x ↔ x = ⊤ :=
+  ⟨fun h ↦ codisjoint_self.1 $ codisjoint_himp_self_right.mono_right h, fun h ↦ le_top.trans h.ge⟩
+
+@[simp] lemma himp_eq_left : x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤ := by
+  rw [codisjoint_himp_self_left.eq_iff]; aesop
+
+lemma himp_ne_right : x ⇨ y ≠ x ↔ x ≠ ⊤ ∨ y ≠ ⊤ := himp_eq_left.not.trans not_and_or
+
 end BooleanAlgebra
 
 instance Prop.booleanAlgebra : BooleanAlgebra Prop :=

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

@@ -1177,7 +1177,7 @@ In this case we have `Sup ∅ = ⊥`, so we can drop some `Nonempty`/`Set.Nonemp
 
 section ConditionallyCompleteLinearOrderBot
 
-variable [ConditionallyCompleteLinearOrderBot α]
+variable [ConditionallyCompleteLinearOrderBot α] {s : Set α} {f : ι → α} {a : α}
 
 @[simp]
 theorem csSup_empty : (sSup ∅ : α) = ⊥ :=
@@ -1223,21 +1223,21 @@ theorem le_ciSup_iff' {s : ι → α} {a : α} (h : BddAbove (range s)) :
 
 theorem le_csInf_iff'' {s : Set α} {a : α} (ne : s.Nonempty) :
     a ≤ sInf s ↔ ∀ b : α, b ∈ s → a ≤ b :=
-  le_csInf_iff ⟨⊥, fun _ _ => bot_le⟩ ne
+  le_csInf_iff (OrderBot.bddBelow _) ne
 #align le_cInf_iff'' le_csInf_iff''
 
 theorem le_ciInf_iff' [Nonempty ι] {f : ι → α} {a : α} : a ≤ iInf f ↔ ∀ i, a ≤ f i :=
-  le_ciInf_iff ⟨⊥, fun _ _ => bot_le⟩
+  le_ciInf_iff (OrderBot.bddBelow _)
 #align le_cinfi_iff' le_ciInf_iff'
 
-theorem csInf_le' {s : Set α} {a : α} (h : a ∈ s) : sInf s ≤ a :=
-  csInf_le ⟨⊥, fun _ _ => bot_le⟩ h
+theorem csInf_le' (h : a ∈ s) : sInf s ≤ a := csInf_le (OrderBot.bddBelow _) h
 #align cInf_le' csInf_le'
 
-theorem ciInf_le' (f : ι → α) (i : ι) : iInf f ≤ f i :=
-  ciInf_le ⟨⊥, fun _ _ => bot_le⟩ _
+theorem ciInf_le' (f : ι → α) (i : ι) : iInf f ≤ f i := ciInf_le (OrderBot.bddBelow _) _
 #align cinfi_le' ciInf_le'
 
+lemma ciInf_le_of_le' (c : ι) : f c ≤ a → iInf f ≤ a := ciInf_le_of_le (OrderBot.bddBelow _) _
+
 theorem exists_lt_of_lt_csSup' {s : Set α} {a : α} (h : a < sSup s) : ∃ b ∈ s, a < b := by
   contrapose! h
   exact csSup_le' h

Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

@@ -84,9 +84,9 @@ non-empty. As a result, we can translate between the two.
 
 
 namespace Finset
+variable {ι : Type*} [ConditionallyCompleteLattice α]
 
-theorem sup'_eq_csSup_image [ConditionallyCompleteLattice β] (s : Finset α) (H) (f : α → β) :
-    s.sup' H f = sSup (f '' s) := by
+theorem sup'_eq_csSup_image (s : Finset ι) (H) (f : ι → α) : s.sup' H f = sSup (f '' s) := by
   apply le_antisymm
   · refine' Finset.sup'_le _ _ fun a ha => _
     refine' le_csSup ⟨s.sup' H f, _⟩ ⟨a, ha, rfl⟩
@@ -97,18 +97,24 @@ theorem sup'_eq_csSup_image [ConditionallyCompleteLattice β] (s : Finset α) (H
     exact Finset.le_sup' _ ha
 #align finset.sup'_eq_cSup_image Finset.sup'_eq_csSup_image
 
-theorem inf'_eq_csInf_image [ConditionallyCompleteLattice β] (s : Finset α) (H) (f : α → β) :
-    s.inf' H f = sInf (f '' s) :=
-  @sup'_eq_csSup_image _ βᵒᵈ _ _ H _
+theorem inf'_eq_csInf_image (s : Finset ι) (hs) (f : ι → α) : s.inf' hs f = sInf (f '' s) :=
+  sup'_eq_csSup_image (α := αᵒᵈ) _ hs _
 #align finset.inf'_eq_cInf_image Finset.inf'_eq_csInf_image
 
-theorem sup'_id_eq_csSup [ConditionallyCompleteLattice α] (s : Finset α) (H) :
-    s.sup' H id = sSup s := by rw [sup'_eq_csSup_image s H, Set.image_id]
+theorem sup'_id_eq_csSup (s : Finset α) (hs) : s.sup' hs id = sSup s := by
+  rw [sup'_eq_csSup_image s hs, Set.image_id]
 #align finset.sup'_id_eq_cSup Finset.sup'_id_eq_csSup
 
-theorem inf'_id_eq_csInf [ConditionallyCompleteLattice α] (s : Finset α) (H) :
-    s.inf' H id = sInf s :=
-  @sup'_id_eq_csSup αᵒᵈ _ _ H
+theorem inf'_id_eq_csInf (s : Finset α) (hs) : s.inf' hs id = sInf s :=
+  sup'_id_eq_csSup (α := αᵒᵈ) _ hs
 #align finset.inf'_id_eq_cInf Finset.inf'_id_eq_csInf
 
+variable [Fintype ι] [Nonempty ι]
+
+lemma sup'_univ_eq_ciSup (f : ι → α) : univ.sup' univ_nonempty f = ⨆ i, f i := by
+  simp [sup'_eq_csSup_image, iSup]
+
+lemma inf'_univ_eq_ciInf (f : ι → α) : univ.inf' univ_nonempty f = ⨅ i, f i := by
+  simp [inf'_eq_csInf_image, iInf]
+
 end Finset

Mathlib/Order/Disjoint.lean

@@ -101,6 +101,10 @@ theorem Disjoint.eq_bot_of_ge (hab : Disjoint a b) : b ≤ a → b = ⊥ :=
   hab.symm.eq_bot_of_le
 #align disjoint.eq_bot_of_ge Disjoint.eq_bot_of_ge
 
+lemma Disjoint.eq_iff (hab : Disjoint a b) : a = b ↔ a = ⊥ ∧ b = ⊥ := by aesop
+lemma Disjoint.ne_iff (hab : Disjoint a b) : a ≠ b ↔ a ≠ ⊥ ∨ b ≠ ⊥ :=
+  hab.eq_iff.not.trans not_and_or
+
 end PartialOrderBot
 
 section PartialBoundedOrder
@@ -285,6 +289,10 @@ theorem Codisjoint.eq_top_of_ge (hab : Codisjoint a b) : a ≤ b → b = ⊤ :=
   hab.symm.eq_top_of_le
 #align codisjoint.eq_top_of_ge Codisjoint.eq_top_of_ge
 
+lemma Codisjoint.eq_iff (hab : Codisjoint a b) : a = b ↔ a = ⊤ ∧ b = ⊤ := by aesop
+lemma Codisjoint.ne_iff (hab : Codisjoint a b) : a ≠ b ↔ a ≠ ⊤ ∨ b ≠ ⊤ :=
+  hab.eq_iff.not.trans not_and_or
+
 end PartialOrderTop
 
 section PartialBoundedOrder

Mathlib/Order/Heyting/Basic.lean

@@ -442,6 +442,9 @@ theorem le_himp_himp : a ≤ (a ⇨ b) ⇨ b :=
   le_himp_iff.2 inf_himp_le
 #align le_himp_himp le_himp_himp
 
+@[simp] lemma himp_eq_himp_iff : b ⇨ a = a ⇨ b ↔ a = b := by simp [le_antisymm_iff]
+lemma himp_ne_himp_iff : b ⇨ a ≠ a ⇨ b ↔ a ≠ b := himp_eq_himp_iff.not
+
 theorem himp_triangle (a b c : α) : (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c := by
   rw [le_himp_iff, inf_right_comm, ← le_himp_iff]
   exact himp_inf_le.trans le_himp_himp
@@ -698,6 +701,9 @@ theorem sdiff_sdiff_le : a \ (a \ b) ≤ b :=
   sdiff_le_iff.2 le_sdiff_sup
 #align sdiff_sdiff_le sdiff_sdiff_le
 
+@[simp] lemma sdiff_eq_sdiff_iff : a \ b = b \ a ↔ a = b := by simp [le_antisymm_iff]
+lemma sdiff_ne_sdiff_iff : a \ b ≠ b \ a ↔ a ≠ b := sdiff_eq_sdiff_iff.not
+
 theorem sdiff_triangle (a b c : α) : a \ c ≤ a \ b ⊔ b \ c := by
   rw [sdiff_le_iff, sup_left_comm, ← sdiff_le_iff]
   exact sdiff_sdiff_le.trans le_sup_sdiff