feat(data/finset/basic): When insert is injective and other lemmas (#…

…11982)

* `insert`/`cons` lemmas for `finset` and `multiset`
* `has_ssubset` instance for `multiset`
* `finset.sdiff_nonempty`
* `disjoint.of_image_finset`, `finset.disjoint_image`, `finset.disjoint_map`
* `finset.exists_eq_insert_iff`
* `mem` lemmas
* change `pred` to `- 1` into the statement of `finset.card_erase_of_mem`

src/combinatorics/derangements/finite.lean

@@ -47,7 +47,8 @@ begin
   have h1 : ∀ a : fin (n+1), card ({a}ᶜ : set (fin (n+1))) = card (fin n),
   { intro a,
     simp only [fintype.card_fin, finset.card_fin, fintype.card_of_finset, finset.filter_ne' _ a,
-      set.mem_compl_singleton_iff, finset.card_erase_of_mem (finset.mem_univ a), nat.pred_succ] },
+      set.mem_compl_singleton_iff, finset.card_erase_of_mem (finset.mem_univ a),
+      add_tsub_cancel_right] },
   have h2 : card (fin (n+2)) = card (option (fin (n+1))),
   { simp only [card_fin, card_option] },
   -- rewrite the LHS and substitute in our fintype-level equivalence

src/combinatorics/set_family/shadow.lean

@@ -77,7 +77,6 @@ begin
   intros A h,
   obtain ⟨A, hA, i, hi, rfl⟩ := mem_shadow_iff.1 h,
   rw [card_erase_of_mem hi, h𝒜 hA],
-  refl,
 end
 
 /-- `t` is in the shadow of `𝒜` iff we can add an element to it so that the resulting finset is in

src/combinatorics/simple_graph/basic.lean

@@ -649,10 +649,7 @@ by simp only [neighbor_finset, neighbor_set_compl, set.to_finset_sdiff, set.to_f
 @[simp]
 lemma complete_graph_degree [decidable_eq V] (v : V) :
   (⊤ : simple_graph V).degree v = fintype.card V - 1 :=
-begin
-  convert univ.card.pred_eq_sub_one,
-  erw [degree, neighbor_finset_eq_filter, filter_ne, card_erase_of_mem (mem_univ v)],
-end
+by erw [degree, neighbor_finset_eq_filter, filter_ne, card_erase_of_mem (mem_univ v), card_univ]
 
 lemma bot_degree (v : V) : (⊥ : simple_graph V).degree v = 0 :=
 begin

src/combinatorics/simple_graph/degree_sum.lean

@@ -214,12 +214,10 @@ begin
     rw and_comm, },
   simp only [hc, filter_congr_decidable],
   rw [←filter_filter, filter_ne', card_erase_of_mem],
-  { use k - 1,
-    rw [nat.pred_eq_succ_iff, hg, mul_tsub, tsub_add_eq_add_tsub, eq_comm,
-      tsub_eq_iff_eq_add_of_le],
-    { ring },
-    { exact add_le_add_right (zero_le _) 2 },
-    { exact nat.mul_le_mul_left _ hk } },
+  { refine ⟨k - 1, tsub_eq_of_eq_add $ hg.trans _⟩,
+    rw [add_assoc, one_add_one_eq_two,  ←nat.mul_succ],
+    congr,
+    exact (tsub_add_cancel_of_le $ nat.succ_le_iff.2 hk).symm },
   { simpa only [true_and, mem_filter, mem_univ] },
 end
 

src/data/finset/basic.lean

@@ -510,9 +510,22 @@ def cons (a : α) (s : finset α) (h : a ∉ s) : finset α := ⟨a ::ₘ s.1, n
 
 @[simp] lemma coe_cons {a s h} : (@cons α a s h : set α) = insert a s := by { ext, simp }
 
+lemma subset_cons (h : a ∉ s) : s ⊆ s.cons a h := subset_cons _ _
+lemma ssubset_cons (h : a ∉ s) : s ⊂ s.cons a h := ssubset_cons h
+lemma cons_subset {h : a ∉ s} : s.cons a h ⊆ t ↔ a ∈ t ∧ s ⊆ t := cons_subset
+
 @[simp] lemma cons_subset_cons {hs ht} : s.cons a hs ⊆ t.cons a ht ↔ s ⊆ t :=
 by rwa [← coe_subset, coe_cons, coe_cons, set.insert_subset_insert_iff, coe_subset]
 
+lemma ssubset_iff_exists_cons_subset : s ⊂ t ↔ ∃ a (h : a ∉ s), s.cons a h ⊆ t :=
+begin
+  refine ⟨λ h, _, λ ⟨a, ha, h⟩, ssubset_of_ssubset_of_subset (ssubset_cons _) h⟩,
+  obtain ⟨a, hs, ht⟩ := (not_subset _ _).1 h.2,
+  exact ⟨a, ht, cons_subset.2 ⟨hs, h.subset⟩⟩,
+end
+
+end cons
+
 /-! ### disjoint union -/
 
 /-- `disj_union s t h` is the set such that `a ∈ disj_union s t h` iff `a ∈ s` or `a ∈ t`.
@@ -525,8 +538,6 @@ def disj_union {α} (s t : finset α) (h : ∀ a ∈ s, a ∉ t) : finset α :=
   a ∈ @disj_union α s t h ↔ a ∈ s ∨ a ∈ t :=
 by rcases s with ⟨⟨s⟩⟩; rcases t with ⟨⟨t⟩⟩; apply list.mem_append
 
-end cons
-
 /-! ### insert -/
 
 section decidable_eq
@@ -550,6 +561,8 @@ by rw [insert_val, ndinsert_of_not_mem h]
 theorem mem_insert_self (a : α) (s : finset α) : a ∈ insert a s := mem_ndinsert_self a s.1
 lemma mem_insert_of_mem (h : a ∈ s) : a ∈ insert b s := mem_ndinsert_of_mem h
 lemma mem_of_mem_insert_of_ne (h : b ∈ insert a s) : b ≠ a → b ∈ s := (mem_insert.1 h).resolve_left
+lemma eq_of_not_mem_of_mem_insert (ha : b ∈ insert a s) (hb : b ∉ s) : b = a :=
+(mem_insert.1 ha).resolve_right hb
 
 @[simp] theorem cons_eq_insert {α} [decidable_eq α] (a s h) : @cons α a s h = insert a s :=
 ext $ λ a, by simp
@@ -606,6 +619,11 @@ lemma subset_insert (a : α) (s : finset α) : s ⊆ insert a s := λ b, mem_ins
 theorem insert_subset_insert (a : α) {s t : finset α} (h : s ⊆ t) : insert a s ⊆ insert a t :=
 insert_subset.2 ⟨mem_insert_self _ _, subset.trans h (subset_insert _ _)⟩
 
+lemma insert_inj (ha : a ∉ s) : insert a s = insert b s ↔ a = b :=
+⟨λ h, eq_of_not_mem_of_mem_insert (h.subst $ mem_insert_self _ _) ha, congr_arg _⟩
+
+lemma insert_inj_on (s : finset α) : set.inj_on (λ a, insert a s) sᶜ := λ a h b _, (insert_inj h).1
+
 lemma ssubset_iff : s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t :=
 by exact_mod_cast @set.ssubset_iff_insert α s t
 
@@ -1116,6 +1134,9 @@ lemma sdiff_union_inter (s t : finset α) : (s \ t) ∪ (s ∩ t) = s := sup_sdi
 
 lemma sdiff_eq_empty_iff_subset : s \ t = ∅ ↔ s ⊆ t := sdiff_eq_bot_iff
 
+lemma sdiff_nonempty : (s \ t).nonempty ↔ ¬ s ⊆ t :=
+nonempty_iff_ne_empty.trans sdiff_eq_empty_iff_subset.not
+
 @[simp] lemma empty_sdiff (s : finset α) : ∅ \ s = ∅ := bot_sdiff
 
 lemma insert_sdiff_of_not_mem (s : finset α) {t : finset α} {x : α} (h : x ∉ t) :
@@ -2319,7 +2340,7 @@ end bUnion
 /-! ### disjoint -/
 --TODO@Yaël: Kill lemmas duplicate with `boolean_algebra`
 section disjoint
-variables [decidable_eq α] [decidable_eq β] {s t u : finset α} {a b : α}
+variables [decidable_eq α] [decidable_eq β] {f : α → β} {s t u : finset α} {a b : α}
 
 lemma disjoint_left : disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t :=
 by simp only [_root_.disjoint, inf_eq_inter, le_iff_subset, subset_iff, mem_inter, not_and,
@@ -2335,6 +2356,9 @@ lemma disjoint_right : disjoint s t ↔ ∀ {a}, a ∈ t → a ∉ s := by rw [d
 lemma disjoint_iff_ne : disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b :=
 by simp only [disjoint_left, imp_not_comm, forall_eq']
 
+lemma _root_.disjoint.forall_ne_finset (h : disjoint s t) (ha : a ∈ s) (hb : b ∈ t) : a ≠ b :=
+disjoint_iff_ne.1 h _ ha _ hb
+
 lemma not_disjoint_iff : ¬ disjoint s t ↔ ∃ a, a ∈ s ∧ a ∈ t :=
 not_forall.trans $ exists_congr $ λ a, not_not.trans mem_inter
 
@@ -2407,6 +2431,23 @@ lemma disjoint_filter_filter_neg (s : finset α) (p : α → Prop) [decidable_pr
 lemma disjoint_iff_disjoint_coe : disjoint s t ↔ disjoint (s : set α) (t : set α) :=
 by { rw [finset.disjoint_left, set.disjoint_left], refl }
 
+@[simp] lemma _root_.disjoint.of_image_finset (h : disjoint (s.image f) (t.image f)) :
+  disjoint s t :=
+disjoint_iff_ne.2 $ λ a ha b hb, ne_of_apply_ne f $ h.forall_ne_finset
+  (mem_image_of_mem _ ha) (mem_image_of_mem _ hb)
+
+@[simp] lemma disjoint_image {f : α → β} (hf : injective f) :
+  disjoint (s.image f) (t.image f) ↔ disjoint s t :=
+begin
+  simp only [disjoint_iff_ne, mem_image, exists_prop, exists_imp_distrib, and_imp],
+  refine ⟨λ h a ha b hb hab, h _ _ ha rfl _ _ hb rfl $ congr_arg _ hab, _⟩,
+  rintro h _ a ha rfl _ b hb rfl,
+  exact hf.ne (h _ ha _ hb),
+end
+
+@[simp] lemma disjoint_map {f : α ↪ β} : disjoint (s.map f) (t.map f) ↔ disjoint s t :=
+by { simp_rw map_eq_image, exact disjoint_image f.injective }
+
 end disjoint
 
 /-! ### choose -/

src/data/finset/card.lean

@@ -88,9 +88,7 @@ begin
   { rw [card_insert_of_not_mem h, if_neg h] }
 end
 
-@[simp]
-lemma card_erase_of_mem : a ∈ s → (s.erase a).card = pred s.card := card_erase_of_mem
-
+@[simp] lemma card_erase_of_mem : a ∈ s → (s.erase a).card = s.card - 1 := card_erase_of_mem
 @[simp] lemma card_erase_add_one : a ∈ s → (s.erase a).card + 1 = s.card := card_erase_add_one
 
 lemma card_erase_lt_of_mem : a ∈ s → (s.erase a).card < s.card := card_erase_lt_of_mem
@@ -106,7 +104,7 @@ begin
 end
 
 /-- If `a ∈ s` is known, see also `finset.card_erase_of_mem` and `finset.erase_eq_of_not_mem`. -/
-lemma card_erase_eq_ite : (s.erase a).card = if a ∈ s then pred s.card else s.card :=
+lemma card_erase_eq_ite : (s.erase a).card = if a ∈ s then s.card - 1 else s.card :=
 card_erase_eq_ite
 
 end insert_erase
@@ -335,9 +333,8 @@ begin
     apply nat.succ_pos },
   rcases this with ⟨a, ha⟩,
   have z : i + card B + k = card (erase A a),
-  { rw [card_erase_of_mem, ←h, nat.add_succ, nat.pred_succ],
-    rw mem_sdiff at ha,
-    exact ha.1 },
+  { rw [card_erase_of_mem (mem_sdiff.1 ha).1, ←h],
+    refl },
   rcases ih _ z with ⟨B', hB', B'subA', cards⟩,
   { exact ⟨B', hB', trans B'subA' (erase_subset _ _), cards⟩ },
   { rintro t th,
@@ -369,6 +366,21 @@ end
 lemma card_eq_one : s.card = 1 ↔ ∃ a, s = {a} :=
 by cases s; simp only [multiset.card_eq_one, finset.card, ←val_inj, singleton_val]
 
+lemma exists_eq_insert_iff [decidable_eq α] {s t : finset α} :
+  (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.card + 1 = t.card :=
+begin
+  split,
+  { rintro ⟨a, ha, rfl⟩,
+    exact ⟨subset_insert _ _, (card_insert_of_not_mem ha).symm⟩ },
+  { rintro ⟨hst, h⟩,
+    obtain ⟨a, ha⟩ : ∃ a, t \ s = {a},
+    { exact card_eq_one.1 (by rw [card_sdiff hst, ←h, add_tsub_cancel_left]) },
+    refine ⟨a, λ hs, (_ : a ∉ {a}) $ mem_singleton_self _,
+      by rw [insert_eq, ←ha, sdiff_union_of_subset hst]⟩,
+    rw ←ha,
+    exact not_mem_sdiff_of_mem_right hs }
+end
+
 lemma card_le_one : s.card ≤ 1 ↔ ∀ (a ∈ s) (b ∈ s), a = b :=
 begin
   obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty,
@@ -428,12 +440,11 @@ begin
   { exact ⟨y, hy, ha⟩ }
 end
 
-lemma card_eq_succ [decidable_eq α] :
-  s.card = n + 1 ↔ (∃ a t, a ∉ t ∧ insert a t = s ∧ t.card = n) :=
-⟨λ eq,
-  let ⟨a, has⟩ := card_pos.mp (eq.symm ▸ nat.zero_lt_succ _ : 0 < s.card) in
+lemma card_eq_succ [decidable_eq α] : s.card = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.card = n :=
+⟨λ h,
+  let ⟨a, has⟩ := card_pos.mp (h.symm ▸ nat.zero_lt_succ _ : 0 < s.card) in
     ⟨a, s.erase a, s.not_mem_erase a, insert_erase has,
-      by simp only [eq, card_erase_of_mem has, pred_succ]⟩,
+      by simp only [h, card_erase_of_mem has, add_tsub_cancel_right]⟩,
   λ ⟨a, t, hat, s_eq, n_eq⟩, s_eq ▸ n_eq ▸ card_insert_of_not_mem hat⟩
 
 lemma card_eq_two [decidable_eq α] : s.card = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y} :=

src/data/finset/powerset.lean

@@ -238,7 +238,7 @@ begin
       { refine ⟨insert x t, _, mem_insert_self _ _⟩,
         rw [←insert_erase hx, powerset_len_succ_insert (not_mem_erase _ _)],
         exact mem_union_right _ (mem_image_of_mem _ ht) },
-      { rwa [card_erase_of_mem hx, nat.lt_pred_iff] } } }
+      { rwa [card_erase_of_mem hx, lt_tsub_iff_right] } } }
 end
 
 @[simp]

src/data/multiset/basic.lean

@@ -228,6 +228,7 @@ section subset
 protected def subset (s t : multiset α) : Prop := ∀ ⦃a : α⦄, a ∈ s → a ∈ t
 
 instance : has_subset (multiset α) := ⟨multiset.subset⟩
+instance : has_ssubset (multiset α) := ⟨λ s t, s ⊆ t ∧ ¬ t ⊆ s⟩
 
 @[simp] theorem coe_subset {l₁ l₂ : list α} : (l₁ : multiset α) ⊆ l₂ ↔ l₁ ⊆ l₂ := iff.rfl
 
@@ -243,9 +244,17 @@ theorem mem_of_subset {s t : multiset α} {a : α} (h : s ⊆ t) : a ∈ s → a
 @[simp] theorem zero_subset (s : multiset α) : 0 ⊆ s :=
 λ a, (not_mem_nil a).elim
 
+lemma subset_cons (s : multiset α) (a : α) : s ⊆ a ::ₘ s := λ _, mem_cons_of_mem
+
+lemma ssubset_cons {s : multiset α} {a : α} (ha : a ∉ s) : s ⊂ a ::ₘ s :=
+⟨subset_cons _ _, λ h, ha $ h $ mem_cons_self _ _⟩
+
 @[simp] theorem cons_subset {a : α} {s t : multiset α} : (a ::ₘ s) ⊆ t ↔ a ∈ t ∧ s ⊆ t :=
 by simp [subset_iff, or_imp_distrib, forall_and_distrib]
 
+lemma cons_subset_cons {a : α} {s t : multiset α} : s ⊆ t → a ::ₘ s ⊆ a ::ₘ t :=
+quotient.induction_on₂ s t $ λ _ _, cons_subset_cons _
+
 theorem eq_zero_of_subset_zero {s : multiset α} (h : s ⊆ 0) : s = 0 :=
 eq_zero_of_forall_not_mem h
 

src/data/nat/totient.lean

@@ -49,8 +49,8 @@ calc totient n ≤ ((range n).filter (≠ 0)).card :
     intros n1 hn1 hn1',
     simpa only [hn1', coprime_zero_right, hn.ne'] using hn1,
   end
-... = n - 1 : by simp only [filter_ne' (range n) 0, card_erase_of_mem, n.pred_eq_sub_one,
-                card_range, pos_of_gt hn, mem_range]
+... = n - 1
+    : by simp only [filter_ne' (range n) 0, card_erase_of_mem, card_range, pos_of_gt hn, mem_range]
 ... < n : nat.sub_lt (pos_of_gt hn) zero_lt_one
 
 lemma totient_pos : ∀ {n : ℕ}, 0 < n → 0 < φ n

src/data/polynomial/erase_lead.lean

@@ -98,8 +98,7 @@ lemma erase_lead_card_support {c : ℕ} (fc : f.support.card = c) :
 begin
   by_cases f0 : f = 0,
   { rw [← fc, f0, erase_lead_zero, support_zero, card_empty] },
-  { rw [erase_lead_support, card_erase_of_mem (nat_degree_mem_support_of_nonzero f0), fc],
-    exact c.pred_eq_sub_one },
+  { rw [erase_lead_support, card_erase_of_mem (nat_degree_mem_support_of_nonzero f0), fc] }
 end
 
 lemma erase_lead_card_support' {c : ℕ} (fc : f.support.card = c + 1) :

src/data/set/basic.lean

@@ -166,7 +166,7 @@ by { rintro rfl x hx, exact hx }
 
 namespace set
 
-variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {a : α} {s t : set α}
+variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {a b : α} {s t : set α}
 
 instance : inhabited (set α) := ⟨∅⟩
 
@@ -644,8 +644,8 @@ theorem mem_insert_of_mem {x : α} {s : set α} (y : α) : x ∈ s → x ∈ ins
 
 theorem eq_or_mem_of_mem_insert {x a : α} {s : set α} : x ∈ insert a s → x = a ∨ x ∈ s := id
 
-theorem mem_of_mem_insert_of_ne {x a : α} {s : set α} : x ∈ insert a s → x ≠ a → x ∈ s :=
-or.resolve_left
+lemma mem_of_mem_insert_of_ne : b ∈ insert a s → b ≠ a → b ∈ s := or.resolve_left
+lemma eq_of_not_mem_of_mem_insert : b ∈ insert a s → b ∉ s → b = a := or.resolve_right
 
 @[simp] theorem mem_insert_iff {x a : α} {s : set α} : x ∈ insert a s ↔ x = a ∨ x ∈ s := iff.rfl
 
@@ -690,6 +690,9 @@ instance (a : α) (s : set α) : nonempty (insert a s : set α) := (insert_nonem
 lemma insert_inter (x : α) (s t : set α) : insert x (s ∩ t) = insert x s ∩ insert x t :=
 ext $ λ y, or_and_distrib_left
 
+lemma insert_inj (ha : a ∉ s) : insert a s = insert b s ↔ a = b :=
+⟨λ h, eq_of_not_mem_of_mem_insert (h.subst $ mem_insert a s) ha, congr_arg _⟩
+
 -- useful in proofs by induction
 theorem forall_of_forall_insert {P : α → Prop} {a : α} {s : set α}
   (H : ∀ x, x ∈ insert a s → P x) (x) (h : x ∈ s) : P x := H _ (or.inr h)

src/data/set/finite.lean

@@ -808,7 +808,7 @@ lemma card_ne_eq [fintype α] (a : α) [fintype {x : α | x ≠ a}] :
 begin
   haveI := classical.dec_eq α,
   rw [←to_finset_card, to_finset_ne_eq_erase, finset.card_erase_of_mem (finset.mem_univ _),
-      finset.card_univ, nat.pred_eq_sub_one],
+      finset.card_univ],
 end
 
 end decidable_eq

src/data/set/function.lean

@@ -1116,4 +1116,6 @@ lemma update_comp_eq_of_not_mem_range {α β γ : Sort*} [decidable_eq β]
   (function.update g i a) ∘ f = g ∘ f :=
 update_comp_eq_of_not_mem_range' g a h
 
+lemma insert_inj_on (s : set α) : sᶜ.inj_on (λ a, insert a s) := λ a ha b _, (insert_inj ha).1
+
 end function

src/linear_algebra/affine_space/finite_dimensional.lean

@@ -204,7 +204,7 @@ begin
   rw [vector_span_eq_span_vsub_finset_right_ne k hp₁],
   refine le_trans (finrank_span_finset_le_card (((s.image p).erase p₁).image (λ p, p -ᵥ p₁))) _,
   rw [finset.card_image_of_injective _ (vsub_left_injective p₁), finset.card_erase_of_mem hp₁,
-      nat.pred_le_iff, nat.succ_eq_add_one, ← hc],
+      tsub_le_iff_right, ← hc],
   apply finset.card_image_le
 end
 

src/linear_algebra/lagrange.lean

@@ -116,7 +116,7 @@ theorem degree_interpolate_erase {x} (hx : x ∈ s) :
   (interpolate (s.erase x) f).degree < (s.card - 1 : ℕ) :=
 begin
   convert degree_interpolate_lt (s.erase x) f,
-  rw [finset.card_erase_of_mem hx, nat.pred_eq_sub_one]
+  rw finset.card_erase_of_mem hx,
 end
 
 theorem interpolate_eq_of_eval_eq (f g : F → F) {s : finset F} (hs : ∀ x ∈ s, f x = g x) :

src/logic/basic.lean

@@ -734,6 +734,19 @@ end propositional
 
 /-! ### Declarations about equality -/
 
+section mem
+variables {α β : Type*} [has_mem α β] {s t : β} {a b : α}
+
+lemma ne_of_mem_of_not_mem (h : a ∈ s) : b ∉ s → a ≠ b := mt $ λ e, e ▸ h
+lemma ne_of_mem_of_not_mem' (h : a ∈ s) : a ∉ t → s ≠ t := mt $ λ e, e ▸ h
+
+/-- **Alias** of `ne_of_mem_of_not_mem`. -/
+lemma has_mem.mem.ne_of_not_mem : a ∈ s → b ∉ s → a ≠ b := ne_of_mem_of_not_mem
+/-- **Alias** of `ne_of_mem_of_not_mem'`. -/
+lemma has_mem.mem.ne_of_not_mem' : a ∈ s → a ∉ t → s ≠ t := ne_of_mem_of_not_mem'
+
+end mem
+
 section equality
 variables {α : Sort*} {a b : α}
 
@@ -744,10 +757,6 @@ theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : hp == hq :=
 have p = q, from propext ⟨λ _, hq, λ _, hp⟩,
 by subst q; refl
 
-theorem ne_of_mem_of_not_mem {α β} [has_mem α β] {s : β} {a b : α}
-  (h : a ∈ s) : b ∉ s → a ≠ b :=
-mt $ λ e, e ▸ h
-
 -- todo: change name
 lemma ball_cond_comm {α} {s : α → Prop} {p : α → α → Prop} :
   (∀ a, s a → ∀ b, s b → p a b) ↔ (∀ a b, s a → s b → p a b) :=