chore(order/cover): split to reduce imports

src/algebra/parity.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
 import algebra.associated
+import algebra.order.field
 import algebra.field.power
 
 /-!  # Squares, even and odd elements

src/combinatorics/simple_graph/hasse.lean

@@ -6,6 +6,7 @@ Authors: Yaël Dillies
 import combinatorics.simple_graph.prod
 import data.fin.succ_pred
 import order.succ_pred.relation
+import order.cover.ord_connected
 
 /-!
 # The Hasse diagram as a graph

src/combinatorics/simple_graph/regularity/energy.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import algebra.big_operators.order
+import algebra.module.basic
 import combinatorics.simple_graph.density
 
 /-!

src/data/enat/basic.lean

@@ -6,6 +6,7 @@ Authors: Yury Kudryashov
 import data.nat.lattice
 import data.nat.succ_pred
 import algebra.order.sub.with_top
+import algebra.char_zero
 
 /-!
 # Definition and basic properties of extended natural numbers

src/data/fin/succ_pred.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 -/
 import order.succ_pred.basic
+import data.fin.basic
 
 /-!
 # Successors and predecessors of `fin n`

src/data/nat/succ_pred.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import order.succ_pred.basic
+import data.fin.basic
 
 /-!
 # Successors and predecessors of naturals

src/order/atoms.lean

@@ -5,9 +5,10 @@ Authors: Aaron Anderson
 -/
 
 import order.complete_boolean_algebra
-import order.cover
+import order.cover.basic
 import order.modular_lattice
 import data.fintype.basic
+import data.set.finite
 
 /-!
 # Atoms, Coatoms, and Simple Lattices

src/order/cover.lean → src/order/cover/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Violeta Hernández Palacios, Grayson Burton, Floris van Doorn
 -/
-import data.set.intervals.ord_connected
+
 import order.antisymmetrization
 
 /-!
@@ -74,28 +74,9 @@ by simp_rw [wcovby, h, true_and, not_forall, exists_prop, not_not]
 
 instance wcovby.is_refl : is_refl α (⩿) := ⟨wcovby.refl⟩
 
-lemma wcovby.Ioo_eq (h : a ⩿ b) : Ioo a b = ∅ :=
-eq_empty_iff_forall_not_mem.2 $ λ x hx, h.2 hx.1 hx.2
-
 lemma wcovby.of_image (f : α ↪o β) (h : f a ⩿ f b) : a ⩿ b :=
 ⟨f.le_iff_le.mp h.le, λ c hac hcb, h.2 (f.lt_iff_lt.mpr hac) (f.lt_iff_lt.mpr hcb)⟩
 
-lemma wcovby.image (f : α ↪o β) (hab : a ⩿ b) (h : (range f).ord_connected) : f a ⩿ f b :=
-begin
-  refine ⟨f.monotone hab.le, λ c ha hb, _⟩,
-  obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩,
-  rw f.lt_iff_lt at ha hb,
-  exact hab.2 ha hb,
-end
-
-lemma set.ord_connected.apply_wcovby_apply_iff (f : α ↪o β) (h : (range f).ord_connected) :
-  f a ⩿ f b ↔ a ⩿ b :=
-⟨λ h2, h2.of_image f, λ hab, hab.image f h⟩
-
-@[simp] lemma apply_wcovby_apply_iff {E : Type*} [order_iso_class E α β] (e : E) :
-  e a ⩿ e b ↔ a ⩿ b :=
-(ord_connected_range (e : α ≃o β)).apply_wcovby_apply_iff ((e : α ≃o β) : α ↪o β)
-
 @[simp] lemma to_dual_wcovby_to_dual_iff : to_dual b ⩿ to_dual a ↔ a ⩿ b :=
 and_congr_right' $ forall_congr $ λ c, forall_swap
 
@@ -127,15 +108,6 @@ begin
   refine ⟨λ h2, h.eq_or_eq h2.1 h2.2, _⟩, rintro (rfl|rfl), exacts [⟨le_rfl, h.le⟩, ⟨h.le, le_rfl⟩]
 end
 
-lemma wcovby.Icc_eq (h : a ⩿ b) : Icc a b = {a, b} :=
-by { ext c, exact h.le_and_le_iff }
-
-lemma wcovby.Ico_subset (h : a ⩿ b) : Ico a b ⊆ {a} :=
-by rw [← Icc_diff_right, h.Icc_eq, diff_singleton_subset_iff, pair_comm]
-
-lemma wcovby.Ioc_subset (h : a ⩿ b) : Ioc a b ⊆ {b} :=
-by rw [← Icc_diff_left, h.Icc_eq, diff_singleton_subset_iff]
-
 end partial_order
 
 section semilattice_sup
@@ -233,23 +205,9 @@ instance : is_nonstrict_strict_order α (⩿) (⋖) :=
 
 instance covby.is_irrefl : is_irrefl α (⋖) := ⟨λ a ha, ha.ne rfl⟩
 
-lemma covby.Ioo_eq (h : a ⋖ b) : Ioo a b = ∅ :=
-h.wcovby.Ioo_eq
-
 lemma covby.of_image (f : α ↪o β) (h : f a ⋖ f b) : a ⋖ b :=
 ⟨f.lt_iff_lt.mp h.lt, λ c hac hcb, h.2 (f.lt_iff_lt.mpr hac) (f.lt_iff_lt.mpr hcb)⟩
 
-lemma covby.image (f : α ↪o β) (hab : a ⋖ b) (h : (range f).ord_connected) : f a ⋖ f b :=
-(hab.wcovby.image f h).covby_of_lt $ f.strict_mono hab.lt
-
-lemma set.ord_connected.apply_covby_apply_iff (f : α ↪o β) (h : (range f).ord_connected) :
-  f a ⋖ f b ↔ a ⋖ b :=
-⟨covby.of_image f, λ hab, hab.image f h⟩
-
-@[simp] lemma apply_covby_apply_iff {E : Type*} [order_iso_class E α β] (e : E) :
-  e a ⋖ e b ↔ a ⋖ b :=
-(ord_connected_range (e : α ≃o β)).apply_covby_apply_iff ((e : α ≃o β) : α ↪o β)
-
 lemma covby_of_eq_or_eq (hab : a < b) (h : ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b) : a ⋖ b :=
 ⟨hab, λ c ha hb, (h c ha.le hb.le).elim ha.ne' hb.ne⟩
 
@@ -273,26 +231,12 @@ h.wcovby.eq_or_eq h2 h3
 lemma covby_iff_lt_and_eq_or_eq : a ⋖ b ↔ a < b ∧ ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b :=
 ⟨λ h, ⟨h.lt, λ c, h.eq_or_eq⟩, and.rec covby_of_eq_or_eq⟩
 
-lemma covby.Ico_eq (h : a ⋖ b) : Ico a b = {a} :=
-by rw [←Ioo_union_left h.lt, h.Ioo_eq, empty_union]
-
-lemma covby.Ioc_eq (h : a ⋖ b) : Ioc a b = {b} :=
-by rw [←Ioo_union_right h.lt, h.Ioo_eq, empty_union]
-
-lemma covby.Icc_eq (h : a ⋖ b) : Icc a b = {a, b} :=
-h.wcovby.Icc_eq
 
 end partial_order
 
 section linear_order
 variables [linear_order α] {a b c : α}
 
-lemma covby.Ioi_eq (h : a ⋖ b) : Ioi a = Ici b :=
-by rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union]
-
-lemma covby.Iio_eq (h : a ⋖ b) : Iio b = Iic a :=
-by rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]
-
 lemma wcovby.le_of_lt (hab : a ⩿ b) (hcb : c < b) : c ≤ a := not_lt.1 $ λ hac, hab.2 hac hcb
 lemma wcovby.ge_of_gt (hab : a ⩿ b) (hac : a < c) : b ≤ c := not_lt.1 $ hab.2 hac
 lemma covby.le_of_lt (hab : a ⋖ b) : c < b → c ≤ a := hab.wcovby.le_of_lt
@@ -330,12 +274,6 @@ end set
 namespace prod
 variables [partial_order α] [partial_order β] {a a₁ a₂ : α} {b b₁ b₂ : β} {x y : α × β}
 
-@[simp] lemma swap_wcovby_swap : x.swap ⩿ y.swap ↔ x ⩿ y :=
-apply_wcovby_apply_iff (order_iso.prod_comm : α × β ≃o β × α)
-
-@[simp] lemma swap_covby_swap : x.swap ⋖ y.swap ↔ x ⋖ y :=
-apply_covby_apply_iff (order_iso.prod_comm : α × β ≃o β × α)
-
 lemma fst_eq_or_snd_eq_of_wcovby : x ⩿ y → x.1 = y.1 ∨ x.2 = y.2 :=
 begin
   refine λ h, of_not_not (λ hab, _),
@@ -358,41 +296,4 @@ begin
   exact h h₁ h₂,
 end
 
-lemma mk_wcovby_mk_iff_right : (a, b₁) ⩿ (a, b₂) ↔ b₁ ⩿ b₂ :=
-swap_wcovby_swap.trans mk_wcovby_mk_iff_left
-
-lemma mk_covby_mk_iff_left : (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂ :=
-by simp_rw [covby_iff_wcovby_and_lt, mk_wcovby_mk_iff_left, mk_lt_mk_iff_left]
-
-lemma mk_covby_mk_iff_right : (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂ :=
-by simp_rw [covby_iff_wcovby_and_lt, mk_wcovby_mk_iff_right, mk_lt_mk_iff_right]
-
-lemma mk_wcovby_mk_iff : (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ :=
-begin
-  refine ⟨λ h, _, _⟩,
-  { obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovby h,
-    { exact or.inr ⟨mk_wcovby_mk_iff_right.1 h, rfl⟩ },
-    { exact or.inl ⟨mk_wcovby_mk_iff_left.1 h, rfl⟩ } },
-  { rintro (⟨h, rfl⟩ | ⟨h, rfl⟩),
-    { exact mk_wcovby_mk_iff_left.2 h },
-    { exact mk_wcovby_mk_iff_right.2 h } }
-end
-
-lemma mk_covby_mk_iff : (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ :=
-begin
-  refine ⟨λ h, _, _⟩,
-  { obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovby h.wcovby,
-    { exact or.inr ⟨mk_covby_mk_iff_right.1 h, rfl⟩ },
-    { exact or.inl ⟨mk_covby_mk_iff_left.1 h, rfl⟩ } },
-  { rintro (⟨h, rfl⟩ | ⟨h, rfl⟩),
-    { exact mk_covby_mk_iff_left.2 h },
-    { exact mk_covby_mk_iff_right.2 h } }
-end
-
-lemma wcovby_iff : x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1 :=
-by { cases x, cases y, exact mk_wcovby_mk_iff }
-
-lemma covby_iff : x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1 :=
-by { cases x, cases y, exact mk_covby_mk_iff }
-
 end prod

src/order/cover/ord_connected.lean

@@ -0,0 +1,149 @@
+/-
+Copyright (c) 2021 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Violeta Hernández Palacios, Grayson Burton, Floris van Doorn
+-/
+import order.cover.basic
+import data.set.intervals.ord_connected
+
+/-!
+# Lemmas about the order covering relation and order connected sets.
+-/
+
+open set order_dual
+
+variables {α β : Type*}
+
+section weakly_covers
+
+section preorder
+variables [preorder α] [preorder β] {a b c : α}
+
+lemma wcovby.Ioo_eq (h : a ⩿ b) : Ioo a b = ∅ :=
+eq_empty_iff_forall_not_mem.2 $ λ x hx, h.2 hx.1 hx.2
+
+lemma wcovby.image (f : α ↪o β) (hab : a ⩿ b) (h : (range f).ord_connected) : f a ⩿ f b :=
+begin
+  refine ⟨f.monotone hab.le, λ c ha hb, _⟩,
+  obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩,
+  rw f.lt_iff_lt at ha hb,
+  exact hab.2 ha hb,
+end
+
+lemma set.ord_connected.apply_wcovby_apply_iff (f : α ↪o β) (h : (range f).ord_connected) :
+  f a ⩿ f b ↔ a ⩿ b :=
+⟨λ h2, h2.of_image f, λ hab, hab.image f h⟩
+
+@[simp] lemma apply_wcovby_apply_iff {E : Type*} [order_iso_class E α β] (e : E) :
+  e a ⩿ e b ↔ a ⩿ b :=
+(ord_connected_range (e : α ≃o β)).apply_wcovby_apply_iff ((e : α ≃o β) : α ↪o β)
+
+end preorder
+
+section partial_order
+variables [partial_order α] {a b c : α}
+
+lemma wcovby.Icc_eq (h : a ⩿ b) : Icc a b = {a, b} :=
+by { ext c, exact h.le_and_le_iff }
+
+lemma wcovby.Ico_subset (h : a ⩿ b) : Ico a b ⊆ {a} :=
+by rw [← Icc_diff_right, h.Icc_eq, diff_singleton_subset_iff, pair_comm]
+
+lemma wcovby.Ioc_subset (h : a ⩿ b) : Ioc a b ⊆ {b} :=
+by rw [← Icc_diff_left, h.Icc_eq, diff_singleton_subset_iff]
+
+end partial_order
+
+end weakly_covers
+
+section preorder
+variables [preorder α] [preorder β] {a b c : α}
+
+lemma covby.Ioo_eq (h : a ⋖ b) : Ioo a b = ∅ :=
+h.wcovby.Ioo_eq
+
+lemma covby.image (f : α ↪o β) (hab : a ⋖ b) (h : (range f).ord_connected) : f a ⋖ f b :=
+(hab.wcovby.image f h).covby_of_lt $ f.strict_mono hab.lt
+
+lemma set.ord_connected.apply_covby_apply_iff (f : α ↪o β) (h : (range f).ord_connected) :
+  f a ⋖ f b ↔ a ⋖ b :=
+⟨covby.of_image f, λ hab, hab.image f h⟩
+
+@[simp] lemma apply_covby_apply_iff {E : Type*} [order_iso_class E α β] (e : E) :
+  e a ⋖ e b ↔ a ⋖ b :=
+(ord_connected_range (e : α ≃o β)).apply_covby_apply_iff ((e : α ≃o β) : α ↪o β)
+
+end preorder
+
+section partial_order
+variables [partial_order α] {a b c : α}
+
+lemma covby.Ico_eq (h : a ⋖ b) : Ico a b = {a} :=
+by rw [←Ioo_union_left h.lt, h.Ioo_eq, empty_union]
+
+lemma covby.Ioc_eq (h : a ⋖ b) : Ioc a b = {b} :=
+by rw [←Ioo_union_right h.lt, h.Ioo_eq, empty_union]
+
+lemma covby.Icc_eq (h : a ⋖ b) : Icc a b = {a, b} :=
+h.wcovby.Icc_eq
+
+end partial_order
+
+section linear_order
+variables [linear_order α] {a b c : α}
+
+lemma covby.Ioi_eq (h : a ⋖ b) : Ioi a = Ici b :=
+by rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union]
+
+lemma covby.Iio_eq (h : a ⋖ b) : Iio b = Iic a :=
+by rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]
+
+end linear_order
+
+namespace prod
+variables [partial_order α] [partial_order β] {a a₁ a₂ : α} {b b₁ b₂ : β} {x y : α × β}
+
+@[simp] lemma swap_wcovby_swap : x.swap ⩿ y.swap ↔ x ⩿ y :=
+apply_wcovby_apply_iff (order_iso.prod_comm : α × β ≃o β × α)
+
+@[simp] lemma swap_covby_swap : x.swap ⋖ y.swap ↔ x ⋖ y :=
+apply_covby_apply_iff (order_iso.prod_comm : α × β ≃o β × α)
+
+lemma mk_wcovby_mk_iff_right : (a, b₁) ⩿ (a, b₂) ↔ b₁ ⩿ b₂ :=
+swap_wcovby_swap.trans mk_wcovby_mk_iff_left
+
+lemma mk_covby_mk_iff_left : (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂ :=
+by simp_rw [covby_iff_wcovby_and_lt, mk_wcovby_mk_iff_left, mk_lt_mk_iff_left]
+
+lemma mk_covby_mk_iff_right : (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂ :=
+by simp_rw [covby_iff_wcovby_and_lt, mk_wcovby_mk_iff_right, mk_lt_mk_iff_right]
+
+lemma mk_wcovby_mk_iff : (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ :=
+begin
+  refine ⟨λ h, _, _⟩,
+  { obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovby h,
+    { exact or.inr ⟨mk_wcovby_mk_iff_right.1 h, rfl⟩ },
+    { exact or.inl ⟨mk_wcovby_mk_iff_left.1 h, rfl⟩ } },
+  { rintro (⟨h, rfl⟩ | ⟨h, rfl⟩),
+    { exact mk_wcovby_mk_iff_left.2 h },
+    { exact mk_wcovby_mk_iff_right.2 h } }
+end
+
+lemma mk_covby_mk_iff : (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ :=
+begin
+  refine ⟨λ h, _, _⟩,
+  { obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovby h.wcovby,
+    { exact or.inr ⟨mk_covby_mk_iff_right.1 h, rfl⟩ },
+    { exact or.inl ⟨mk_covby_mk_iff_left.1 h, rfl⟩ } },
+  { rintro (⟨h, rfl⟩ | ⟨h, rfl⟩),
+    { exact mk_covby_mk_iff_left.2 h },
+    { exact mk_covby_mk_iff_right.2 h } }
+end
+
+lemma wcovby_iff : x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1 :=
+by { cases x, cases y, exact mk_wcovby_mk_iff }
+
+lemma covby_iff : x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1 :=
+by { cases x, cases y, exact mk_covby_mk_iff }
+
+end prod

src/order/modular_lattice.lean

@@ -3,7 +3,8 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Yaël Dillies
 -/
-import order.cover
+import order.cover.basic
+import order.galois_connection
 import order.lattice_intervals
 
 /-!

src/order/succ_pred/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import order.complete_lattice
-import order.cover
+import order.cover.basic
 import order.iterate
 import tactic.monotonicity
 

src/order/succ_pred/interval_succ.lean

@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import order.succ_pred.basic
 import data.set.lattice
+import data.set.pairwise
 
 /-!
 # Intervals `Ixx (f x) (f (order.succ x))`