feat(data/sym/basic): add fill_mem, append_mem and supporting lem…

…mas (#16486)

Add lemmas for membership of fill and append, with supporting coercion and casting lemmas.

src/data/sym/basic.lean

@@ -53,7 +53,7 @@ local attribute [instance] vector.perm.is_setoid
 
 namespace sym
 
-variables {α β : Type*} {n : ℕ} {s : sym α n} {a b : α}
+variables {α β : Type*} {n n' m : ℕ} {s : sym α n} {a b : α}
 
 lemma coe_injective : injective (coe : sym α n → multiset α) := subtype.coe_injective
 
@@ -117,10 +117,12 @@ s.1.decidable_mem _
 @[simp]
 lemma mem_mk (a : α) (s : multiset α) (h : s.card = n) : a ∈ mk s h ↔ a ∈ s := iff.rfl
 
-@[simp] lemma mem_cons {a b : α} {s : sym α n} : a ∈ b ::ₛ s ↔ a = b ∨ a ∈ s :=
+@[simp] lemma mem_cons : a ∈ b ::ₛ s ↔ a = b ∨ a ∈ s :=
 multiset.mem_cons
 
-lemma mem_cons_of_mem {a b : α} {s : sym α n} (h : a ∈ s) : a ∈ b ::ₛ s :=
+@[simp] lemma mem_coe : a ∈ (s : multiset α) ↔ a ∈ s := iff.rfl
+
+lemma mem_cons_of_mem (h : a ∈ s) : a ∈ b ::ₛ s :=
 multiset.mem_cons_of_mem h
 
 @[simp] lemma mem_cons_self (a : α) (s : sym α n) : a ∈ a ::ₛ s :=
@@ -324,36 +326,46 @@ protected def cast {n m : ℕ} (h : n = m) : sym α n ≃ sym α m :=
 
 @[simp] lemma cast_rfl : sym.cast rfl s = s := subtype.ext rfl
 
-@[simp] lemma cast_cast {n n' n'' : ℕ} (s : sym α n) (h : n = n') (h' : n' = n'') :
+@[simp] lemma cast_cast {n'' : ℕ} (h : n = n') (h' : n' = n'') :
   sym.cast h' (sym.cast h s) = sym.cast (h.trans h') s := rfl
 
-@[simp] lemma coe_cast {n m : ℕ} (h : n = m) (s : sym α n) :
-  (sym.cast h s : multiset α) = s := rfl
+@[simp] lemma coe_cast (h : n = m) : (sym.cast h s : multiset α) = s := rfl
+
+@[simp] lemma mem_cast (h : n = m) : a ∈ sym.cast h s ↔ a ∈ s := iff.rfl
 
 /-- Append a pair of `sym` terms. -/
-def append {n n' : ℕ} (s : sym α n) (s' : sym α n') : sym α (n + n') :=
+def append (s : sym α n) (s' : sym α n') : sym α (n + n') :=
 ⟨s.1 + s'.1, by simp_rw [← s.2, ← s'.2, map_add]⟩
 
-@[simp] lemma append_inj_right {n n' : ℕ} (s : sym α n) (t t' : sym α n') :
+@[simp] lemma append_inj_right (s : sym α n) {t t' : sym α n'} :
   s.append t = s.append t' ↔ t = t' :=
 subtype.ext_iff.trans $ (add_right_inj _).trans subtype.ext_iff.symm
 
-@[simp] lemma append_inj_left {n n' : ℕ} (s s' : sym α n) (t : sym α n') :
+@[simp] lemma append_inj_left {s s' : sym α n} (t : sym α n') :
   s.append t = s'.append t ↔ s = s' :=
 subtype.ext_iff.trans $ (add_left_inj _).trans subtype.ext_iff.symm
 
-lemma append_comm {n n' : ℕ} (s : sym α n) (s' : sym α n') :
+lemma append_comm (s : sym α n') (s' : sym α n') :
   s.append s' = sym.cast (add_comm _ _) (s'.append s) :=
 by { ext, simp [append, add_comm], }
 
+@[simp, norm_cast] lemma coe_append (s : sym α n') (s' : sym α n') :
+  (s.append s' : multiset α) = s + s' := rfl
+
+lemma mem_append_iff {s' : sym α m} : a ∈ s.append s' ↔ a ∈ s ∨ a ∈ s' := multiset.mem_add
+
 /-- Fill a term `m : sym α (n - i)` with `i` copies of `a` to obtain a term of `sym α n`.
 This is a convenience wrapper for `m.append (repeat a i)` that adjusts the term using `sym.cast`. -/
 def fill (a : α) (i : fin (n + 1)) (m : sym α (n - i)) : sym α n :=
 sym.cast (nat.sub_add_cancel i.is_le) (m.append (repeat a i))
 
+lemma mem_fill_iff (a b : α) (i : fin (n + 1)) (s : sym α (n - i)) :
+  a ∈ sym.fill b i s ↔ ((i : ℕ) ≠ 0 ∧ a = b) ∨ a ∈ s :=
+by rw [fill, mem_cast, mem_append_iff, or_comm, mem_repeat]
+
 /-- Remove every `a` from a given `sym α n`.
 Yields the number of copies `i` and a term of `sym α (n - i)`. -/
-def filter_ne [decidable_eq α] (a : α) {n : ℕ} (m : sym α n) : Σ i : fin (n + 1), sym α (n - i) :=
+def filter_ne [decidable_eq α] (a : α) (m : sym α n) : Σ i : fin (n + 1), sym α (n - i) :=
 ⟨⟨m.1.count a, (multiset.count_le_card _ _).trans_lt $ by rw [m.2, nat.lt_succ_iff]⟩,
   m.1.filter ((≠) a), eq_tsub_of_add_eq $ eq.trans begin
     rw [← multiset.countp_eq_card_filter, add_comm],