feat: The lexicographic sum of two locally finite orders is locally f…

…inite (#6340)

Forward-ports leanprover-community/mathlib#11352




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Data/Finset/Sum.lean

@@ -6,7 +6,7 @@ Authors: Yaël Dillies
 import Mathlib.Data.Multiset.Sum
 import Mathlib.Data.Finset.Card
 
-#align_import data.finset.sum from "leanprover-community/mathlib"@"9003f28797c0664a49e4179487267c494477d853"
+#align_import data.finset.sum from "leanprover-community/mathlib"@"48a058d7e39a80ed56858505719a0b2197900999"
 
 /-!
 # Disjoint sum of finsets
@@ -79,6 +79,10 @@ theorem inr_mem_disjSum : inr b ∈ s.disjSum t ↔ b ∈ t :=
   Multiset.inr_mem_disjSum
 #align finset.inr_mem_disj_sum Finset.inr_mem_disjSum
 
+@[simp]
+theorem disjSum_eq_empty : s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅ := by simp [ext_iff]
+#align finset.disj_sum_eq_empty Finset.disjSum_eq_empty
+
 theorem disjSum_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁.disjSum t₁ ⊆ s₂.disjSum t₂ :=
   val_le_iff.1 <| Multiset.disjSum_mono (val_le_iff.2 hs) (val_le_iff.2 ht)
 #align finset.disj_sum_mono Finset.disjSum_mono

Mathlib/Data/Sum/Interval.lean

@@ -3,19 +3,17 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import Mathlib.Data.Finset.Sum
 import Mathlib.Data.Sum.Order
 import Mathlib.Order.LocallyFinite
 
-#align_import data.sum.interval from "leanprover-community/mathlib"@"861a26926586cd46ff80264d121cdb6fa0e35cc1"
+#align_import data.sum.interval from "leanprover-community/mathlib"@"48a058d7e39a80ed56858505719a0b2197900999"
 
 /-!
 # Finite intervals in a disjoint union
 
-This file provides the `LocallyFiniteOrder` instance for the disjoint sum of two orders.
-
-## TODO
-
-Do the same for the lexicographic sum of orders.
+This file provides the `LocallyFiniteOrder` instance for the disjoint sum and linear sum of two
+orders and calculates the cardinality of their finite intervals.
 -/
 
 
@@ -107,6 +105,118 @@ theorem sumLift₂_mono (h₁ : ∀ a b, f₁ a b ⊆ g₁ a b) (h₂ : ∀ a b,
 
 end SumLift₂
 
+section SumLexLift
+variable (f₁ f₁' : α₁ → β₁ → Finset γ₁) (f₂ f₂' : α₂ → β₂ → Finset γ₂)
+  (g₁ g₁' : α₁ → β₂ → Finset γ₁) (g₂ g₂' : α₁ → β₂ → Finset γ₂)
+
+/-- Lifts maps `α₁ → β₁ → Finset γ₁`, `α₂ → β₂ → Finset γ₂`, `α₁ → β₂ → Finset γ₁`,
+`α₂ → β₂ → Finset γ₂`  to a map `α₁ ⊕ α₂ → β₁ ⊕ β₂ → Finset (γ₁ ⊕ γ₂)`. Could be generalized to
+alternative monads if we can make sure to keep computability and universe polymorphism. -/
+def sumLexLift : Sum α₁ α₂ → Sum β₁ β₂ → Finset (Sum γ₁ γ₂)
+  | inl a, inl b => (f₁ a b).map Embedding.inl
+  | inl a, inr b => (g₁ a b).disjSum (g₂ a b)
+  | inr _, inl _ => ∅
+  | inr a, inr b => (f₂ a b).map ⟨_, inr_injective⟩
+#align finset.sum_lex_lift Finset.sumLexLift
+
+@[simp]
+lemma sumLexLift_inl_inl (a : α₁) (b : β₁) :
+    sumLexLift f₁ f₂ g₁ g₂ (inl a) (inl b) = (f₁ a b).map Embedding.inl := rfl
+#align finset.sum_lex_lift_inl_inl Finset.sumLexLift_inl_inl
+
+@[simp]
+lemma sumLexLift_inl_inr (a : α₁) (b : β₂) :
+    sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b) = (g₁ a b).disjSum (g₂ a b) := rfl
+#align finset.sum_lex_lift_inl_inr Finset.sumLexLift_inl_inr
+
+@[simp]
+lemma sumLexLift_inr_inl (a : α₂) (b : β₁) : sumLexLift f₁ f₂ g₁ g₂ (inr a) (inl b) = ∅ := rfl
+#align finset.sum_lex_lift_inr_inl Finset.sumLexLift_inr_inl
+
+@[simp]
+lemma sumLexLift_inr_inr (a : α₂) (b : β₂) :
+    sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b) = (f₂ a b).map ⟨_, inr_injective⟩ := rfl
+#align finset.sum_lex_lift_inr_inr Finset.sumLexLift_inr_inr
+
+variable {f₁ g₁ f₂ g₂ f₁' g₁' f₂' g₂'} {a : Sum α₁ α₂} {b : Sum β₁ β₂} {c : Sum γ₁ γ₂}
+
+lemma mem_sumLexLift :
+    c ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
+      (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
+        (∃ a₁ b₂ c₁, a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
+          (∃ a₁ b₂ c₂, a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
+            ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂ := by
+  constructor
+  · obtain a | a := a <;> obtain b | b :=  b
+    · rw [sumLexLift, mem_map]
+      rintro ⟨c, hc, rfl⟩
+      exact Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩
+    · refine' fun h ↦ (mem_disjSum.1 h).elim _ _
+      · rintro ⟨c, hc, rfl⟩
+        exact Or.inr (Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩)
+      · rintro ⟨c, hc, rfl⟩
+        exact Or.inr (Or.inr $ Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩)
+    · exact fun h ↦ (not_mem_empty _ h).elim
+    · rw [sumLexLift, mem_map]
+      rintro ⟨c, hc, rfl⟩
+      exact Or.inr (Or.inr $ Or.inr $ ⟨a, b, c, rfl, rfl, rfl, hc⟩)
+  · rintro (⟨a, b, c, rfl, rfl, rfl, hc⟩ | ⟨a, b, c, rfl, rfl, rfl, hc⟩ |
+      ⟨a, b, c, rfl, rfl, rfl, hc⟩ | ⟨a, b, c, rfl, rfl, rfl, hc⟩)
+    · exact mem_map_of_mem _ hc
+    · exact inl_mem_disjSum.2 hc
+    · exact inr_mem_disjSum.2 hc
+    · exact mem_map_of_mem _ hc
+#align finset.mem_sum_lex_lift Finset.mem_sumLexLift
+
+lemma inl_mem_sumLexLift {c₁ : γ₁} :
+    inl c₁ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
+      (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
+        ∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₁ ∈ g₁ a₁ b₂ := by
+  simp [mem_sumLexLift]
+#align finset.inl_mem_sum_lex_lift Finset.inl_mem_sumLexLift
+
+lemma inr_mem_sumLexLift {c₂ : γ₂} :
+    inr c₂ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
+      (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
+        ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ f₂ a₂ b₂ := by
+  simp [mem_sumLexLift]
+#align finset.inr_mem_sum_lex_lift Finset.inr_mem_sumLexLift
+
+lemma sumLexLift_mono (hf₁ : ∀ a b, f₁ a b ⊆ f₁' a b) (hf₂ : ∀ a b, f₂ a b ⊆ f₂' a b)
+    (hg₁ : ∀ a b, g₁ a b ⊆ g₁' a b) (hg₂ : ∀ a b, g₂ a b ⊆ g₂' a b) (a : Sum α₁ α₂)
+    (b : Sum β₁ β₂) : sumLexLift f₁ f₂ g₁ g₂ a b ⊆ sumLexLift f₁' f₂' g₁' g₂' a b := by
+  cases a <;> cases b
+  exacts [map_subset_map.2 (hf₁ _ _), disjSum_mono (hg₁ _ _) (hg₂ _ _), Subset.rfl,
+    map_subset_map.2 (hf₂ _ _)]
+#align finset.sum_lex_lift_mono Finset.sumLexLift_mono
+
+lemma sumLexLift_eq_empty :
+    sumLexLift f₁ f₂ g₁ g₂ a b = ∅ ↔
+      (∀ a₁ b₁, a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
+        (∀ a₁ b₂, a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
+          ∀ a₂ b₂, a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅ := by
+  refine' ⟨fun h ↦ ⟨_, _, _⟩, fun h ↦ _⟩
+  any_goals rintro a b rfl rfl; exact map_eq_empty.1 h
+  · rintro a b rfl rfl; exact disjSum_eq_empty.1 h
+  cases a <;> cases b
+  · exact map_eq_empty.2 (h.1 _ _ rfl rfl)
+  · simp [h.2.1 _ _ rfl rfl]
+  · rfl
+  · exact map_eq_empty.2 (h.2.2 _ _ rfl rfl)
+#align finset.sum_lex_lift_eq_empty Finset.sumLexLift_eq_empty
+
+lemma sumLexLift_nonempty :
+    (sumLexLift f₁ f₂ g₁ g₂ a b).Nonempty ↔
+      (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f₁ a₁ b₁).Nonempty) ∨
+        (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ ((g₁ a₁ b₂).Nonempty ∨ (g₂ a₁ b₂).Nonempty)) ∨
+          ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (f₂ a₂ b₂).Nonempty := by
+  -- porting note: was `simp [nonempty_iff_ne_empty, sumLexLift_eq_empty, not_and_or]`. Could
+  -- add `-exists_and_left, -not_and, -exists_and_right` but easier to squeeze.
+  simp only [nonempty_iff_ne_empty, Ne.def, sumLexLift_eq_empty, not_and_or, exists_prop,
+    not_forall]
+#align finset.sum_lex_lift_nonempty Finset.sumLexLift_nonempty
+
+end SumLexLift
 end Finset
 
 open Finset Function
@@ -209,4 +319,115 @@ theorem Ioo_inr_inr : Ioo (inr b₁ : Sum α β) (inr b₂) = (Ioo b₁ b₂).ma
 
 end Disjoint
 
+/-! ### Lexicographical sum of orders -/
+
+namespace Lex
+variable [Preorder α] [Preorder β] [OrderTop α] [OrderBot β] [LocallyFiniteOrder α]
+  [LocallyFiniteOrder β]
+
+/-- Throwaway tactic. -/
+local elab "simp_lex" : tactic => do
+  Lean.Elab.Tactic.evalTactic <| ← `(tactic|
+    refine toLex.surjective.forall₃.2 ?_;
+    rintro (a | a) (b | b) (c | c) <;> simp only
+      [sumLexLift_inl_inl, sumLexLift_inl_inr, sumLexLift_inr_inl, sumLexLift_inr_inr,
+        inl_le_inl_iff, inl_le_inr, not_inr_le_inl, inr_le_inr_iff, inl_lt_inl_iff, inl_lt_inr,
+        not_inr_lt_inl, inr_lt_inr_iff, mem_Icc, mem_Ico, mem_Ioc, mem_Ioo, mem_Ici, mem_Ioi,
+        mem_Iic, mem_Iio, Equiv.coe_toEmbedding, toLex_inj, exists_false, and_false, false_and,
+        map_empty, not_mem_empty, true_and, inl_mem_disjSum, inr_mem_disjSum, and_true, ofLex_toLex,
+        mem_map, Embedding.coeFn_mk, exists_prop, exists_eq_right, Embedding.inl_apply,
+        -- porting note: added
+        inl.injEq, inr.injEq]
+  )
+
+instance locallyFiniteOrder : LocallyFiniteOrder (α ⊕ₗ β) where
+  finsetIcc a b :=
+    (sumLexLift Icc Icc (fun a _ => Ici a) (fun _ => Iic) (ofLex a) (ofLex b)).map toLex.toEmbedding
+  finsetIco a b :=
+    (sumLexLift Ico Ico (fun a _ => Ici a) (fun _ => Iio) (ofLex a) (ofLex b)).map toLex.toEmbedding
+  finsetIoc a b :=
+    (sumLexLift Ioc Ioc (fun a _ => Ioi a) (fun _ => Iic) (ofLex a) (ofLex b)).map toLex.toEmbedding
+  finsetIoo a b :=
+    (sumLexLift Ioo Ioo (fun a _ => Ioi a) (fun _ => Iio) (ofLex a) (ofLex b)).map toLex.toEmbedding
+  finset_mem_Icc := by simp_lex
+  finset_mem_Ico := by simp_lex
+  finset_mem_Ioc := by simp_lex
+  finset_mem_Ioo := by simp_lex
+#align sum.lex.locally_finite_order Sum.Lex.locallyFiniteOrder
+
+variable (a a₁ a₂ : α) (b b₁ b₂ : β)
+
+lemma Icc_inl_inl :
+    Icc (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Icc a₁ a₂).map (Embedding.inl.trans toLex.toEmbedding) := by
+  rw [← Finset.map_map]; rfl
+#align sum.lex.Icc_inl_inl Sum.Lex.Icc_inl_inl
+
+lemma Ico_inl_inl :
+    Ico (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Ico a₁ a₂).map (Embedding.inl.trans toLex.toEmbedding) := by
+  rw [← Finset.map_map]; rfl
+#align sum.lex.Ico_inl_inl Sum.Lex.Ico_inl_inl
+
+lemma Ioc_inl_inl :
+    Ioc (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Ioc a₁ a₂).map (Embedding.inl.trans toLex.toEmbedding) := by
+  rw [← Finset.map_map]; rfl
+#align sum.lex.Ioc_inl_inl Sum.Lex.Ioc_inl_inl
+
+lemma Ioo_inl_inl :
+    Ioo (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Ioo a₁ a₂).map (Embedding.inl.trans toLex.toEmbedding) := by
+  rw [← Finset.map_map]; rfl
+#align sum.lex.Ioo_inl_inl Sum.Lex.Ioo_inl_inl
+
+@[simp]
+lemma Icc_inl_inr : Icc (inlₗ a) (inrₗ b) = ((Ici a).disjSum (Iic b)).map toLex.toEmbedding := rfl
+#align sum.lex.Icc_inl_inr Sum.Lex.Icc_inl_inr
+
+@[simp]
+lemma Ico_inl_inr : Ico (inlₗ a) (inrₗ b) = ((Ici a).disjSum (Iio b)).map toLex.toEmbedding := rfl
+#align sum.lex.Ico_inl_inr Sum.Lex.Ico_inl_inr
+
+@[simp]
+lemma Ioc_inl_inr : Ioc (inlₗ a) (inrₗ b) = ((Ioi a).disjSum (Iic b)).map toLex.toEmbedding := rfl
+#align sum.lex.Ioc_inl_inr Sum.Lex.Ioc_inl_inr
+
+@[simp]
+lemma Ioo_inl_inr : Ioo (inlₗ a) (inrₗ b) = ((Ioi a).disjSum (Iio b)).map toLex.toEmbedding := rfl
+#align sum.lex.Ioo_inl_inr Sum.Lex.Ioo_inl_inr
+
+@[simp, nolint simpNF] -- Porting note: dsimp cannot prove this
+lemma Icc_inr_inl : Icc (inrₗ b) (inlₗ a) = ∅ := rfl
+#align sum.lex.Icc_inr_inl Sum.Lex.Icc_inr_inl
+
+@[simp, nolint simpNF] -- Porting note: dsimp cannot prove this
+lemma Ico_inr_inl : Ico (inrₗ b) (inlₗ a) = ∅ := rfl
+#align sum.lex.Ico_inr_inl Sum.Lex.Ico_inr_inl
+
+@[simp, nolint simpNF] -- Porting note: dsimp cannot prove this
+lemma Ioc_inr_inl : Ioc (inrₗ b) (inlₗ a) = ∅ := rfl
+#align sum.lex.Ioc_inr_inl Sum.Lex.Ioc_inr_inl
+
+@[simp, nolint simpNF] -- Porting note: dsimp cannot prove this
+lemma Ioo_inr_inl : Ioo (inrₗ b) (inlₗ a) = ∅ := rfl
+#align sum.lex.Ioo_inr_inl Sum.Lex.Ioo_inr_inl
+
+lemma Icc_inr_inr :
+    Icc (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Icc b₁ b₂).map (Embedding.inr.trans toLex.toEmbedding) := by
+  rw [← Finset.map_map]; rfl
+#align sum.lex.Icc_inr_inr Sum.Lex.Icc_inr_inr
+
+lemma Ico_inr_inr :
+    Ico (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Ico b₁ b₂).map (Embedding.inr.trans toLex.toEmbedding) := by
+  rw [← Finset.map_map]; rfl
+#align sum.lex.Ico_inr_inr Sum.Lex.Ico_inr_inr
+
+lemma Ioc_inr_inr :
+    Ioc (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Ioc b₁ b₂).map (Embedding.inr.trans toLex.toEmbedding) := by
+  rw [← Finset.map_map]; rfl
+#align sum.lex.Ioc_inr_inr Sum.Lex.Ioc_inr_inr
+
+lemma Ioo_inr_inr :
+    Ioo (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Ioo b₁ b₂).map (Embedding.inr.trans toLex.toEmbedding) := by
+  rw [← Finset.map_map]; rfl
+#align sum.lex.Ioo_inr_inr Sum.Lex.Ioo_inr_inr
+
+end Lex
 end Sum