chore(data/{lists,multiset}/*): More dot notation (#12876)

Rename many `list` and `multiset` lemmas to make them eligible to dot notation. Also add a few aliases to `↔` lemmas for even more dot notation.

Renames

Author: YaelDillies

src/algebra/squarefree.lean

@@ -349,7 +349,7 @@ lemma divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) :
     (unique_factorization_monoid.normalized_factors n).to_finset.powerset.val.map
       (λ x, x.val.prod) :=
 begin
-  rw multiset.nodup_ext (finset.nodup _) (multiset.nodup_map_on _ (finset.nodup _)),
+  rw (finset.nodup _).ext ((finset.nodup _).map_on _),
   { intro a,
     simp only [multiset.mem_filter, id.def, multiset.mem_map, finset.filter_val, ← finset.mem_def,
       mem_divisors],

src/combinatorics/simple_graph/connectivity.lean

@@ -487,7 +487,7 @@ by split; intro h; convert h.reverse; simp
 
 lemma is_path.of_append_left {u v w : V} {p : G.walk u v} {q : G.walk v w} :
   (p.append q).is_path → p.is_path :=
-by { simp only [is_path_def, support_append], exact list.nodup_of_nodup_append_left }
+by { simp only [is_path_def, support_append], exact list.nodup.of_append_left }
 
 lemma is_path.of_append_right {u v w : V} {p : G.walk u v} {q : G.walk v w}
   (h : (p.append q).is_path) : q.is_path :=

src/data/equiv/list.lean

@@ -236,8 +236,7 @@ lemma raise_lower : ∀ {l n}, list.sorted (≤) (n :: l) → raise (lower l n)
 | []       n h := rfl
 | (m :: l) n h :=
   have n ≤ m, from list.rel_of_sorted_cons h _ (l.mem_cons_self _),
-  by simp [raise, lower, tsub_add_cancel_of_le this,
-           raise_lower (list.sorted_of_sorted_cons h)]
+  by simp [raise, lower, tsub_add_cancel_of_le this, raise_lower h.of_cons]
 
 lemma raise_chain : ∀ l n, list.chain (≤) n (raise l n)
 | []       n := list.chain.nil
@@ -284,7 +283,7 @@ lemma raise_lower' : ∀ {l n}, (∀ m ∈ l, n ≤ m) → list.sorted (<) l →
 | (m :: l) n h₁ h₂ :=
   have n ≤ m, from h₁ _ (l.mem_cons_self _),
   by simp [raise', lower', tsub_add_cancel_of_le this, raise_lower'
-    (list.rel_of_sorted_cons h₂ : ∀ a ∈ l, m < a) (list.sorted_of_sorted_cons h₂)]
+    (list.rel_of_sorted_cons h₂ : ∀ a ∈ l, m < a) h₂.of_cons]
 
 lemma raise'_chain : ∀ l {m n}, m < n → list.chain (<) m (raise' l n)
 | []       m n h := list.chain.nil

src/data/fin_enum.lean

@@ -59,7 +59,7 @@ open function
 by simp [to_list]; existsi equiv α x; simp
 
 @[simp] lemma nodup_to_list [fin_enum α] : list.nodup (to_list α) :=
-by simp [to_list]; apply list.nodup_map; [apply equiv.injective, apply list.nodup_fin_range]
+by simp [to_list]; apply list.nodup.map; [apply equiv.injective, apply list.nodup_fin_range]
 
 /-- create a `fin_enum` instance using a surjection -/
 def of_surjective {β} (f : β → α) [decidable_eq α] [fin_enum β] (h : surjective f) : fin_enum α :=

src/data/finset/basic.lean

@@ -186,7 +186,7 @@ instance decidable_mem' [decidable_eq α] (a : α) (s : finset α) :
 
 /-! ### extensionality -/
 theorem ext_iff {s₁ s₂ : finset α} : s₁ = s₂ ↔ ∀ a, a ∈ s₁ ↔ a ∈ s₂ :=
-val_inj.symm.trans $ nodup_ext s₁.2 s₂.2
+val_inj.symm.trans $ s₁.nodup.ext s₂.nodup
 
 @[ext]
 theorem ext {s₁ s₂ : finset α} : (∀ a, a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂ :=
@@ -548,9 +548,9 @@ section decidable_eq
 variables [decidable_eq α] {s t u v : finset α} {a b : α}
 
 /-- `insert a s` is the set `{a} ∪ s` containing `a` and the elements of `s`. -/
-instance : has_insert α (finset α) := ⟨λ a s, ⟨_, nodup_ndinsert a s.2⟩⟩
+instance : has_insert α (finset α) := ⟨λ a s, ⟨_, s.2.ndinsert a⟩⟩
 
-theorem insert_def (a : α) (s : finset α) : insert a s = ⟨_, nodup_ndinsert a s.2⟩ := rfl
+lemma insert_def (a : α) (s : finset α) : insert a s = ⟨_, s.2.ndinsert a⟩ := rfl
 
 @[simp] theorem insert_val (a : α) (s : finset α) : (insert a s).1 = ndinsert a s.1 := rfl
 
@@ -715,10 +715,10 @@ end
 /-! ### Lattice structure -/
 
 /-- `s ∪ t` is the set such that `a ∈ s ∪ t` iff `a ∈ s` or `a ∈ t`. -/
-instance : has_union (finset α) := ⟨λ s t, ⟨_, nodup_ndunion s.1 t.2⟩⟩
+instance : has_union (finset α) := ⟨λ s t, ⟨_, t.2.ndunion s.1⟩⟩
 
 /-- `s ∩ t` is the set such that `a ∈ s ∩ t` iff `a ∈ s` and `a ∈ t`. -/
-instance : has_inter (finset α) := ⟨λ s t, ⟨_, nodup_ndinter t.1 s.2⟩⟩
+instance : has_inter (finset α) := ⟨λ s t, ⟨_, s.2.ndinter t.1⟩⟩
 
 instance : lattice (finset α) :=
 { sup          := (∪),
@@ -993,14 +993,14 @@ lemma inter_subset_ite (s s' : finset α) (P : Prop) [decidable P] :
 
 /-- `erase s a` is the set `s - {a}`, that is, the elements of `s` which are
   not equal to `a`. -/
-def erase (s : finset α) (a : α) : finset α := ⟨_, nodup_erase_of_nodup a s.2⟩
+def erase (s : finset α) (a : α) : finset α := ⟨_, s.2.erase a⟩
 
 @[simp] theorem erase_val (s : finset α) (a : α) : (erase s a).1 = s.1.erase a := rfl
 
 @[simp] theorem mem_erase {a b : α} {s : finset α} : a ∈ erase s b ↔ a ≠ b ∧ a ∈ s :=
-mem_erase_iff_of_nodup s.2
+s.2.mem_erase_iff
 
-theorem not_mem_erase (a : α) (s : finset α) : a ∉ erase s a := mem_erase_of_nodup s.2
+lemma not_mem_erase (a : α) (s : finset α) : a ∉ erase s a := s.2.not_mem_erase
 
 -- While this can be solved by `simp`, this lemma is eligible for `dsimp`
 @[nolint simp_nf, simp] theorem erase_empty (a : α) : erase ∅ a = ∅ := rfl
@@ -1395,8 +1395,7 @@ section filter
 variables (p q : α → Prop) [decidable_pred p] [decidable_pred q]
 
 /-- `filter p s` is the set of elements of `s` that satisfy `p`. -/
-def filter (s : finset α) : finset α :=
-⟨_, nodup_filter p s.2⟩
+def filter (s : finset α) : finset α := ⟨_, s.2.filter p⟩
 
 @[simp] theorem filter_val (s : finset α) : (filter p s).1 = s.1.filter p := rfl
 
@@ -1817,8 +1816,7 @@ open function
 
 /-- When `f` is an embedding of `α` in `β` and `s` is a finset in `α`, then `s.map f` is the image
 finset in `β`. The embedding condition guarantees that there are no duplicates in the image. -/
-def map (f : α ↪ β) (s : finset α) : finset β :=
-⟨s.1.map f, nodup_map f.2 s.2⟩
+def map (f : α ↪ β) (s : finset α) : finset β := ⟨s.1.map f, s.2.map f.2⟩
 
 @[simp] theorem map_val (f : α ↪ β) (s : finset α) : (map f s).1 = s.1.map f := rfl
 
@@ -1977,8 +1975,7 @@ instance [can_lift β α] : can_lift (finset β) (finset α) :=
     begin
       rintro ⟨⟨l⟩, hd : l.nodup⟩ hl,
       lift l to list α using hl,
-      refine ⟨⟨l, list.nodup_of_nodup_map _ hd⟩, ext $ λ a, _⟩,
-      simp
+      exact ⟨⟨l, hd.of_map _⟩, ext $ λ a, by simp⟩,
     end }
 
 lemma image_congr (h : (s : set α).eq_on f g) : finset.image f s = finset.image g s :=
@@ -2014,8 +2011,7 @@ theorem image_to_finset [decidable_eq α] {s : multiset α} :
   s.to_finset.image f = (s.map f).to_finset :=
 ext $ λ _, by simp only [mem_image, multiset.mem_to_finset, exists_prop, multiset.mem_map]
 
-theorem image_val_of_inj_on (H : set.inj_on f s) : (image f s).1 = s.1.map f :=
-(nodup_map_on H s.2).dedup
+lemma image_val_of_inj_on (H : set.inj_on f s) : (image f s).1 = s.1.map f := (s.2.map_on H).dedup
 
 @[simp] lemma image_id [decidable_eq α] : s.image id = s :=
 ext $ λ _, by simp only [mem_image, exists_prop, id, exists_eq_right]

src/data/finset/fin.lean

@@ -35,7 +35,7 @@ set.eq_univ_of_forall mem_fin_range
 /-- Given a finset `s` of `ℕ` contained in `{0,..., n-1}`, the corresponding finset in `fin n`
 is `s.attach_fin h` where `h` is a proof that all elements of `s` are less than `n`. -/
 def attach_fin (s : finset ℕ) {n : ℕ} (h : ∀ m ∈ s, m < n) : finset (fin n) :=
-⟨s.1.pmap (λ a ha, ⟨a, ha⟩) h, multiset.nodup_pmap (λ _ _ _ _, fin.veq_of_eq) s.2⟩
+⟨s.1.pmap (λ a ha, ⟨a, ha⟩) h, s.nodup.pmap $ λ _ _ _ _, fin.veq_of_eq⟩
 
 @[simp] lemma mem_attach_fin {n : ℕ} {s : finset ℕ} (h : ∀ m ∈ s, m < n) {a : fin n} :
   a ∈ s.attach_fin h ↔ (a : ℕ) ∈ s :=

src/data/finset/noncomm_prod.lean

@@ -318,7 +318,7 @@ begin
   obtain ⟨tl, tl', rfl⟩ := exists_list_nodup_eq t,
   rw list.disjoint_to_finset_iff_disjoint at h,
   simp [sl', tl', noncomm_prod_to_finset, ←list.prod_append, ←list.to_finset_append,
-        list.nodup_append_of_nodup sl' tl' h]
+    sl'.append tl' h]
 end
 
 @[protected, to_additive]

src/data/finset/option.lean

@@ -54,7 +54,7 @@ order_embedding.of_map_le_iff (λ s, cons none (s.map embedding.some) $ by simp)
   cons_subset_cons.trans map_subset_map
 
 /-⟨none ::ₘ s.1.map some, multiset.nodup_cons.2
-  ⟨by simp, multiset.nodup_map (λ a b, option.some.inj) s.2⟩⟩-/
+  ⟨by simp, s.nodup.map $ λ a b, option.some.inj⟩⟩-/
 
 @[simp] theorem mem_insert_none {s : finset α} : ∀ {o : option α},
   o ∈ s.insert_none ↔ ∀ a ∈ o, a ∈ s

src/data/finset/pi.lean

@@ -28,7 +28,7 @@ variables {δ : α → Type*} [decidable_eq α]
 finset `s.pi t` of all functions defined on elements of `s` taking values in `t a` for `a ∈ s`.
 Note that the elements of `s.pi t` are only partially defined, on `s`. -/
 def pi (s : finset α) (t : Πa, finset (δ a)) : finset (Πa∈s, δ a) :=
-⟨s.1.pi (λ a, (t a).1), nodup_pi s.2 (λ a _, (t a).2)⟩
+⟨s.1.pi (λ a, (t a).1), s.nodup.pi $ λ a _, (t a).nodup⟩
 
 @[simp] lemma pi_val (s : finset α) (t : Πa, finset (δ a)) :
   (s.pi t).1 = s.1.pi (λ a, (t a).1) := rfl
@@ -80,8 +80,7 @@ begin
       λ f a' h', multiset.pi.cons s.1 a b f a' (h ▸ h')))) _ (insert_val_of_not_mem ha),
   subst s', rw pi_cons,
   congr, funext b,
-  rw multiset.nodup.dedup,
-  exact multiset.nodup_map (multiset.pi_cons_injective ha) (pi s t).2,
+  exact ((pi s t).nodup.map $ multiset.pi_cons_injective ha).dedup.symm,
 end
 
 lemma pi_singletons {β : Type*} (s : finset α) (f : α → β) :

src/data/finset/powerset.lean

@@ -19,10 +19,8 @@ section powerset
 
 /-- When `s` is a finset, `s.powerset` is the finset of all subsets of `s` (seen as finsets). -/
 def powerset (s : finset α) : finset (finset α) :=
-⟨s.1.powerset.pmap finset.mk
-  (λ t h, nodup_of_le (mem_powerset.1 h) s.2),
- nodup_pmap (λ a ha b hb, congr_arg finset.val)
-   (nodup_powerset.2 s.2)⟩
+⟨s.1.powerset.pmap finset.mk $ λ t h, nodup_of_le (mem_powerset.1 h) s.nodup,
+ s.nodup.powerset.pmap $ λ a ha b hb, congr_arg finset.val⟩
 
 @[simp] theorem mem_powerset {s t : finset α} : s ∈ powerset t ↔ s ⊆ t :=
 by cases s; simp only [powerset, mem_mk, mem_pmap, mem_powerset, exists_prop, exists_eq_right];
@@ -138,10 +136,8 @@ section powerset_len
 /-- Given an integer `n` and a finset `s`, then `powerset_len n s` is the finset of subsets of `s`
 of cardinality `n`. -/
 def powerset_len (n : ℕ) (s : finset α) : finset (finset α) :=
-⟨(s.1.powerset_len n).pmap finset.mk
-  (λ t h, nodup_of_le (mem_powerset_len.1 h).1 s.2),
- nodup_pmap (λ a ha b hb, congr_arg finset.val)
-   (nodup_powerset_len s.2)⟩
+⟨(s.1.powerset_len n).pmap finset.mk $ λ t h, nodup_of_le (mem_powerset_len.1 h).1 s.2,
+ s.2.powerset_len.pmap $ λ a ha b hb, congr_arg finset.val⟩
 
 /-- **Formula for the Number of Combinations** -/
 theorem mem_powerset_len {n} {s t : finset α} :