feat: minimals/maximals API (#5911)

This PR adds some API to `Data.Order.Minimal`, with a few rewrite lemmas for membership in sets of maximals/minimals, lemmas that give sufficient conditions for two sets having the same maximal/minimal elements, and a bunch of lemmas about images/preimages of sets of maximal elements.

Mathlib/Order/Minimal.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Order.Antichain
 import Mathlib.Order.UpperLower.Basic
+import Mathlib.Data.Set.Intervals.Basic
 
 #align_import order.minimal from "leanprover-community/mathlib"@"59694bd07f0a39c5beccba34bd9f413a160782bf"
 
@@ -90,6 +91,44 @@ theorem eq_of_mem_minimals (ha : a ∈ minimals r s) (hb : b ∈ s) (h : r b a)
   antisymm (ha.2 hb h) h
 #align eq_of_mem_minimals eq_of_mem_minimals
 
+theorem mem_maximals_iff : x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y⦄, y ∈ s → r x y → x = y := by
+  simp only [maximals, Set.mem_sep_iff, and_congr_right_iff]
+  refine' fun _ ↦ ⟨fun h y hys hxy ↦ antisymm hxy (h hys hxy), fun h y hys hxy ↦ _⟩
+  convert hxy <;> rw [h hys hxy]
+
+theorem mem_maximals_setOf_iff : x ∈ maximals r (setOf P) ↔ P x ∧ ∀ ⦃y⦄, P y → r x y → x = y :=
+  mem_maximals_iff
+
+theorem mem_minimals_iff : x ∈ minimals r s ↔ x ∈ s ∧ ∀ ⦃y⦄, y ∈ s → r y x → x = y :=
+  @mem_maximals_iff _ _ _ (IsAntisymm.swap r) _
+
+theorem mem_minimals_setOf_iff : x ∈ minimals r (setOf P) ↔ P x ∧ ∀ ⦃y⦄, P y → r y x → x = y :=
+  mem_minimals_iff
+
+/-- This theorem can't be used to rewrite without specifying `rlt`, since `rlt` would have to be
+  guessed. See `mem_minimals_iff_forall_ssubset_not_mem` and `mem_minimals_iff_forall_lt_not_mem`
+  for `⊆` and `≤` versions.  -/
+theorem mem_minimals_iff_forall_lt_not_mem' (rlt : α → α → Prop) [IsNonstrictStrictOrder α r rlt] :
+    x ∈ minimals r s ↔ x ∈ s ∧ ∀ ⦃y⦄, rlt y x → y ∉ s := by
+  simp [minimals, right_iff_left_not_left_of r rlt, not_imp_not, imp.swap (a := _ ∈ _)]
+
+theorem mem_maximals_iff_forall_lt_not_mem' (rlt : α → α → Prop) [IsNonstrictStrictOrder α r rlt] :
+    x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y⦄, rlt x y → y ∉ s := by
+  simp [maximals, right_iff_left_not_left_of r rlt, not_imp_not, imp.swap (a := _ ∈ _)]
+
+theorem minimals_eq_minimals_of_subset_of_forall [IsTrans α r] (hts : t ⊆ s)
+    (h : ∀ x ∈ s, ∃ y ∈ t, r y x) : minimals r s = minimals r t := by
+  refine Set.ext fun a ↦ ⟨fun ⟨has, hmin⟩ ↦ ⟨?_,fun b hbt ↦ hmin (hts hbt)⟩,
+    fun ⟨hat, hmin⟩ ↦ ⟨hts hat, fun b hbs hba ↦ ?_⟩⟩
+  · obtain ⟨a', ha', haa'⟩ := h _ has
+    rwa [antisymm (hmin (hts ha') haa') haa']
+  obtain ⟨b', hb't, hb'b⟩ := h b hbs
+  rwa [antisymm (hmin hb't (Trans.trans hb'b hba)) (Trans.trans hb'b hba)]
+
+theorem maximals_eq_maximals_of_subset_of_forall [IsTrans α r] (hts : t ⊆ s)
+    (h : ∀ x ∈ s, ∃ y ∈ t, r x y) : maximals r s = maximals r t :=
+  @minimals_eq_minimals_of_subset_of_forall _ _ _ _ (IsAntisymm.swap r) (IsTrans.swap r) hts h
+
 variable (r s)
 
 theorem maximals_antichain : IsAntichain r (maximals r s) := fun _a ha _b hb hab h =>
@@ -103,11 +142,27 @@ theorem minimals_antichain : IsAntichain r (minimals r s) :=
 
 end IsAntisymm
 
--- porting note: new lemma
+theorem mem_minimals_iff_forall_ssubset_not_mem (s : Set (Set α)) :
+    x ∈ minimals (· ⊆ ·) s ↔ x ∈ s ∧ ∀ ⦃y⦄, y ⊂ x → y ∉ s :=
+  mem_minimals_iff_forall_lt_not_mem' (· ⊂ ·)
+
+theorem mem_minimals_iff_forall_lt_not_mem [PartialOrder α] {s : Set α} :
+    x ∈ minimals (· ≤ ·) s ↔ x ∈ s ∧ ∀ ⦃y⦄, y < x → y ∉ s :=
+  mem_minimals_iff_forall_lt_not_mem' (· < ·)
+
+theorem mem_maximals_iff_forall_ssubset_not_mem {s : Set (Set α)} :
+    x ∈ maximals (· ⊆ ·) s ↔ x ∈ s ∧ ∀ ⦃y⦄, x ⊂ y → y ∉ s :=
+  mem_maximals_iff_forall_lt_not_mem' (· ⊂ ·)
+
+theorem mem_maximals_iff_forall_lt_not_mem [PartialOrder α] {s : Set α} :
+    x ∈ maximals (· ≤ ·) s ↔ x ∈ s ∧ ∀ ⦃y⦄, x < y → y ∉ s :=
+  mem_maximals_iff_forall_lt_not_mem' (· < ·)
+
+-- porting note: new theorem
 theorem maximals_of_symm [IsSymm α r] : maximals r s = s :=
   sep_eq_self_iff_mem_true.2 <| fun _ _ _ _ => symm
 
--- porting note: new lemma
+-- porting note: new theorem
 theorem minimals_of_symm [IsSymm α r] : minimals r s = s :=
   sep_eq_self_iff_mem_true.2 <| fun _ _ _ _ => symm
 
@@ -240,3 +295,112 @@ theorem IsAntichain.maximals_lowerClosure (hs : IsAntichain (· ≤ ·) s) :
     maximals (· ≤ ·) (lowerClosure s : Set α) = s :=
   hs.to_dual.minimals_upperClosure
 #align is_antichain.maximals_lower_closure IsAntichain.maximals_lowerClosure
+
+section Image
+
+variable {f : α → β} {r : α → α → Prop} {s : β → β → Prop}
+
+theorem minimals_image_of_rel_iff_rel (hf : ∀ ⦃a a'⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))) :
+    minimals s (f '' x) = f '' (minimals r x) := by
+  ext a
+  simp only [minimals, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
+  constructor
+  · rintro ⟨⟨a, ha, rfl⟩ , h⟩
+    exact ⟨a, ⟨ha, fun y hy hya ↦ (hf ha hy).mpr (h _ hy ((hf hy ha).mp hya))⟩, rfl⟩
+  rintro ⟨a,⟨⟨ha,h⟩,rfl⟩⟩
+  exact ⟨⟨_, ha, rfl⟩, fun y hy hya ↦ (hf ha hy).mp (h hy ((hf hy ha).mpr hya))⟩
+
+theorem maximals_image_of_rel_iff_rel_on
+    (hf : ∀ ⦃a a'⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))) :
+    maximals s (f '' x) = f '' (maximals r x) :=
+  minimals_image_of_rel_iff_rel (fun _ _ a_1 a_2 ↦ hf a_2 a_1)
+
+theorem RelEmbedding.minimals_image_eq (f : r ↪r s) (x : Set α) :
+    minimals s (f '' x) = f '' (minimals r x) := by
+  rw [minimals_image_of_rel_iff_rel]; simp [f.map_rel_iff]
+
+theorem RelEmbedding.maximals_image_eq (f : r ↪r s) (x : Set α) :
+    maximals s (f '' x) = f '' (maximals r x) :=
+  (f.swap).minimals_image_eq x
+
+theorem inter_minimals_preimage_inter_eq_of_rel_iff_rel_on
+    (hf : ∀ ⦃a a'⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))) (y : Set β) :
+    x ∩ f ⁻¹' (minimals s ((f '' x) ∩ y)) = minimals r (x ∩ f ⁻¹' y) := by
+  ext a
+  simp only [minimals, mem_inter_iff, mem_image, and_imp, forall_exists_index,
+    forall_apply_eq_imp_iff₂, preimage_setOf_eq, mem_setOf_eq, mem_preimage]
+  exact ⟨fun ⟨hax,⟨_,hay⟩,h2⟩ ↦ ⟨⟨hax, hay⟩, fun a₁ ha₁ ha₁y ha₁a ↦
+          (hf hax ha₁).mpr (h2 _ ha₁ ha₁y ((hf ha₁ hax).mp ha₁a))⟩ ,
+        fun ⟨⟨hax,hay⟩,h⟩ ↦ ⟨hax, ⟨⟨_, hax, rfl⟩, hay⟩, fun a' ha' ha'y hsa' ↦
+          (hf hax ha').mp (h ha' ha'y ((hf ha' hax).mpr hsa'))⟩⟩
+
+theorem inter_preimage_minimals_eq_of_rel_iff_rel_on_of_subset
+    (hf : ∀ ⦃a a'⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))) (hy : y ⊆ f '' x) :
+    x ∩ f ⁻¹' (minimals s y) = minimals r (x ∩ f ⁻¹' y) := by
+  rw [←inter_eq_self_of_subset_right hy, inter_minimals_preimage_inter_eq_of_rel_iff_rel_on hf,
+    preimage_inter, ←inter_assoc, inter_eq_self_of_subset_left (subset_preimage_image f x)]
+
+theorem RelEmbedding.inter_preimage_minimals_eq (f : r ↪r s) (x : Set α) (y : Set β) :
+    x ∩ f⁻¹' (minimals s ((f '' x) ∩ y)) = minimals r (x ∩ f ⁻¹' y) :=
+  inter_minimals_preimage_inter_eq_of_rel_iff_rel_on (by simp [f.map_rel_iff]) y
+
+theorem RelEmbedding.inter_preimage_minimals_eq_of_subset (f : r ↪r s) (h : y ⊆ f '' x) :
+    x ∩ f ⁻¹' (minimals s y) = minimals r (x ∩ f ⁻¹' y) := by
+  rw [inter_preimage_minimals_eq_of_rel_iff_rel_on_of_subset _ h]; simp [f.map_rel_iff]
+
+theorem RelEmbedding.minimals_preimage_eq (f : r ↪r s) (y : Set β) :
+  minimals r (f ⁻¹' y) = f ⁻¹' minimals s (y ∩ range f) := by
+  convert (f.inter_preimage_minimals_eq univ y).symm; simp [univ_inter]; simp [inter_comm]
+
+theorem inter_maximals_preimage_inter_eq_of_rel_iff_rel_on
+    (hf : ∀ ⦃a a'⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))) (y : Set β) :
+    x ∩ f ⁻¹' (maximals s ((f '' x) ∩ y)) = maximals r (x ∩ f ⁻¹' y) := by
+  apply inter_minimals_preimage_inter_eq_of_rel_iff_rel_on
+  exact fun _ _ a b ↦ hf b a
+
+theorem inter_preimage_maximals_eq_of_rel_iff_rel_on_of_subset
+    (hf : ∀ ⦃a a'⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))) (hy : y ⊆ f '' x) :
+    x ∩ f ⁻¹' (maximals s y) = maximals r (x ∩ f ⁻¹' y) := by
+  apply inter_preimage_minimals_eq_of_rel_iff_rel_on_of_subset _ hy
+  exact fun _ _ a b ↦ hf b a
+
+theorem RelEmbedding.inter_preimage_maximals_eq (f : r ↪r s) (x : Set α) (y : Set β) :
+    x ∩ f⁻¹' (maximals s ((f '' x) ∩ y)) = maximals r (x ∩ f ⁻¹' y) :=
+  inter_minimals_preimage_inter_eq_of_rel_iff_rel_on (by simp [f.map_rel_iff]) y
+
+theorem RelEmbedding.inter_preimage_maximals_eq_of_subset (f : r ↪r s) (h : y ⊆ f '' x) :
+    x ∩ f ⁻¹' (maximals s y) = maximals r (x ∩ f ⁻¹' y) := by
+  rw [inter_preimage_maximals_eq_of_rel_iff_rel_on_of_subset _ h]; simp [f.map_rel_iff]
+
+theorem RelEmbedding.maximals_preimage_eq (f : r ↪r s) (y : Set β) :
+    maximals r (f ⁻¹' y) = f ⁻¹' maximals s (y ∩ range f) := by
+  convert (f.inter_preimage_maximals_eq univ y).symm; simp [univ_inter]; simp [inter_comm]
+
+end Image
+
+section Interval
+
+variable [PartialOrder α] {a b : α}
+
+@[simp] theorem maximals_Iic (a : α) : maximals (· ≤ ·) (Iic a) = {a} :=
+  Set.ext fun _ ↦ ⟨fun h ↦ h.1.antisymm (h.2 rfl.le h.1),
+    fun h ↦ ⟨h.trans_le rfl.le, fun _ hba _ ↦ le_trans hba h.symm.le⟩⟩
+
+@[simp] theorem minimals_Ici (a : α) : minimals (· ≤ ·) (Ici a) = {a} :=
+  maximals_Iic (α := αᵒᵈ) a
+
+theorem maximals_Icc (hab : a ≤ b) : maximals (· ≤ ·) (Icc a b) = {b} :=
+  Set.ext fun x ↦ ⟨fun h ↦ h.1.2.antisymm (h.2 ⟨hab, rfl.le⟩ h.1.2),
+    fun (h : x = b) ↦ ⟨⟨hab.trans_eq h.symm, h.le⟩, fun _ hy _ ↦ hy.2.trans_eq h.symm⟩⟩
+
+theorem minimals_Icc (hab : a ≤ b) : minimals (· ≤ ·) (Icc a b) = {a} := by
+  simp_rw [Icc, and_comm (a := (a ≤ _))]; exact maximals_Icc (α := αᵒᵈ) hab
+
+theorem maximals_Ioc (hab : a < b) : maximals (· ≤ ·) (Ioc a b) = {b} :=
+  Set.ext fun x ↦ ⟨fun h ↦ h.1.2.antisymm (h.2 ⟨hab, rfl.le⟩ h.1.2),
+    fun (h : x = b) ↦ ⟨⟨hab.trans_eq h.symm, h.le⟩, fun _ hy _ ↦ hy.2.trans_eq h.symm⟩⟩
+
+theorem minimals_Ico (hab : a < b) : minimals (· ≤ ·) (Ico a b) = {a} := by
+  simp_rw [Ico, and_comm (a := _ ≤ _)]; exact maximals_Ioc (α := αᵒᵈ) hab
+
+end Interval