chore(multiset): dedicated notation for multiset.cons (#4600)

src/algebra/big_operators/basic.lean

@@ -1089,11 +1089,11 @@ variables [decidable_eq α]
   (∑ a in s.to_finset, s.count a) = s.card :=
 multiset.induction_on s rfl
   (assume a s ih,
-    calc (∑ x in to_finset (a :: s), count x (a :: s)) =
-      ∑ x in to_finset (a :: s), ((if x = a then 1 else 0) + count x s) :
+    calc (∑ x in to_finset (a ::ₘ s), count x (a ::ₘ s)) =
+      ∑ x in to_finset (a ::ₘ s), ((if x = a then 1 else 0) + count x s) :
         finset.sum_congr rfl $ λ _ _, by split_ifs;
         [simp only [h, count_cons_self, nat.one_add], simp only [count_cons_of_ne h, zero_add]]
-      ... = card (a :: s) :
+      ... = card (a ::ₘ s) :
       begin
         by_cases a ∈ s.to_finset,
         { have : ∑ x in s.to_finset, ite (x = a) 1 0 = ∑ x in {a}, ite (x = a) 1 0,
@@ -1112,11 +1112,11 @@ lemma count_sum' {s : finset β} {a : α} {f : β → multiset α} :
 by { dunfold finset.sum, rw count_sum }
 
 lemma to_finset_sum_count_smul_eq (s : multiset α) :
-  (∑ a in s.to_finset, s.count a •ℕ (a :: 0)) = s :=
+  (∑ a in s.to_finset, s.count a •ℕ (a ::ₘ 0)) = s :=
 begin
   apply ext', intro b,
   rw count_sum',
-  have h : count b s = count b (count b s •ℕ (b :: 0)),
+  have h : count b s = count b (count b s •ℕ (b ::ₘ 0)),
   { rw [singleton_coe, count_smul, ← singleton_coe, count_singleton, mul_one] },
   rw h, clear h,
   apply finset.sum_eq_single b,
@@ -1128,9 +1128,9 @@ end
 theorem exists_smul_of_dvd_count (s : multiset α) {k : ℕ} (h : ∀ (a : α), k ∣ multiset.count a s) :
   ∃ (u : multiset α), s = k •ℕ u :=
 begin
-  use ∑ a in s.to_finset, (s.count a / k) •ℕ (a :: 0),
-  have h₂ : ∑ (x : α) in s.to_finset, k •ℕ (count x s / k •ℕ (x :: 0)) =
-    ∑ (x : α) in s.to_finset, count x s •ℕ (x :: 0),
+  use ∑ a in s.to_finset, (s.count a / k) •ℕ (a ::ₘ 0),
+  have h₂ : ∑ (x : α) in s.to_finset, k •ℕ (count x s / k •ℕ (x ::ₘ 0)) =
+    ∑ (x : α) in s.to_finset, count x s •ℕ (x ::ₘ 0),
   { refine congr_arg s.to_finset.sum _,
     apply funext, intro x,
     rw [← mul_nsmul, nat.mul_div_cancel' (h x)] },

src/data/dfinsupp.lean

@@ -367,11 +367,11 @@ begin
         { left, rw H3, exact H1 },
         { left, exact H3 } },
       right, exact H2 },
-    have H3 : (⟦{to_fun := f, pre_support := i :: s, zero := H}⟧ : Π₀ i, β i)
+    have H3 : (⟦{to_fun := f, pre_support := i ::ₘ s, zero := H}⟧ : Π₀ i, β i)
       = ⟦{to_fun := f, pre_support := s, zero := H2}⟧,
     { exact quotient.sound (λ i, rfl) },
     rw H3, apply ih },
-  have H2 : p (erase i ⟦{to_fun := f, pre_support := i :: s, zero := H}⟧),
+  have H2 : p (erase i ⟦{to_fun := f, pre_support := i ::ₘ s, zero := H}⟧),
   { dsimp only [erase, quotient.lift_on_beta],
     have H2 : ∀ j, j ∈ s ∨ ite (j = i) 0 (f j) = 0,
     { intro j, cases H j with H2 H2,
@@ -380,11 +380,11 @@ begin
         { left, exact H3 } },
       right, split_ifs; [refl, exact H2] },
     have H3 : (⟦{to_fun := λ (j : ι), ite (j = i) 0 (f j),
-         pre_support := i :: s, zero := _}⟧ : Π₀ i, β i)
+         pre_support := i ::ₘ s, zero := _}⟧ : Π₀ i, β i)
       = ⟦{to_fun := λ (j : ι), ite (j = i) 0 (f j), pre_support := s, zero := H2}⟧ :=
       quotient.sound (λ i, rfl),
     rw H3, apply ih },
-  have H3 : single i _ + _ = (⟦{to_fun := f, pre_support := i :: s, zero := H}⟧ : Π₀ i, β i) :=
+  have H3 : single i _ + _ = (⟦{to_fun := f, pre_support := i ::ₘ s, zero := H}⟧ : Π₀ i, β i) :=
     single_add_erase,
   rw ← H3,
   change p (single i (f i) + _),

src/data/finmap.lean

@@ -314,7 +314,7 @@ lift_on s (λ t, ⟦insert a b t⟧) $
   insert a b ⟦s⟧ = ⟦s.insert a b⟧ := by simp [insert]
 
 theorem insert_entries_of_neg {a : α} {b : β a} {s : finmap β} : a ∉ s →
-  (insert a b s).entries = ⟨a, b⟩ :: s.entries :=
+  (insert a b s).entries = ⟨a, b⟩ ::ₘ s.entries :=
 induction_on s $ λ s h,
 by simp [insert_entries_of_neg (mt mem_to_finmap.1 h)]
 

src/data/finset/basic.lean

@@ -220,7 +220,7 @@ This differs from `insert a ∅` in that it does not require a `decidable_eq` in
 -/
 instance : has_singleton α (finset α) := ⟨λ a, ⟨{a}, nodup_singleton a⟩⟩
 
-@[simp] theorem singleton_val (a : α) : ({a} : finset α).1 = a :: 0 := rfl
+@[simp] theorem singleton_val (a : α) : ({a} : finset α).1 = a ::ₘ 0 := rfl
 
 @[simp] theorem mem_singleton {a b : α} : b ∈ ({a} : finset α) ↔ b = a := mem_singleton
 
@@ -264,15 +264,15 @@ singleton_subset_set_iff
 `insert a s` when it is defined, but unlike `insert a s` it does not require `decidable_eq α`,
 and the union is guaranteed to be disjoint.  -/
 def cons {α} (a : α) (s : finset α) (h : a ∉ s) : finset α :=
-⟨a :: s.1, multiset.nodup_cons.2 ⟨h, s.2⟩⟩
+⟨a ::ₘ s.1, multiset.nodup_cons.2 ⟨h, s.2⟩⟩
 
 @[simp] theorem mem_cons {α a s h b} : b ∈ @cons α a s h ↔ b = a ∨ b ∈ s :=
 by rcases s with ⟨⟨s⟩⟩; apply list.mem_cons_iff
 
-@[simp] theorem cons_val {a : α} {s : finset α} (h : a ∉ s) : (cons a s h).1 = a :: s.1 := rfl
+@[simp] theorem cons_val {a : α} {s : finset α} (h : a ∉ s) : (cons a s h).1 = a ::ₘ s.1 := rfl
 
-@[simp] theorem mk_cons {a : α} {s : multiset α} (h : (a :: s).nodup) :
-  (⟨a :: s, h⟩ : finset α) = cons a ⟨s, (multiset.nodup_cons.1 h).2⟩ (multiset.nodup_cons.1 h).1 :=
+@[simp] theorem mk_cons {a : α} {s : multiset α} (h : (a ::ₘ s).nodup) :
+  (⟨a ::ₘ s, h⟩ : finset α) = cons a ⟨s, (multiset.nodup_cons.1 h).2⟩ (multiset.nodup_cons.1 h).1 :=
 rfl
 
 @[simp] theorem nonempty_cons {a : α} {s : finset α} (h : a ∉ s) : (cons a s h).nonempty :=
@@ -305,10 +305,10 @@ theorem insert_def (a : α) (s : finset α) : insert a s = ⟨_, nodup_ndinsert
 
 @[simp] theorem insert_val (a : α) (s : finset α) : (insert a s).1 = ndinsert a s.1 := rfl
 
-theorem insert_val' (a : α) (s : finset α) : (insert a s).1 = erase_dup (a :: s.1) :=
+theorem insert_val' (a : α) (s : finset α) : (insert a s).1 = erase_dup (a ::ₘ s.1) :=
 by rw [erase_dup_cons, erase_dup_eq_self]; refl
 
-theorem insert_val_of_not_mem {a : α} {s : finset α} (h : a ∉ s) : (insert a s).1 = a :: s.1 :=
+theorem insert_val_of_not_mem {a : α} {s : finset α} (h : a ∉ s) : (insert a s).1 = a ::ₘ s.1 :=
 by rw [insert_val, ndinsert_of_not_mem h]
 
 @[simp] theorem mem_insert {a b : α} {s : finset α} : a ∈ insert b s ↔ a = b ∨ a ∈ s := mem_ndinsert
@@ -373,7 +373,7 @@ protected theorem induction {α : Type*} {p : finset α → Prop} [decidable_eq
   (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α}, a ∉ s → p s → p (insert a s)) : ∀ s, p s
 | ⟨s, nd⟩ := multiset.induction_on s (λ _, h₁) (λ a s IH nd, begin
     cases nodup_cons.1 nd with m nd',
-    rw [← (eq_of_veq _ : insert a (finset.mk s _) = ⟨a::s, nd⟩)],
+    rw [← (eq_of_veq _ : insert a (finset.mk s _) = ⟨a ::ₘ s, nd⟩)],
     { exact h₂ (by exact m) (IH nd') },
     { rw [insert_val, ndinsert_of_not_mem m] }
   end) nd
@@ -1215,7 +1215,7 @@ mem_erase_dup
 rfl
 
 @[simp] lemma to_finset_cons (a : α) (s : multiset α) :
-  to_finset (a :: s) = insert a (to_finset s) :=
+  to_finset (a ::ₘ s) = insert a (to_finset s) :=
 finset.eq_of_veq erase_dup_cons
 
 @[simp] lemma to_finset_add (s t : multiset α) :

src/data/finset/pi.lean

@@ -74,7 +74,7 @@ assume e₁ e₂ eq,
 begin
   apply eq_of_veq,
   rw ← multiset.erase_dup_eq_self.2 (pi (insert a s) t).2,
-  refine (λ s' (h : s' = a :: s.1), (_ : erase_dup (multiset.pi s' (λ a, (t a).1)) =
+  refine (λ s' (h : s' = a ::ₘ s.1), (_ : erase_dup (multiset.pi s' (λ a, (t a).1)) =
     erase_dup ((t a).1.bind $ λ b,
     erase_dup $ (multiset.pi s.1 (λ (a : α), (t a).val)).map $
       λ f a' h', multiset.pi.cons s.1 a b f a' (h ▸ h')))) _ (insert_val_of_not_mem ha),

src/data/finsupp/basic.lean

@@ -1320,8 +1320,8 @@ end
 calc f.to_multiset.count a = f.sum (λx n, (n •ℕ {x} : multiset α).count a) :
     (f.support.sum_hom $ multiset.count a).symm
   ... = f.sum (λx n, n * ({x} : multiset α).count a) : by simp only [multiset.count_smul]
-  ... = f.sum (λx n, n * (x :: 0 : multiset α).count a) : rfl
-  ... = f a * (a :: 0 : multiset α).count a : sum_eq_single _
+  ... = f.sum (λx n, n * (x ::ₘ 0 : multiset α).count a) : rfl
+  ... = f a * (a ::ₘ 0 : multiset α).count a : sum_eq_single _
     (λ a' _ H, by simp only [multiset.count_cons_of_ne (ne.symm H), multiset.count_zero, mul_zero])
     (λ H, by simp only [not_mem_support_iff.1 H, zero_mul])
   ... = f a : by simp only [multiset.count_singleton, mul_one]

src/data/fintype/basic.lean

@@ -387,7 +387,7 @@ instance : fintype punit := fintype.of_subsingleton punit.star
 
 @[simp] theorem fintype.card_punit : fintype.card punit = 1 := rfl
 
-instance : fintype bool := ⟨⟨tt::ff::0, by simp⟩, λ x, by cases x; simp⟩
+instance : fintype bool := ⟨⟨tt ::ₘ ff ::ₘ 0, by simp⟩, λ x, by cases x; simp⟩
 
 @[simp] theorem fintype.univ_bool : @univ bool _ = {tt, ff} := rfl
 
@@ -408,7 +408,7 @@ by classical; exact fintype.of_injective units.val units.ext
 /-- Given a finset on `α`, lift it to being a finset on `option α`
 using `option.some` and then insert `option.none`. -/
 def finset.insert_none (s : finset α) : finset (option α) :=
-⟨none :: s.1.map some, multiset.nodup_cons.2
+⟨none ::ₘ s.1.map some, multiset.nodup_cons.2
   ⟨by simp, multiset.nodup_map (λ a b, option.some.inj) s.2⟩⟩
 
 @[simp] theorem finset.mem_insert_none {s : finset α} : ∀ {o : option α},
@@ -660,7 +660,7 @@ instance plift.fintype (p : Prop) [decidable p] : fintype (plift p) :=
 ⟨if h : p then {⟨h⟩} else ∅, λ ⟨h⟩, by simp [h]⟩
 
 instance Prop.fintype : fintype Prop :=
-⟨⟨true::false::0, by simp [true_ne_false]⟩,
+⟨⟨true ::ₘ false ::ₘ 0, by simp [true_ne_false]⟩,
  classical.cases (by simp) (by simp)⟩
 
 instance subtype.fintype (p : α → Prop) [decidable_pred p] [fintype α] : fintype {x // p x} :=

src/data/multiset/antidiagonal.lean

@@ -53,9 +53,9 @@ by simp [powerset_aux']
 quotient.induction_on s $ λ l,
 by simp [powerset_aux']
 
-@[simp] theorem antidiagonal_zero : @antidiagonal α 0 = (0, 0)::0 := rfl
+@[simp] theorem antidiagonal_zero : @antidiagonal α 0 = (0, 0) ::ₘ 0 := rfl
 
-@[simp] theorem antidiagonal_cons (a : α) (s) : antidiagonal (a::s) =
+@[simp] theorem antidiagonal_cons (a : α) (s) : antidiagonal (a ::ₘ s) =
   map (prod.map id (cons a)) (antidiagonal s) +
   map (prod.map (cons a) id) (antidiagonal s) :=
 quotient.induction_on s $ λ l, begin