chore({data/finset,data/multiset,order}/locally_finite): Better line …

…wraps (#10087)

src/data/finset/locally_finite.lean

@@ -54,28 +54,16 @@ alias Ioc_eq_empty_iff ↔ _ finset.Ioc_eq_empty
 @[simp] lemma Ioo_eq_empty (h : ¬a < b) : Ioo a b = ∅ :=
 eq_empty_iff_forall_not_mem.2 $ λ x hx, h ((mem_Ioo.1 hx).1.trans (mem_Ioo.1 hx).2)
 
-@[simp] lemma Icc_eq_empty_of_lt (h : b < a) : Icc a b = ∅ :=
-Icc_eq_empty h.not_le
-
-@[simp] lemma Ico_eq_empty_of_le (h : b ≤ a) : Ico a b = ∅ :=
-Ico_eq_empty h.not_lt
-
-@[simp] lemma Ioc_eq_empty_of_le (h : b ≤ a) : Ioc a b = ∅ :=
-Ioc_eq_empty h.not_lt
-
-@[simp] lemma Ioo_eq_empty_of_le (h : b ≤ a) : Ioo a b = ∅ :=
-Ioo_eq_empty h.not_lt
+@[simp] lemma Icc_eq_empty_of_lt (h : b < a) : Icc a b = ∅ := Icc_eq_empty h.not_le
+@[simp] lemma Ico_eq_empty_of_le (h : b ≤ a) : Ico a b = ∅ := Ico_eq_empty h.not_lt
+@[simp] lemma Ioc_eq_empty_of_le (h : b ≤ a) : Ioc a b = ∅ := Ioc_eq_empty h.not_lt
+@[simp] lemma Ioo_eq_empty_of_le (h : b ≤ a) : Ioo a b = ∅ := Ioo_eq_empty h.not_lt
 
 variables (a)
 
-@[simp] lemma Ico_self : Ico a a = ∅ :=
-by rw [←coe_eq_empty, coe_Ico, set.Ico_self]
-
-@[simp] lemma Ioc_self : Ioc a a = ∅ :=
-by rw [←coe_eq_empty, coe_Ioc, set.Ioc_self]
-
-@[simp] lemma Ioo_self : Ioo a a = ∅ :=
-by rw [←coe_eq_empty, coe_Ioo, set.Ioo_self]
+@[simp] lemma Ico_self : Ico a a = ∅ := by rw [←coe_eq_empty, coe_Ico, set.Ico_self]
+@[simp] lemma Ioc_self : Ioc a a = ∅ := by rw [←coe_eq_empty, coe_Ioc, set.Ioc_self]
+@[simp] lemma Ioo_self : Ioo a a = ∅ := by rw [←coe_eq_empty, coe_Ioo, set.Ioo_self]
 
 @[simp] lemma right_not_mem_Ico {a b : α} : b ∉ Ico a b :=
 by { rw [mem_Ico, not_and], exact λ _, lt_irrefl _ }
@@ -126,8 +114,7 @@ end preorder
 section partial_order
 variables [partial_order α] [locally_finite_order α] {a b : α}
 
-@[simp] lemma Icc_self (a : α) : Icc a a = {a} :=
-by rw [←coe_eq_singleton, coe_Icc, set.Icc_self]
+@[simp] lemma Icc_self (a : α) : Icc a a = {a} := by rw [←coe_eq_singleton, coe_Icc, set.Icc_self]
 
 lemma Ico_insert_right [decidable_eq α] (h : a ≤ b) : insert b (Ico a b) = Icc a b :=
 by rw [←coe_inj, coe_insert, coe_Icc, coe_Ico, set.insert_eq, set.union_comm, set.Ico_union_right h]

src/data/multiset/locally_finite.lean

@@ -23,9 +23,7 @@ section preorder
 variables [preorder α] [locally_finite_order α] {a b : α}
 
 lemma nodup_Icc : (Icc a b).nodup := finset.nodup _
-
 lemma nodup_Ioc : (Ioc a b).nodup := finset.nodup _
-
 lemma nodup_Ioo : (Ioo a b).nodup := finset.nodup _
 
 @[simp] lemma Icc_eq_zero_iff : Icc a b = 0 ↔ ¬a ≤ b :=
@@ -43,36 +41,26 @@ alias Ioc_eq_zero_iff ↔ _ multiset.Ioc_eq_zero
 @[simp] lemma Ioo_eq_zero (h : ¬a < b) : Ioo a b = 0 :=
 eq_zero_iff_forall_not_mem.2 $ λ x hx, h ((mem_Ioo.1 hx).1.trans (mem_Ioo.1 hx).2)
 
-@[simp] lemma Icc_eq_zero_of_lt (h : b < a) : Icc a b = 0 :=
-Icc_eq_zero h.not_le
-
-@[simp] lemma Ioc_eq_zero_of_le (h : b ≤ a) : Ioc a b = 0 :=
-Ioc_eq_zero h.not_lt
-
-@[simp] lemma Ioo_eq_zero_of_le (h : b ≤ a) : Ioo a b = 0 :=
-Ioo_eq_zero h.not_lt
+@[simp] lemma Icc_eq_zero_of_lt (h : b < a) : Icc a b = 0 := Icc_eq_zero h.not_le
+@[simp] lemma Ioc_eq_zero_of_le (h : b ≤ a) : Ioc a b = 0 := Ioc_eq_zero h.not_lt
+@[simp] lemma Ioo_eq_zero_of_le (h : b ≤ a) : Ioo a b = 0 := Ioo_eq_zero h.not_lt
 
 variables (a)
 
-@[simp] lemma Ioc_self : Ioc a a = 0 :=
-by rw [Ioc, finset.Ioc_self, finset.empty_val]
-
-@[simp] lemma Ioo_self : Ioo a a = 0 :=
-by rw [Ioo, finset.Ioo_self, finset.empty_val]
+@[simp] lemma Ioc_self : Ioc a a = 0 := by rw [Ioc, finset.Ioc_self, finset.empty_val]
+@[simp] lemma Ioo_self : Ioo a a = 0 := by rw [Ioo, finset.Ioo_self, finset.empty_val]
 
 end preorder
 
 section partial_order
 variables [partial_order α] [locally_finite_order α] {a b : α}
 
-@[simp] lemma Icc_self (a : α) : Icc a a = {a} :=
-by rw [Icc, finset.Icc_self, finset.singleton_val]
+@[simp] lemma Icc_self (a : α) : Icc a a = {a} := by rw [Icc, finset.Icc_self, finset.singleton_val]
 
 end partial_order
 
 section ordered_cancel_add_comm_monoid
-variables [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α]
-  [locally_finite_order α]
+variables [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] [locally_finite_order α]
 
 lemma map_add_left_Icc (a b c : α) : (Icc a b).map ((+) c) = Icc (c + a) (c + b) :=
 by { classical, rw [Icc, Icc, ←finset.image_add_left_Icc, finset.image_val,

src/order/locally_finite.lean

@@ -157,23 +157,19 @@ variables [preorder α] [locally_finite_order α]
 
 /-- The finset of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `set.Icc a b` as a finset.
 -/
-def Icc (a b : α) : finset α :=
-locally_finite_order.finset_Icc a b
+def Icc (a b : α) : finset α := locally_finite_order.finset_Icc a b
 
 /-- The finset of elements `x` such that `a ≤ x` and `x < b`. Basically `set.Ico a b` as a finset.
 -/
-def Ico (a b : α) : finset α :=
-locally_finite_order.finset_Ico a b
+def Ico (a b : α) : finset α := locally_finite_order.finset_Ico a b
 
 /-- The finset of elements `x` such that `a < x` and `x ≤ b`. Basically `set.Ioc a b` as a finset.
 -/
-def Ioc (a b : α) : finset α :=
-locally_finite_order.finset_Ioc a b
+def Ioc (a b : α) : finset α := locally_finite_order.finset_Ioc a b
 
 /-- The finset of elements `x` such that `a < x` and `x < b`. Basically `set.Ioo a b` as a finset.
 -/
-def Ioo (a b : α) : finset α :=
-locally_finite_order.finset_Ioo a b
+def Ioo (a b : α) : finset α := locally_finite_order.finset_Ioo a b
 
 @[simp] lemma mem_Icc {a b x : α} : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b :=
 locally_finite_order.finset_mem_Icc a b x
@@ -199,8 +195,7 @@ by { ext, rw [mem_coe, mem_Ioc, set.mem_Ioc] }
 @[simp, norm_cast] lemma coe_Ioo (a b : α) : (Ioo a b : set α) = set.Ioo a b :=
 by { ext, rw [mem_coe, mem_Ioo, set.mem_Ioo] }
 
-theorem Ico_subset_Ico {a₁ b₁ a₂ b₂ : α} (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) :
-  Ico a₁ b₁ ⊆ Ico a₂ b₂ :=
+theorem Ico_subset_Ico {a₁ b₁ a₂ b₂ : α} (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Ico a₁ b₁ ⊆ Ico a₂ b₂ :=
 begin
   rintro x hx,
   rw mem_Ico at ⊢ hx,
@@ -227,24 +222,19 @@ by rw [Ici, coe_Icc, set.Icc_top]
 @[simp, norm_cast] lemma coe_Ioi (a : α) : (Ioi a : set α) = set.Ioi a :=
 by rw [Ioi, coe_Ioc, set.Ioc_top]
 
-@[simp] lemma mem_Ici {a x : α} : x ∈ Ici a ↔ a ≤ x :=
-by rw [←set.mem_Ici, ←coe_Ici, mem_coe]
-
-@[simp] lemma mem_Ioi {a x : α} : x ∈ Ioi a ↔ a < x :=
-by rw [←set.mem_Ioi, ←coe_Ioi, mem_coe]
+@[simp] lemma mem_Ici {a x : α} : x ∈ Ici a ↔ a ≤ x := by rw [←set.mem_Ici, ←coe_Ici, mem_coe]
+@[simp] lemma mem_Ioi {a x : α} : x ∈ Ioi a ↔ a < x := by rw [←set.mem_Ioi, ←coe_Ioi, mem_coe]
 
 end order_top
 
 section order_bot
 variables [order_bot α] [locally_finite_order α]
 
 /-- The finset of elements `x` such that `x ≤ b`. Basically `set.Iic b` as a finset. -/
-def Iic (b : α) : finset α :=
-Icc ⊥ b
+def Iic (b : α) : finset α := Icc ⊥ b
 
 /-- The finset of elements `x` such that `x < b`. Basically `set.Iio b` as a finset. -/
-def Iio (b : α) : finset α :=
-Ico ⊥ b
+def Iio (b : α) : finset α := Ico ⊥ b
 
 lemma Iic_eq_Icc : Iic = Icc (⊥ : α) := rfl
 lemma Iio_eq_Ico : Iio = Ico (⊥ : α) := rfl
@@ -255,11 +245,8 @@ by rw [Iic, coe_Icc, set.Icc_bot]
 @[simp, norm_cast] lemma coe_Iio (b : α) : (Iio b : set α) = set.Iio b :=
 by rw [Iio, coe_Ico, set.Ico_bot]
 
-@[simp] lemma mem_Iic {b x : α} : x ∈ Iic b ↔ x ≤ b :=
-by rw [←set.mem_Iic, ←coe_Iic, mem_coe]
-
-@[simp] lemma mem_Iio {b x : α} : x ∈ Iio b ↔ x < b :=
-by rw [←set.mem_Iio, ←coe_Iio, mem_coe]
+@[simp] lemma mem_Iic {b x : α} : x ∈ Iic b ↔ x ≤ b := by rw [←set.mem_Iic, ←coe_Iic, mem_coe]
+@[simp] lemma mem_Iio {b x : α} : x ∈ Iio b ↔ x < b := by rw [←set.mem_Iio, ←coe_Iio, mem_coe]
 
 end order_bot
 end finset
@@ -272,20 +259,17 @@ variables [preorder α] [locally_finite_order α]
 
 /-- The multiset of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `set.Icc a b` as a
 multiset. -/
-def Icc (a b : α) : multiset α :=
-(finset.Icc a b).val
+def Icc (a b : α) : multiset α := (finset.Icc a b).val
 
 -- TODO@Yaël: Nuke `data.multiset.intervals` and redefine `multiset.Ico` here
 
 /-- The multiset of elements `x` such that `a < x` and `x ≤ b`. Basically `set.Ioc a b` as a
 multiset. -/
-def Ioc (a b : α) : multiset α :=
-(finset.Ioc a b).val
+def Ioc (a b : α) : multiset α := (finset.Ioc a b).val
 
 /-- The multiset of elements `x` such that `a < x` and `x < b`. Basically `set.Ioo a b` as a
 multiset. -/
-def Ioo (a b : α) : multiset α :=
-(finset.Ioo a b).val
+def Ioo (a b : α) : multiset α := (finset.Ioo a b).val
 
 @[simp] lemma mem_Icc {a b x : α} : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b :=
 by rw [Icc, ←finset.mem_def, finset.mem_Icc]
@@ -302,37 +286,28 @@ section order_top
 variables [order_top α] [locally_finite_order α]
 
 /-- The multiset of elements `x` such that `a ≤ x`. Basically `set.Ici a` as a multiset. -/
-def Ici (a : α) : multiset α :=
-(finset.Ici a).val
+def Ici (a : α) : multiset α := (finset.Ici a).val
 
 /-- The multiset of elements `x` such that `a < x`. Basically `set.Ioi a` as a multiset. -/
-def Ioi (a : α) : multiset α :=
-(finset.Ioi a).val
-
-@[simp] lemma mem_Ici {a x : α} : x ∈ Ici a ↔ a ≤ x :=
-by rw [Ici, ←finset.mem_def, finset.mem_Ici]
+def Ioi (a : α) : multiset α := (finset.Ioi a).val
 
-@[simp] lemma mem_Ioi {a x : α} : x ∈ Ioi a ↔ a < x :=
-by rw [Ioi, ←finset.mem_def, finset.mem_Ioi]
+@[simp] lemma mem_Ici {a x : α} : x ∈ Ici a ↔ a ≤ x := by rw [Ici, ←finset.mem_def, finset.mem_Ici]
+@[simp] lemma mem_Ioi {a x : α} : x ∈ Ioi a ↔ a < x := by rw [Ioi, ←finset.mem_def, finset.mem_Ioi]
 
 end order_top
 
 section order_bot
 variables [order_bot α] [locally_finite_order α]
 
 /-- The multiset of elements `x` such that `x ≤ b`. Basically `set.Iic b` as a multiset. -/
-def Iic (b : α) : multiset α :=
-(finset.Iic b).val
+def Iic (b : α) : multiset α := (finset.Iic b).val
 
 /-- The multiset of elements `x` such that `x < b`. Basically `set.Iio b` as a multiset. -/
-def Iio (b : α) : multiset α :=
-(finset.Iio b).val
+def Iio (b : α) : multiset α := (finset.Iio b).val
 
-@[simp] lemma mem_Iic {b x : α} : x ∈ Iic b ↔ x ≤ b :=
-by rw [Iic, ←finset.mem_def, finset.mem_Iic]
+@[simp] lemma mem_Iic {b x : α} : x ∈ Iic b ↔ x ≤ b := by rw [Iic, ←finset.mem_def, finset.mem_Iic]
 
-@[simp] lemma mem_Iio {b x : α} : x ∈ Iio b ↔ x < b :=
-by rw [Iio, ←finset.mem_def, finset.mem_Iio]
+@[simp] lemma mem_Iio {b x : α} : x ∈ Iio b ↔ x < b := by rw [Iio, ←finset.mem_def, finset.mem_Iio]
 
 end order_bot
 end multiset
@@ -378,11 +353,9 @@ fintype.of_finset (finset.Ici a) (λ x, by rw [finset.mem_Ici, mem_Ici])
 instance fintype_Ioi : fintype (Ioi a) :=
 fintype.of_finset (finset.Ioi a) (λ x, by rw [finset.mem_Ioi, mem_Ioi])
 
-lemma finite_Ici : (Ici a).finite :=
-⟨set.fintype_Ici a⟩
+lemma finite_Ici : (Ici a).finite := ⟨set.fintype_Ici a⟩
 
-lemma finite_Ioi : (Ioi a).finite :=
-⟨set.fintype_Ioi a⟩
+lemma finite_Ioi : (Ioi a).finite := ⟨set.fintype_Ioi a⟩
 
 end order_top
 
@@ -395,11 +368,9 @@ fintype.of_finset (finset.Iic b) (λ x, by rw [finset.mem_Iic, mem_Iic])
 instance fintype_Iio : fintype (Iio b) :=
 fintype.of_finset (finset.Iio b) (λ x, by rw [finset.mem_Iio, mem_Iio])
 
-lemma finite_Iic : (Iic b).finite :=
-⟨set.fintype_Iic b⟩
+lemma finite_Iic : (Iic b).finite := ⟨set.fintype_Iic b⟩
 
-lemma finite_Iio : (Iio b).finite :=
-⟨set.fintype_Iio b⟩
+lemma finite_Iio : (Iio b).finite := ⟨set.fintype_Iio b⟩
 
 end order_bot
 
@@ -413,8 +384,7 @@ section preorder
 variables [preorder α]
 
 /-- A noncomputable constructor from the finiteness of all closed intervals. -/
-noncomputable def locally_finite_order.of_finite_Icc
-  (h : ∀ a b : α, (set.Icc a b).finite) :
+noncomputable def locally_finite_order.of_finite_Icc (h : ∀ a b : α, (set.Icc a b).finite) :
   locally_finite_order α :=
 @locally_finite_order.of_Icc' α _ (classical.dec_rel _)
   (λ a b, (h a b).to_finset)