chore(data/list/cycle): Add basic simp lemmas + minor golfing (#13533)

src/data/list/cycle.lean

@@ -440,14 +440,15 @@ lemma coe_cons_eq_coe_append (l : list α) (a : α) : (↑(a :: l) : cycle α) =
 quot.sound ⟨1, by rw [rotate_cons_succ, rotate_zero]⟩
 
 /-- The unique empty cycle. -/
-def nil : cycle α := ↑([] : list α)
+def nil : cycle α := ([] : list α)
 
 @[simp] lemma coe_nil : ↑([] : list α) = @nil α :=
 rfl
 
 @[simp] lemma coe_eq_nil (l : list α) : (l : cycle α) = nil ↔ l = [] :=
 coe_eq_coe.trans is_rotated_nil_iff
 
+/-- For consistency with `list.has_emptyc`. -/
 instance : has_emptyc (cycle α) := ⟨nil⟩
 
 @[simp] lemma empty_eq : ∅ = @nil α :=
@@ -462,7 +463,7 @@ quotient.induction_on' s $ λ l, by { apply list.rec_on l; simp, assumption' }
 
 /-- For `x : α`, `s : cycle α`, `x ∈ s` indicates that `x` occurs at least once in `s`. -/
 def mem (a : α) (s : cycle α) : Prop :=
-quot.lift_on s (λ l, a ∈ l) (λ l₁ l₂ (e : l₁ ~r l₂), propext $ e.mem_iff)
+quot.lift_on s (λ l, a ∈ l) (λ l₁ l₂ e, propext $ e.mem_iff)
 
 instance : has_mem α (cycle α) := ⟨mem⟩
 
@@ -480,7 +481,7 @@ quotient.rec_on_subsingleton' s (λ l, list.decidable_mem x l)
 
 /-- Reverse a `s : cycle α` by reversing the underlying `list`. -/
 def reverse (s : cycle α) : cycle α :=
-quot.map reverse (λ l₁ l₂ (e : l₁ ~r l₂), e.reverse) s
+quot.map reverse (λ l₁ l₂, is_rotated.reverse) s
 
 @[simp] lemma reverse_coe (l : list α) : (l : cycle α).reverse = l.reverse :=
 rfl
@@ -496,7 +497,7 @@ rfl
 
 /-- The length of the `s : cycle α`, which is the number of elements, counting duplicates. -/
 def length (s : cycle α) : ℕ :=
-quot.lift_on s length (λ l₁ l₂ (e : l₁ ~r l₂), e.perm.length_eq)
+quot.lift_on s length (λ l₁ l₂ e, e.perm.length_eq)
 
 @[simp] lemma length_coe (l : list α) : length (l : cycle α) = l.length :=
 rfl
@@ -563,7 +564,7 @@ end
 
 /-- The `s : cycle α` contains no duplicates. -/
 def nodup (s : cycle α) : Prop :=
-quot.lift_on s nodup (λ l₁ l₂ (e : l₁ ~r l₂), propext $ e.nodup_iff)
+quot.lift_on s nodup (λ l₁ l₂ e, propext $ e.nodup_iff)
 
 @[simp] lemma nodup_nil : nodup (@nil α) :=
 nodup_nil
@@ -595,14 +596,20 @@ end
 The `s : cycle α` as a `multiset α`.
 -/
 def to_multiset (s : cycle α) : multiset α :=
-quotient.lift_on' s (λ l, (l : multiset α)) (λ l₁ l₂ (h : l₁ ~r l₂), multiset.coe_eq_coe.mpr h.perm)
+quotient.lift_on' s coe (λ l₁ l₂ h, multiset.coe_eq_coe.mpr h.perm)
 
 @[simp] lemma coe_to_multiset (l : list α) : (l : cycle α).to_multiset = l :=
 rfl
 
-@[simp] lemma nil_to_multiset : nil.to_multiset = (∅ : multiset α) :=
+@[simp] lemma nil_to_multiset : nil.to_multiset = (0 : multiset α) :=
 rfl
 
+@[simp] lemma card_to_multiset (s : cycle α) : s.to_multiset.card = s.length :=
+quotient.induction_on' s (by simp)
+
+@[simp] lemma to_multiset_eq_nil {s : cycle α} : s.to_multiset = 0 ↔ s = cycle.nil :=
+quotient.induction_on' s (by simp)
+
 /-- The lift of `list.map`. -/
 def map {β : Type*} (f : α → β) : cycle α → cycle β :=
 quotient.map' (list.map f) $ λ l₁ l₂ h, h.map _
@@ -614,13 +621,13 @@ rfl
 rfl
 
 @[simp] lemma map_eq_nil {β : Type*} (f : α → β) (s : cycle α) : map f s = nil ↔ s = nil :=
-quotient.induction_on' s $ λ l, by simp
+quotient.induction_on' s (by simp)
 
 /-- The `multiset` of lists that can make the cycle. -/
 def lists (s : cycle α) : multiset (list α) :=
 quotient.lift_on' s
   (λ l, (l.cyclic_permutations : multiset (list α))) $
-  λ l₁ l₂ (h : l₁ ~r l₂), by simpa using h.cyclic_permutations.perm
+  λ l₁ l₂ h, by simpa using h.cyclic_permutations.perm
 
 @[simp] lemma lists_coe (l : list α) : lists (l : cycle α) = ↑l.cyclic_permutations :=
 rfl
@@ -651,7 +658,7 @@ instance {s : cycle α} : decidable (nontrivial s) :=
 quot.rec_on_subsingleton s decidable_nontrivial_coe
 
 instance {s : cycle α} : decidable (nodup s) :=
-quot.rec_on_subsingleton s (λ (l : list α), list.nodup_decidable l)
+quot.rec_on_subsingleton s list.nodup_decidable
 
 instance fintype_nodup_cycle [fintype α] : fintype {s : cycle α // s.nodup} :=
 fintype.of_surjective (λ (l : {l : list α // l.nodup}), ⟨l.val, by simpa using l.prop⟩)
@@ -667,24 +674,30 @@ fintype.subtype (((finset.univ : finset {s : cycle α // s.nodup}).map
 def to_finset (s : cycle α) : finset α :=
 s.to_multiset.to_finset
 
+@[simp] theorem to_finset_to_multiset (s : cycle α) : s.to_multiset.to_finset = s.to_finset :=
+rfl
+
 @[simp] lemma coe_to_finset (l : list α) : (l : cycle α).to_finset = l.to_finset :=
 rfl
 
 @[simp] lemma nil_to_finset : (@nil α).to_finset = ∅ :=
 rfl
 
+@[simp] lemma to_finset_eq_nil {s : cycle α} : s.to_finset = ∅ ↔ s = cycle.nil :=
+quotient.induction_on' s (by simp)
+
 /-- Given a `s : cycle α` such that `nodup s`, retrieve the next element after `x ∈ s`. -/
 def next : Π (s : cycle α) (hs : nodup s) (x : α) (hx : x ∈ s), α :=
 λ s, quot.hrec_on s (λ l hn x hx, next l x hx)
-  (λ l₁ l₂ (h : l₁ ~r l₂),
+  (λ l₁ l₂ h,
   function.hfunext (propext h.nodup_iff) (λ h₁ h₂ he, function.hfunext rfl
     (λ x y hxy, function.hfunext (propext (by simpa [eq_of_heq hxy] using h.mem_iff))
     (λ hm hm' he', heq_of_eq (by simpa [eq_of_heq hxy] using is_rotated_next_eq h h₁ _)))))
 
 /-- Given a `s : cycle α` such that `nodup s`, retrieve the previous element before `x ∈ s`. -/
 def prev : Π (s : cycle α) (hs : nodup s) (x : α) (hx : x ∈ s), α :=
 λ s, quot.hrec_on s (λ l hn x hx, prev l x hx)
-  (λ l₁ l₂ (h : l₁ ~r l₂),
+  (λ l₁ l₂ h,
   function.hfunext (propext h.nodup_iff) (λ h₁ h₂ he, function.hfunext rfl
     (λ x y hxy, function.hfunext (propext (by simpa [eq_of_heq hxy] using h.mem_iff))
     (λ hm hm' he', heq_of_eq (by simpa [eq_of_heq hxy] using is_rotated_prev_eq h h₁ _)))))

src/data/multiset/basic.lean

@@ -56,7 +56,7 @@ instance inhabited_multiset : inhabited (multiset α)  := ⟨0⟩
 @[simp] theorem coe_nil_eq_zero : (@nil α : multiset α) = 0 := rfl
 @[simp] theorem empty_eq_zero : (∅ : multiset α) = 0 := rfl
 
-theorem coe_eq_zero (l : list α) : (l : multiset α) = 0 ↔ l = [] :=
+@[simp] theorem coe_eq_zero (l : list α) : (l : multiset α) = 0 ↔ l = [] :=
 iff.trans coe_eq_coe perm_nil
 
 /-! ### `multiset.cons` -/