[Merged by Bors] - feat(data/sym): Provide API for data.sym

src/data/multiset/basic.lean

@@ -586,6 +586,20 @@ by simp only [repeat_succ, singleton_eq_cons, eq_self_iff_true, repeat_zero, con
 
 theorem eq_of_mem_repeat {a b : α} {n} : b ∈ repeat a n → b = a := eq_of_mem_repeat
 
+lemma repeat_left_injective (n : ℕ) (h : n ≠ 0) : function.injective (λ a : α, repeat a n) :=
+begin
+  intros a b x,
+  simp only at x,
+  apply @eq_of_mem_repeat _ b a n,
+  cases n,
+  { exact false.elim (h rfl) },
+  { rw [x.symm, repeat_succ],
+    exact mem_cons_self a (repeat a n) },
+end
+
+@[simp] lemma repeat_left_inj (a b : α) (n : ℕ) (h : n ≠ 0) : repeat a n = repeat b n ↔ a = b :=
+(repeat_left_injective n h).eq_iff
+
 theorem eq_repeat' {a : α} {s : multiset α} : s = repeat a s.card ↔ ∀ b ∈ s, b = a :=
 quot.induction_on s $ λ l, iff.trans ⟨λ h,
   (perm_repeat.1 $ (quotient.exact h)), congr_arg coe⟩ eq_repeat'

src/data/sym/basic.lean

@@ -116,6 +116,9 @@ begin
   exact h,
 end
 
+def erase [decidable_eq α] (s : sym α (n + 1)) (a : α) (h : a ∈ s) : sym α n :=
+⟨s.val.erase a, (multiset.card_erase_of_mem h).trans $ s.property.symm ▸ n.pred_succ⟩
+
 /--
 Another definition of the nth symmetric power, using vectors modulo permutations. (See `sym`.)
 -/
@@ -150,4 +153,97 @@ instance inhabited_sym' [inhabited α] (n : ℕ) : inhabited (sym' α n) :=
 
 end inhabited
 
+instance has_zero : has_zero (sym α 0) := ⟨⟨0, rfl⟩⟩
+instance has_emptyc : has_emptyc (sym α 0) := ⟨0⟩
+
+instance subsingleton {n : ℕ} [subsingleton α] : subsingleton (sym α n) :=
+⟨begin
+  rintros ⟨a, ha⟩ ⟨b, hb⟩,
+  simp only [subtype.mk.inj_eq],
+  induction a using multiset.case_strong_induction_on with k hk ih generalizing n b,
+  { rw [ha.symm, multiset.card_zero] at hb, exact (multiset.card_eq_zero.mp hb).symm, },
+  { cases n,
+    { exact false.elim (multiset.cons_ne_zero (multiset.card_eq_zero.mp ha)) },
+    { by_cases hzero : b = 0,
+      { rw [hzero, multiset.card_zero] at hb,
+        exact false.elim (nat.succ_ne_zero n hb.symm) },
+      { have hmem := multiset.exists_mem_of_ne_zero hzero,
+        rcases hmem with ⟨r, hr⟩,
+        cases multiset.exists_cons_of_mem hr,
+        rw h,
+        have heq := @ih hk rfl.ge n w begin
+          rw multiset.card_cons at ha,
+          refine nat.succ.inj ha,
+        end begin
+          rw [h, multiset.card_cons] at hb,
+          refine nat.succ.inj hb,
+        end,
+        rw [heq, subsingleton.elim k r] } } }
+end⟩
+
+instance unique (n : ℕ) [unique α] : unique (sym α n) := unique.mk' _
+
+instance is_empty (n : ℕ) [is_empty α] : is_empty (sym α n.succ) :=
+⟨begin
+  intro h,
+  rw sym at h,
+  refine is_empty.exists_iff.mp (@multiset.exists_mem_of_ne_zero _ h.val _),
+  intro y,
+  have z := h.property,
+  rw [y, multiset.card_zero] at z,
+  exact false.elim (nat.succ_ne_zero n z.symm),
+end⟩
+
+def repeat (a : α) (n : ℕ) : sym α n := ⟨multiset.repeat a n, multiset.card_repeat _ _⟩
+
+lemma repeat_left_injective (n : ℕ) (h : n ≠ 0) : function.injective (λ x : α, repeat x n) :=
+begin
+  intros a b x,
+  simp only [repeat, subtype.mk.inj_eq] at x,
+  exact (multiset.repeat_left_inj a b n h).mp x,
+end
+
+lemma repeat_left_inj (a b : α) (n : ℕ) (h : n ≠ 0) : repeat a n = repeat b n ↔ a = b :=
+(repeat_left_injective n h).eq_iff
+
+instance nontrivial (n : ℕ) [nontrivial α] : nontrivial (sym α (n + 1)) :=
+(repeat_left_injective n.succ n.succ_ne_zero).nontrivial
+
+def map {α β : Type*} {n : ℕ} (f : α → β) (x : sym α n) : sym β n :=
+⟨x.val.map f, by simpa [multiset.card_map] using x.property⟩
+
+@[simp] lemma mem_map {α β : Type*} {n : ℕ} {f : α → β} {b : β} {l : sym α n} :
+  b ∈ sym.map f l ↔ ∃ a, a ∈ l ∧ f a = b := multiset.mem_map
+
+@[simp] lemma map_id {α : Type*} {n : ℕ} (s : sym α n) : sym.map id s = s :=
+by simp [sym.map, subtype.mk.inj_eq]
+
+@[simp] lemma map_map {α β γ : Type*} {n : ℕ} (g : β → γ) (f : α → β) (s : sym α n) :
+  sym.map g (sym.map f s) = sym.map (g ∘ f) s :=
+by simp [sym.map, subtype.mk.inj_eq]
+
+@[simp] lemma map_zero {α β : Type*} (f : α → β) :
+  sym.map f (0 : sym α 0) = (0 : sym β 0) :=
+begin
+  rw sym.has_zero,
+  simp only [sym.map, multiset.map_zero],
+  rw sym.has_zero,
+  simp only [subtype.mk_eq_mk],
+end
+
+@[simp] lemma map_cons {α β : Type*} {n : ℕ} (f : α → β) (a : α) (s : sym α n) :
+  sym.map f (a::s) = (f a)::sym.map f s :=
+begin
+  simp only [map, subtype.mk.inj_eq, cons],
+  convert multiset.map_cons f a s.val,
+  cases s,
+  rw sym.cons,
+end
+
+def equiv_congr (β : Type u) (h : α ≃ β) : sym α n ≃ sym β n :=
+{ to_fun := sym.map h,
+  inv_fun := sym.map h.symm,
+  left_inv := λ x, by simp only [equiv.symm_comp_self, map_id, map_map],
+  right_inv := λ x, by simp only [equiv.self_comp_symm, map_id, map_map] }
+
 end sym

src/data/sym/sym2.lean

@@ -496,4 +496,13 @@ end
 
 end decidable
 
+instance subsingleton [g : subsingleton α] : subsingleton (sym2 α) :=
+(equiv_sym α).injective.subsingleton
+
+instance unique [unique α] : unique (sym2 α) := unique.mk' _
+
+instance is_empty [is_empty α] : is_empty (sym2 α) := (equiv_sym α).is_empty
+
+instance nontrivial [nontrivial α] : nontrivial (sym2 α) := diag_injective.nontrivial
+
 end sym2