feat(Order): maximal chains are preserved under order isomorphisms (#19471)

From LeanCamCombi

Author: YaelDillies

Mathlib/Order/Chain.lean

@@ -52,10 +52,12 @@ def SuperChain (s t : Set α) : Prop :=
 def IsMaxChain (s : Set α) : Prop :=
   IsChain r s ∧ ∀ ⦃t⦄, IsChain r t → s ⊆ t → s = t
 
-variable {r} {c c₁ c₂ s t : Set α} {a x y : α}
+variable {r} {c c₁ c₂ s t : Set α} {a b x y : α}
 
-theorem isChain_empty : IsChain r ∅ :=
-  Set.pairwise_empty _
+@[simp] lemma IsChain.empty : IsChain r ∅ := pairwise_empty _
+@[simp] lemma IsChain.singleton : IsChain r {a} := pairwise_singleton ..
+
+@[deprecated (since := "2024-11-25")] alias isChain_empty := IsChain.empty
 
 theorem Set.Subsingleton.isChain (hs : s.Subsingleton) : IsChain r s :=
   hs.pairwise _
@@ -78,6 +80,9 @@ protected theorem IsChain.insert (hs : IsChain r s) (ha : ∀ b ∈ s, a ≠ b 
     IsChain r (insert a s) :=
   hs.insert_of_symmetric (fun _ _ => Or.symm) ha
 
+lemma IsChain.pair (h : r a b) : IsChain r {a, b} :=
+  IsChain.singleton.insert fun _ hb _ ↦ .inl <| (eq_of_mem_singleton hb).symm.recOn ‹_›
+
 theorem isChain_univ_iff : IsChain r (univ : Set α) ↔ IsTrichotomous α r := by
   refine ⟨fun h => ⟨fun a b => ?_⟩, fun h => @isChain_of_trichotomous _ _ h univ⟩
   rw [or_left_comm, or_iff_not_imp_left]
@@ -136,6 +141,14 @@ theorem IsMaxChain.bot_mem [LE α] [OrderBot α] (h : IsMaxChain (· ≤ ·) s)
 theorem IsMaxChain.top_mem [LE α] [OrderTop α] (h : IsMaxChain (· ≤ ·) s) : ⊤ ∈ s :=
   (h.2 (h.1.insert fun _ _ _ => Or.inr le_top) <| subset_insert _ _).symm ▸ mem_insert _ _
 
+lemma IsMaxChain.image {s : β → β → Prop} (e : r ≃r s) {c : Set α} (hc : IsMaxChain r c) :
+    IsMaxChain s (e '' c) where
+  left := hc.isChain.image _ _ _ fun _ _ ↦ by exact e.map_rel_iff.2
+  right t ht hf := by
+    rw [← e.coe_fn_toEquiv, ← e.toEquiv.eq_preimage_iff_image_eq, preimage_equiv_eq_image_symm]
+    exact hc.2 (ht.image _ _ _ fun _ _ ↦ by exact e.symm.map_rel_iff.2)
+      ((e.toEquiv.subset_symm_image _ _).2 hf)
+
 open Classical in
 /-- Given a set `s`, if there exists a chain `t` strictly including `s`, then `SuccChain s`
 is one of these chains. Otherwise it is `s`. -/
@@ -302,11 +315,17 @@ theorem top_mem [OrderTop α] (s : Flag α) : (⊤ : α) ∈ s :=
 theorem bot_mem [OrderBot α] (s : Flag α) : (⊥ : α) ∈ s :=
   s.maxChain.bot_mem
 
+/-- Reinterpret a maximal chain as a flag. -/
+def ofIsMaxChain (c : Set α) (hc : IsMaxChain (· ≤ ·) c) : Flag α := ⟨c, hc.isChain, hc.2⟩
+
+@[simp, norm_cast]
+lemma coe_ofIsMaxChain (c : Set α) (hc) : ofIsMaxChain c hc = c := rfl
+
 end LE
 
 section Preorder
 
-variable [Preorder α] {a b : α}
+variable [Preorder α] [Preorder β] {a b : α} {s : Flag α}
 
 protected theorem le_or_le (s : Flag α) (ha : a ∈ s) (hb : b ∈ s) : a ≤ b ∨ b ≤ a :=
   s.chain_le.total ha hb
@@ -320,6 +339,24 @@ instance [OrderBot α] (s : Flag α) : OrderBot s :=
 instance [BoundedOrder α] (s : Flag α) : BoundedOrder s :=
   Subtype.boundedOrder s.bot_mem s.top_mem
 
+lemma mem_iff_forall_le_or_ge : a ∈ s ↔ ∀ ⦃b⦄, b ∈ s → a ≤ b ∨ b ≤ a :=
+  ⟨fun ha b => s.le_or_le ha, fun hb =>
+    of_not_not fun ha =>
+      Set.ne_insert_of_not_mem _ ‹_› <|
+        s.maxChain.2 (s.chain_le.insert fun c hc _ => hb hc) <| Set.subset_insert _ _⟩
+
+/-- Flags are preserved under order isomorphisms. -/
+def map (e : α ≃o β) : Flag α ≃ Flag β
+    where
+  toFun s := ofIsMaxChain _ (s.maxChain.image e)
+  invFun s := ofIsMaxChain _ (s.maxChain.image e.symm)
+  left_inv s := ext <| e.symm_image_image s
+  right_inv s := ext <| e.image_symm_image s
+
+@[simp, norm_cast] lemma coe_map (e : α ≃o β) (s : Flag α) : ↑(map e s) = e '' s := rfl
+
+@[simp] lemma symm_map (e : α ≃o β) : (map e).symm = map e.symm := rfl
+
 end Preorder
 
 section PartialOrder