feat(src/data/*): lemmas about emptiness for finset/multiset/vector c…

…oercions (#16113)

Adds basic lemmas about whether the result of `to_list` is empty for various data structures.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/algebra/big_operators/multiset.lean

@@ -56,13 +56,13 @@ lemma prod_cons (a : α) (s) : prod (a ::ₘ s) = a * prod s := foldr_cons _ _ _
 
 @[simp, to_additive]
 lemma prod_erase [decidable_eq α] (h : a ∈ s) : a * (s.erase a).prod = s.prod :=
-by rw [← s.coe_to_list, coe_erase, coe_prod, coe_prod, list.prod_erase ((s.mem_to_list a).2 h)]
+by rw [← s.coe_to_list, coe_erase, coe_prod, coe_prod, list.prod_erase (mem_to_list.2 h)]
 
 @[simp, to_additive]
 lemma prod_map_erase [decidable_eq ι] {a : ι} (h : a ∈ m) :
   f a * ((m.erase a).map f).prod = (m.map f).prod :=
 by rw [← m.coe_to_list, coe_erase, coe_map, coe_map, coe_prod, coe_prod,
-  list.prod_map_erase f ((m.mem_to_list a).2 h)]
+  list.prod_map_erase f (mem_to_list.2 h)]
 
 @[simp, to_additive]
 lemma prod_singleton (a : α) : prod {a} = a :=

src/algebra/periodic.lean

@@ -85,7 +85,7 @@ end
 lemma _root_.multiset.periodic_prod [has_add α] [comm_monoid β]
   (s : multiset (α → β)) (hs : ∀ f ∈ s, periodic f c) :
   periodic s.prod c :=
-s.prod_to_list ▸ s.to_list.periodic_prod $ λ f hf, hs f $ (multiset.mem_to_list f s).mp hf
+s.prod_to_list ▸ s.to_list.periodic_prod $ λ f hf, hs f $ multiset.mem_to_list.mp hf
 
 @[to_additive]
 lemma _root_.finset.periodic_prod [has_add α] [comm_monoid β]

src/data/finset/basic.lean

@@ -2463,18 +2463,29 @@ finset.val_inj.1 (multiset.dedup_map_dedup_eq _ _).symm
 section to_list
 
 /-- Produce a list of the elements in the finite set using choice. -/
-@[reducible] noncomputable def to_list (s : finset α) : list α := s.1.to_list
+noncomputable def to_list (s : finset α) : list α := s.1.to_list
 
 lemma nodup_to_list (s : finset α) : s.to_list.nodup :=
 by { rw [to_list, ←multiset.coe_nodup, multiset.coe_to_list], exact s.nodup }
 
-@[simp] lemma mem_to_list {a : α} (s : finset α) : a ∈ s.to_list ↔ a ∈ s :=
-by { rw [to_list, ←multiset.mem_coe, multiset.coe_to_list], exact iff.rfl }
+@[simp] lemma mem_to_list {a : α} {s : finset α} : a ∈ s.to_list ↔ a ∈ s := mem_to_list
 
-@[simp] lemma to_list_empty : (∅ : finset α).to_list = [] := by simp [to_list]
+@[simp] lemma to_list_eq_nil {s : finset α} : s.to_list = [] ↔ s = ∅ :=
+to_list_eq_nil.trans val_eq_zero
+
+@[simp] lemma empty_to_list {s : finset α} : s.to_list.empty ↔ s = ∅ :=
+list.empty_iff_eq_nil.trans to_list_eq_nil
+
+@[simp] lemma to_list_empty : (∅ : finset α).to_list = [] := to_list_eq_nil.mpr rfl
+
+lemma nonempty.to_list_ne_nil {s : finset α} (hs : s.nonempty) : s.to_list ≠ [] :=
+mt to_list_eq_nil.mp hs.ne_empty
+
+lemma nonempty.not_empty_to_list {s : finset α} (hs : s.nonempty) : ¬s.to_list.empty :=
+mt empty_to_list.mp hs.ne_empty
 
 @[simp, norm_cast]
-lemma coe_to_list (s : finset α) : (s.to_list : multiset α) = s.val := by { classical, ext, simp }
+lemma coe_to_list (s : finset α) : (s.to_list : multiset α) = s.val := s.val.coe_to_list
 
 @[simp] lemma to_list_to_finset [decidable_eq α] (s : finset α) : s.to_list.to_finset = s :=
 by { ext, simp }

src/data/multiset/basic.lean

@@ -59,6 +59,9 @@ instance inhabited_multiset : inhabited (multiset α)  := ⟨0⟩
 @[simp] theorem coe_eq_zero (l : list α) : (l : multiset α) = 0 ↔ l = [] :=
 iff.trans coe_eq_coe perm_nil
 
+lemma coe_eq_zero_iff_empty (l : list α) : (l : multiset α) = 0 ↔ l.empty :=
+iff.trans (coe_eq_zero l) (empty_iff_eq_nil).symm
+
 /-! ### `multiset.cons` -/
 
 /-- `cons a s` is the multiset which contains `s` plus one more
@@ -296,19 +299,21 @@ end subset
 section to_list
 
 /-- Produces a list of the elements in the multiset using choice. -/
-@[reducible] noncomputable def to_list {α : Type*} (s : multiset α) :=
-classical.some (quotient.exists_rep s)
-
-@[simp] lemma to_list_zero {α : Type*} : (multiset.to_list 0 : list α) = [] :=
-(multiset.coe_eq_zero _).1 (classical.some_spec (quotient.exists_rep multiset.zero))
+noncomputable def to_list (s : multiset α) := s.out'
 
 @[simp, norm_cast]
-lemma coe_to_list {α : Type*} (s : multiset α) : (s.to_list : multiset α) = s :=
-classical.some_spec (quotient.exists_rep _)
+lemma coe_to_list (s : multiset α) : (s.to_list : multiset α) = s := s.out_eq'
 
-@[simp]
-lemma mem_to_list {α : Type*} (a : α) (s : multiset α) : a ∈ s.to_list ↔ a ∈ s :=
-by rw [←multiset.mem_coe, multiset.coe_to_list]
+@[simp] lemma to_list_eq_nil {s : multiset α} : s.to_list = [] ↔ s = 0 :=
+by rw [← coe_eq_zero, coe_to_list]
+
+@[simp] lemma empty_to_list {s : multiset α} : s.to_list.empty ↔ s = 0 :=
+empty_iff_eq_nil.trans to_list_eq_nil
+
+@[simp] lemma to_list_zero : (multiset.to_list 0 : list α) = [] := to_list_eq_nil.mpr rfl
+
+@[simp] lemma mem_to_list {a : α} {s : multiset α} : a ∈ s.to_list ↔ a ∈ s :=
+by rw [← mem_coe, coe_to_list]
 
 end to_list
 

src/data/vector/basic.lean

@@ -143,6 +143,8 @@ by simp only [←cons_head_tail, eq_iff_true_of_subsingleton]
   tail (of_fn f) = of_fn (λ i, f i.succ) :=
 (of_fn_nth _).symm.trans $ by { congr, funext i, cases i, simp, }
 
+@[simp] theorem to_list_empty (v : vector α 0) : v.to_list = [] := list.length_eq_zero.mp v.2
+
 /-- The list that makes up a `vector` made up of a single element,
 retrieved via `to_list`, is equal to the list of that single element. -/
 @[simp] lemma to_list_singleton (v : vector α 1) : v.to_list = [v.head] :=
@@ -152,6 +154,12 @@ begin
              and_self, singleton_tail]
 end
 
+@[simp] lemma empty_to_list_eq_ff (v : vector α (n + 1)) : v.to_list.empty = ff :=
+match v with | ⟨a :: as, _⟩ := rfl end
+
+lemma not_empty_to_list (v : vector α (n + 1)) : ¬ v.to_list.empty :=
+by simp only [empty_to_list_eq_ff, coe_sort_ff, not_false_iff]
+
 /-- Mapping under `id` does not change a vector. -/
 @[simp] lemma map_id {n : ℕ} (v : vector α n) : vector.map id v = v :=
   vector.eq _ _ (by simp only [list.map_id, vector.to_list_map])

src/data/vector/mem.lean

@@ -27,7 +27,7 @@ by simp only [list.mem_iff_nth_le, fin.exists_iff, vector.nth_eq_nth_le];
 
 lemma not_mem_nil : a ∉ (vector.nil : vector α 0).to_list := id
 
-@[simp] lemma not_mem_zero (v : vector α 0) : a ∉ v.to_list :=
+lemma not_mem_zero (v : vector α 0) : a ∉ v.to_list :=
 (vector.eq_nil v).symm ▸ (not_mem_nil a)
 
 lemma mem_cons_iff (v : vector α n) :

src/field_theory/splitting_field.lean

@@ -293,7 +293,7 @@ else or.inr $ λ p hp hdp, begin
   { refine (hp.2.1 $ is_unit_of_dvd_unit hd _).elim,
     exact is_unit_C.2 ((leading_coeff_ne_zero.2 hf0).is_unit.map i) },
   { obtain ⟨q, hq, hd⟩ := hp.dvd_prod_iff.1 hd,
-    obtain ⟨a, ha, rfl⟩ := multiset.mem_map.1 ((multiset.mem_to_list _ _).1 hq),
+    obtain ⟨a, ha, rfl⟩ := multiset.mem_map.1 (multiset.mem_to_list.1 hq),
     rw degree_eq_degree_of_associated ((hp.dvd_prime_iff_associated $ prime_X_sub_C a).1 hd),
     exact degree_X_sub_C a },
 end

src/number_theory/class_number/admissible_absolute_value.lean

@@ -96,7 +96,7 @@ begin
     { intros i j h, ext, exact list.nodup_iff_nth_le_inj.mp (finset.nodup_to_list _) _ _ _ _ h },
     have : ∀ i h, (finset.univ.filter (λ x, t x = s)).to_list.nth_le i h ∈
       finset.univ.filter (λ x, t x = s),
-    { intros i h, exact (finset.mem_to_list _).mp (list.nth_le_mem _ _ _) },
+    { intros i h, exact finset.mem_to_list.mp (list.nth_le_mem _ _ _) },
     obtain ⟨_, h₀⟩ := finset.mem_filter.mp (this i₀ _),
     obtain ⟨_, h₁⟩ := finset.mem_filter.mp (this i₁ _),
     exact h₀.trans h₁.symm },