feat(data/{finset,multiset}/locally_finite): When an Icc is a singl…

…eton, cardinality generalization (#10925)

This proves `Icc a b = {c} ↔ a = c ∧ b = c` for sets and finsets, gets rid of the `a ≤ b` assumption in `card_Ico_eq_card_Icc_sub_one` and friends and proves them for multisets.

src/data/finset/interval.lean

@@ -77,14 +77,14 @@ end
 
 /-- Cardinality of an `Ico` of finsets. -/
 lemma card_Ico_finset (h : s ⊆ t) : (Ico s t).card = 2 ^ (t.card - s.card) - 1 :=
-by rw [card_Ico_eq_card_Icc_sub_one (le_iff_subset.2 h), card_Icc_finset h]
+by rw [card_Ico_eq_card_Icc_sub_one, card_Icc_finset h]
 
 /-- Cardinality of an `Ioc` of finsets. -/
 lemma card_Ioc_finset (h : s ⊆ t) : (Ioc s t).card = 2 ^ (t.card - s.card) - 1 :=
-by rw [card_Ioc_eq_card_Icc_sub_one (le_iff_subset.2 h), card_Icc_finset h]
+by rw [card_Ioc_eq_card_Icc_sub_one, card_Icc_finset h]
 
 /-- Cardinality of an `Ioo` of finsets. -/
 lemma card_Ioo_finset (h : s ⊆ t) : (Ioo s t).card = 2 ^ (t.card - s.card) - 2 :=
-by rw [card_Ioo_eq_card_Icc_sub_two (le_iff_subset.2 h), card_Icc_finset h]
+by rw [card_Ioo_eq_card_Icc_sub_two, card_Icc_finset h]
 
 end finset

src/data/finset/locally_finite.lean

@@ -122,10 +122,13 @@ let ⟨a, ha⟩ := h₀, ⟨b, hb⟩ := h₁ in by { classical, exact ⟨set.fin
 end preorder
 
 section partial_order
-variables [partial_order α] [locally_finite_order α] {a b : α}
+variables [partial_order α] [locally_finite_order α] {a b c : α}
 
 @[simp] lemma Icc_self (a : α) : Icc a a = {a} := by rw [←coe_eq_singleton, coe_Icc, set.Icc_self]
 
+@[simp] lemma Icc_eq_singleton_iff : Icc a b = {c} ↔ a = c ∧ b = c :=
+by rw [←coe_eq_singleton, coe_Icc, set.Icc_eq_singleton_iff]
+
 section decidable_eq
 variables [decidable_eq α]
 
@@ -161,27 +164,31 @@ begin
   exact and_iff_left_of_imp (λ h, h.le.trans_lt hab),
 end
 
-lemma card_Ico_eq_card_Icc_sub_one (h : a ≤ b) : (Ico a b).card = (Icc a b).card - 1 :=
+lemma card_Ico_eq_card_Icc_sub_one (a b : α) : (Ico a b).card = (Icc a b).card - 1 :=
 begin
   classical,
-  rw [←Ico_insert_right h, card_insert_of_not_mem right_not_mem_Ico],
-  exact (nat.add_sub_cancel _ _).symm,
+  by_cases h : a ≤ b,
+  { rw [←Ico_insert_right h, card_insert_of_not_mem right_not_mem_Ico],
+    exact (nat.add_sub_cancel _ _).symm },
+  { rw [Ico_eq_empty (λ h', h h'.le), Icc_eq_empty h, card_empty, zero_tsub] }
 end
 
-lemma card_Ioc_eq_card_Icc_sub_one (h : a ≤ b) : (Ioc a b).card = (Icc a b).card - 1 :=
-@card_Ico_eq_card_Icc_sub_one (order_dual α) _ _ _ _ h
+lemma card_Ioc_eq_card_Icc_sub_one (a b : α) : (Ioc a b).card = (Icc a b).card - 1 :=
+@card_Ico_eq_card_Icc_sub_one (order_dual α) _ _ _ _
 
-lemma card_Ioo_eq_card_Ico_sub_one (h : a ≤ b) : (Ioo a b).card = (Ico a b).card - 1 :=
+lemma card_Ioo_eq_card_Ico_sub_one (a b : α) : (Ioo a b).card = (Ico a b).card - 1 :=
 begin
-  obtain rfl | h' := h.eq_or_lt,
-  { rw [Ioo_self, Ico_self, card_empty] },
   classical,
-  rw [←Ioo_insert_left h', card_insert_of_not_mem left_not_mem_Ioo],
-  exact (nat.add_sub_cancel _ _).symm,
+  by_cases h : a ≤ b,
+  { obtain rfl | h' := h.eq_or_lt,
+    { rw [Ioo_self, Ico_self, card_empty] },
+    rw [←Ioo_insert_left h', card_insert_of_not_mem left_not_mem_Ioo],
+    exact (nat.add_sub_cancel _ _).symm },
+  { rw [Ioo_eq_empty (λ h', h h'.le), Ico_eq_empty (λ h', h h'.le), card_empty, zero_tsub] }
 end
 
-lemma card_Ioo_eq_card_Icc_sub_two (h : a ≤ b) : (Ioo a b).card = (Icc a b).card - 2 :=
-by { rw [card_Ioo_eq_card_Ico_sub_one h, card_Ico_eq_card_Icc_sub_one h], refl }
+lemma card_Ioo_eq_card_Icc_sub_two (a b : α) : (Ioo a b).card = (Icc a b).card - 2 :=
+by { rw [card_Ioo_eq_card_Ico_sub_one, card_Ico_eq_card_Icc_sub_one], refl }
 
 end partial_order
 

src/data/multiset/locally_finite.lean

@@ -115,6 +115,18 @@ lemma Ico_filter_le_left {a b : α} [decidable_pred (≤ a)] (hab : a < b) :
   (Ico a b).filter (λ x, x ≤ a) = {a} :=
 by { rw [Ico, ←finset.filter_val, finset.Ico_filter_le_left hab], refl }
 
+lemma card_Ico_eq_card_Icc_sub_one (a b : α) : (Ico a b).card = (Icc a b).card - 1 :=
+finset.card_Ico_eq_card_Icc_sub_one _ _
+
+lemma card_Ioc_eq_card_Icc_sub_one (a b : α) : (Ioc a b).card = (Icc a b).card - 1 :=
+finset.card_Ioc_eq_card_Icc_sub_one _ _
+
+lemma card_Ioo_eq_card_Ico_sub_one (a b : α) : (Ioo a b).card = (Ico a b).card - 1 :=
+finset.card_Ioo_eq_card_Ico_sub_one _ _
+
+lemma card_Ioo_eq_card_Icc_sub_two (a b : α) : (Ioo a b).card = (Icc a b).card - 2 :=
+finset.card_Ioo_eq_card_Icc_sub_two _ _
+
 end partial_order
 
 section linear_order

src/data/set/intervals/basic.lean

@@ -375,11 +375,21 @@ by rw [←not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioo]
 end intervals
 
 section partial_order
-variables {α : Type u} [partial_order α] {a b : α}
+variables {α : Type u} [partial_order α] {a b c : α}
 
 @[simp] lemma Icc_self (a : α) : Icc a a = {a} :=
 set.ext $ by simp [Icc, le_antisymm_iff, and_comm]
 
+@[simp] lemma Icc_eq_singleton_iff : Icc a b = {c} ↔ a = c ∧ b = c :=
+begin
+  refine ⟨λ h, _, _⟩,
+  { have hab : a ≤ b := nonempty_Icc.1 (h.symm.subst $ singleton_nonempty c),
+    exact ⟨eq_of_mem_singleton $ h.subst $ left_mem_Icc.2 hab,
+      eq_of_mem_singleton $ h.subst $ right_mem_Icc.2 hab⟩ },
+  { rintro ⟨rfl, rfl⟩,
+    exact Icc_self _ }
+end
+
 @[simp] lemma Icc_diff_left : Icc a b \ {a} = Ioc a b :=
 ext $ λ x, by simp [lt_iff_le_and_ne, eq_comm, and.right_comm]