feat(data/set/finite): Align set.to_finset and `set.finite.to_finse…

…t` (#17959)

Match lemmas about `set.to_finset` and `set.finite.to_finset`. This mostly involves making sure we have all pairs of the form `set.to_finset_whatever`/`set.finite.to_finset_whatever`.

Also add a few lemmas and tag existing ones with simp.

src/algebra/big_operators/basic.lean

@@ -1679,7 +1679,7 @@ lemma disjoint_finset_sum_left {β : Type*} {i : finset β} {f : β → multiset
   multiset.disjoint (i.sum f) a ↔ ∀ b ∈ i, multiset.disjoint (f b) a :=
 begin
   convert (@disjoint_sum_left _ a) (map f i.val),
-  simp [finset.mem_def, and.congr_left_iff, iff_self],
+  simp [and.congr_left_iff, iff_self],
 end
 
 lemma disjoint_finset_sum_right {β : Type*} {i : finset β} {f : β → multiset α} {a : multiset α} :

src/analysis/analytic/inverse.lean

@@ -126,7 +126,7 @@ begin
     ext k,
     simp [h] },
   simp [formal_multilinear_series.comp, show n + 2 ≠ 1, by dec_trivial, A, finset.sum_union B,
-    apply_composition_ones, C, D],
+    apply_composition_ones, C, D, -set.to_finset_set_of],
 end
 
 /-! ### The right inverse of a formal multilinear series -/
@@ -196,7 +196,7 @@ begin
             = p 1 (λ (i : fin 1), q n v),
   { apply p.congr (composition.single_length hn) (λ j hj1 hj2, _),
     simp [apply_composition_single] },
-  simp [formal_multilinear_series.comp, A, finset.sum_union B, C],
+  simp [formal_multilinear_series.comp, A, finset.sum_union B, C, -set.to_finset_set_of],
 end
 
 lemma comp_right_inv_aux2
@@ -229,7 +229,7 @@ begin
       continuous_linear_equiv.coe_apply, continuous_multilinear_curry_fin1_symm_apply] },
   have N : 0 < n+2, by dec_trivial,
   simp [comp_right_inv_aux1 N, h, right_inv, lt_irrefl n, show n + 2 ≠ 1, by dec_trivial,
-        ← sub_eq_add_neg, sub_eq_zero, comp_right_inv_aux2],
+        ← sub_eq_add_neg, sub_eq_zero, comp_right_inv_aux2, -set.to_finset_set_of],
 end
 
 lemma right_inv_coeff (p : formal_multilinear_series 𝕜 E F) (i : E ≃L[𝕜] F) (n : ℕ) (hn : 2 ≤ n) :
@@ -244,7 +244,7 @@ begin
   ext v,
   have N : 0 < n + 2, by dec_trivial,
   have : (p 1) (λ (i : fin 1), 0) = 0 := continuous_multilinear_map.map_zero _,
-  simp [comp_right_inv_aux1 N, lt_irrefl n, this, comp_right_inv_aux2]
+  simp [comp_right_inv_aux1 N, lt_irrefl n, this, comp_right_inv_aux2, -set.to_finset_set_of],
 end
 
 /-! ### Coincidence of the left and the right inverse -/

src/analysis/locally_convex/weak_dual.lean

@@ -98,7 +98,7 @@ begin
     simp only [id.def],
     let U' := hU₁.to_finset,
     by_cases hU₃ : U.fst.nonempty,
-    { have hU₃' : U'.nonempty := hU₁.nonempty_to_finset.mpr hU₃,
+    { have hU₃' : U'.nonempty := hU₁.to_finset_nonempty.mpr hU₃,
       refine ⟨(U'.sup p).ball 0 $ U'.inf' hU₃' U.snd, p.basis_sets_mem _ $
         (finset.lt_inf'_iff _).2 $ λ y hy, hU₂ y $ (hU₁.mem_to_finset).mp hy, λ x hx y hy, _⟩,
       simp only [set.mem_preimage, set.mem_pi, mem_ball_zero_iff],

src/combinatorics/simple_graph/basic.lean

@@ -960,7 +960,7 @@ lemma degree_compl [fintype (Gᶜ.neighbor_set v)] [fintype V] :
 begin
   classical,
   rw [← card_neighbor_set_union_compl_neighbor_set G v, set.to_finset_union],
-  simp [card_disjoint_union (set.to_finset_disjoint_iff.mpr (compl_neighbor_set_disjoint G v))],
+  simp [card_disjoint_union (set.disjoint_to_finset.mpr (compl_neighbor_set_disjoint G v))],
 end
 
 instance incidence_set_fintype [decidable_eq V] : fintype (G.incidence_set v) :=
@@ -1197,7 +1197,7 @@ begin
   { rw finset.insert_subset,
     split,
     { simpa, },
-    { rw [neighbor_finset, set.to_finset_subset],
+    { rw [neighbor_finset, set.to_finset_subset_to_finset],
       exact G.common_neighbors_subset_neighbor_set_left _ _ } }
 end
 
@@ -1207,7 +1207,7 @@ begin
   simp only [common_neighbors_top_eq, ← set.to_finset_card, set.to_finset_diff],
   rw finset.card_sdiff,
   { simp [finset.card_univ, h], },
-  { simp only [set.to_finset_subset, set.subset_univ] },
+  { simp only [set.to_finset_subset_to_finset, set.subset_univ] },
 end
 
 end finite

src/data/finset/basic.lean

@@ -158,6 +158,7 @@ instance has_decidable_eq [decidable_eq α] : decidable_eq (finset α)
 instance : has_mem α (finset α) := ⟨λ a s, a ∈ s.1⟩
 
 theorem mem_def {a : α} {s : finset α} : a ∈ s ↔ a ∈ s.1 := iff.rfl
+@[simp] lemma mem_val {a : α} {s : finset α} : a ∈ s.1 ↔ a ∈ s := iff.rfl
 
 @[simp] theorem mem_mk {a : α} {s nd} : a ∈ @finset.mk α s nd ↔ a ∈ s := iff.rfl
 

src/data/finset/mul_antidiagonal.lean

@@ -62,11 +62,11 @@ by simp [mul_antidiagonal, and_rotate]
 
 @[to_additive] lemma mul_antidiagonal_mono_left (h : u ⊆ s) :
   mul_antidiagonal hu ht a ⊆ mul_antidiagonal hs ht a :=
-set.finite.to_finset_subset.2 $ set.mul_antidiagonal_mono_left h
+set.finite.to_finset_mono $ set.mul_antidiagonal_mono_left h
 
 @[to_additive] lemma mul_antidiagonal_mono_right (h : u ⊆ t) :
   mul_antidiagonal hs hu a ⊆ mul_antidiagonal hs ht a :=
-set.finite.to_finset_subset.2 $ set.mul_antidiagonal_mono_right h
+set.finite.to_finset_mono $ set.mul_antidiagonal_mono_right h
 
 @[simp, to_additive] lemma swap_mem_mul_antidiagonal :
   x.swap ∈ finset.mul_antidiagonal hs ht a ↔ x ∈ finset.mul_antidiagonal ht hs a :=

src/data/finset/pointwise.lean

@@ -1028,7 +1028,7 @@ t.zero_smul_subset.antisymm $ by simpa [mem_smul] using ht
 
 /-- A nonempty set is scaled by zero to the singleton set containing 0. -/
 lemma zero_smul_finset {s : finset β} (h : s.nonempty) : (0 : α) • s = (0 : finset β) :=
-coe_injective $ by simpa using set.zero_smul_set h
+coe_injective $ by simpa using @set.zero_smul_set α _ _ _ _ _ h
 
 lemma zero_smul_finset_subset (s : finset β) : (0 : α) • s ⊆ 0 :=
 image_subset_iff.2 $ λ x _, mem_zero.2 $ zero_smul α x

src/data/fintype/basic.lean

@@ -446,9 +446,6 @@ by cc
 @[simp] theorem mem_to_finset {s : set α} [fintype s] {a : α} : a ∈ s.to_finset ↔ a ∈ s :=
 by simp [to_finset]
 
-@[simp] theorem mem_to_finset_val {s : set α} [fintype s] {a : α} : a ∈ s.to_finset.1 ↔ a ∈ s :=
-mem_to_finset
-
 /-- Many `fintype` instances for sets are defined using an extensionally equal `finset`.
 Rewriting `s.to_finset` with `set.to_finset_of_finset` replaces the term with such a `finset`. -/
 theorem to_finset_of_finset {p : set α} (s : finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) :
@@ -472,51 +469,83 @@ by rw [←finset.coe_nonempty, coe_to_finset]
   s.to_finset = t.to_finset ↔ s = t :=
 ⟨λ h, by rw [←s.coe_to_finset, h, t.coe_to_finset], λ h, by simp [h]; congr⟩
 
-@[simp, mono] lemma to_finset_subset [fintype s] [fintype t] : s.to_finset ⊆ t.to_finset ↔ s ⊆ t :=
+@[mono]
+lemma to_finset_subset_to_finset [fintype s] [fintype t] : s.to_finset ⊆ t.to_finset ↔ s ⊆ t :=
 by simp [finset.subset_iff, set.subset_def]
 
-@[simp, mono] lemma to_finset_ssubset [fintype s] [fintype t] : s.to_finset ⊂ t.to_finset ↔ s ⊂ t :=
-by simp only [finset.ssubset_def, to_finset_subset, ssubset_def]
+@[simp] lemma to_finset_ssubset [fintype s] {t : finset α} : s.to_finset ⊂ t ↔ s ⊂ t :=
+by rw [←finset.coe_ssubset, coe_to_finset]
+
+@[simp] lemma subset_to_finset {s : finset α} [fintype t] : s ⊆ t.to_finset ↔ ↑s ⊆ t :=
+by rw [←finset.coe_subset, coe_to_finset]
+
+@[simp] lemma ssubset_to_finset {s : finset α} [fintype t] : s ⊂ t.to_finset ↔ ↑s ⊂ t :=
+by rw [←finset.coe_ssubset, coe_to_finset]
+
+@[mono]
+lemma to_finset_ssubset_to_finset [fintype s] [fintype t] : s.to_finset ⊂ t.to_finset ↔ s ⊂ t :=
+by simp only [finset.ssubset_def, to_finset_subset_to_finset, ssubset_def]
+
+@[simp] lemma to_finset_subset [fintype s] {t : finset α} : s.to_finset ⊆ t ↔ s ⊆ t :=
+by rw [←finset.coe_subset, coe_to_finset]
 
-@[simp] theorem to_finset_disjoint_iff {s t : set α} [fintype s] [fintype t] :
+alias to_finset_subset_to_finset ↔ _ to_finset_mono
+alias to_finset_ssubset_to_finset ↔ _ to_finset_strict_mono
+
+@[simp] lemma disjoint_to_finset [fintype s] [fintype t] :
   disjoint s.to_finset t.to_finset ↔ disjoint s t :=
 by simp only [←disjoint_coe, coe_to_finset]
 
-@[simp] lemma to_finset_inter {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∩ t : set α)]
-  [fintype s] [fintype t] : (s ∩ t).to_finset = s.to_finset ∩ t.to_finset :=
-by { ext, simp }
+section decidable_eq
+variables [decidable_eq α] (s t) [fintype s] [fintype t]
 
-@[simp] lemma to_finset_union {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∪ t : set α)]
-  [fintype s] [fintype t] : (s ∪ t).to_finset = s.to_finset ∪ t.to_finset :=
+@[simp] lemma to_finset_inter [fintype ↥(s ∩ t)] : (s ∩ t).to_finset = s.to_finset ∩ t.to_finset :=
 by { ext, simp }
 
-@[simp] lemma to_finset_diff {α : Type*} [decidable_eq α] (s t : set α) [fintype s] [fintype t]
-  [fintype (s \ t : set α)] : (s \ t).to_finset = s.to_finset \ t.to_finset :=
+@[simp] lemma to_finset_union [fintype ↥(s ∪ t)] : (s ∪ t).to_finset = s.to_finset ∪ t.to_finset :=
 by { ext, simp }
 
-lemma to_finset_ne_eq_erase {α : Type*} [decidable_eq α] [fintype α] (a : α)
-  [fintype {x : α | x ≠ a}] : {x : α | x ≠ a}.to_finset = finset.univ.erase a :=
+@[simp] lemma to_finset_diff [fintype ↥(s \ t)] : (s \ t).to_finset = s.to_finset \ t.to_finset :=
 by { ext, simp }
 
-@[simp] theorem to_finset_compl [decidable_eq α] [fintype α] (s : set α) [fintype s] [fintype ↥sᶜ] :
-  (sᶜ).to_finset = s.to_finsetᶜ :=
+@[simp] lemma to_finset_symm_diff [fintype ↥(s ∆ t)] :
+  (s ∆ t).to_finset = s.to_finset ∆ t.to_finset :=
+by { ext, simp [mem_symm_diff, finset.mem_symm_diff] }
+
+@[simp] lemma to_finset_compl [fintype α] [fintype ↥sᶜ] : sᶜ.to_finset = s.to_finsetᶜ :=
 by { ext, simp }
 
-@[simp] lemma to_finset_eq_univ [fintype α] {s : set α} [fintype s] :
-  s.to_finset = finset.univ ↔ s = set.univ :=
-by rw [← coe_inj, coe_to_finset, coe_univ]
+end decidable_eq
+
+/- TODO The `↥` circumvents an elaboration bug. See comment on `set.to_finset_univ`. -/
+@[simp] lemma to_finset_empty [fintype ↥(∅ : set α)] : (∅ : set α).to_finset = ∅ := by { ext, simp }
 
-/- TODO Without the coercion arrow (`↥`) there is an elaboration bug;
+/- TODO Without the coercion arrow (`↥`) there is an elaboration bug in the following two;
 it essentially infers `fintype.{v} (set.univ.{u} : set α)` with `v` and `u` distinct.
 Reported in leanprover-community/lean#672 -/
-@[simp] lemma to_finset_univ [fintype ↥(set.univ : set α)] [fintype α] :
+@[simp] lemma to_finset_univ [fintype α] [fintype ↥(set.univ : set α)] :
   (set.univ : set α).to_finset = finset.univ :=
-to_finset_eq_univ.2 rfl
+by { ext, simp }
+
+@[simp] lemma to_finset_eq_empty [fintype s] : s.to_finset = ∅ ↔ s = ∅ :=
+by rw [←to_finset_empty, to_finset_inj]
+
+@[simp] lemma to_finset_eq_univ [fintype α] [fintype s] : s.to_finset = finset.univ ↔ s = univ :=
+by rw [← coe_inj, coe_to_finset, coe_univ]
+
+@[simp] lemma to_finset_set_of [fintype α] (p : α → Prop) [decidable_pred p] [fintype {x | p x}] :
+  {x | p x}.to_finset = finset.univ.filter p :=
+by { ext, simp }
 
 @[simp] lemma to_finset_ssubset_univ [fintype α] {s : set α} [fintype s] :
   s.to_finset ⊂ finset.univ ↔ s ⊂ univ :=
 by rw [← coe_ssubset, coe_to_finset, coe_univ]
 
+@[simp]
+lemma to_finset_image [decidable_eq β] (f : α → β) (s : set α) [fintype s] [fintype (f '' s)] :
+  (f '' s).to_finset = s.to_finset.image f :=
+finset.coe_injective $ by simp
+
 @[simp] lemma to_finset_range [decidable_eq α] [fintype β] (f : β → α) [fintype (set.range f)] :
   (set.range f).to_finset = finset.univ.image f :=
 by { ext, simp }
@@ -673,12 +702,6 @@ instance Prop.fintype : fintype Prop :=
 instance subtype.fintype (p : α → Prop) [decidable_pred p] [fintype α] : fintype {x // p x} :=
 fintype.subtype (univ.filter p) (by simp)
 
-@[simp] lemma set.to_finset_eq_empty_iff {s : set α} [fintype s] : s.to_finset = ∅ ↔ s = ∅ :=
-by simp only [ext_iff, set.ext_iff, set.mem_to_finset, not_mem_empty, set.mem_empty_iff_false]
-
-@[simp] lemma set.to_finset_empty : (∅ : set α).to_finset = ∅ :=
-set.to_finset_eq_empty_iff.mpr rfl
-
 /-- A set on a fintype, when coerced to a type, is a fintype. -/
 def set_fintype [fintype α] (s : set α) [decidable_pred (∈ s)] : fintype s :=
 subtype.fintype (λ x, x ∈ s)
@@ -809,7 +832,7 @@ theorem quotient.fin_choice_eq {ι : Type*} [decidable_eq ι] [fintype ι]
 begin
   let q, swap, change quotient.lift_on q _ _ = _,
   have : q = ⟦λ i h, f i⟧,
-  { dsimp [q],
+  { dsimp only [q],
     exact quotient.induction_on
       (@finset.univ ι _).1 (λ l, quotient.fin_choice_aux_eq _ _) },
   simp [this], exact setoid.refl _

src/data/nat/nth.lean

@@ -83,7 +83,7 @@ begin
   apply finset.card_erase_of_mem,
   rw [nth, set.finite.mem_to_finset],
   apply Inf_mem,
-  rwa [←hp''.nonempty_to_finset, ←finset.card_pos, hk],
+  rwa [←hp''.to_finset_nonempty, ←finset.card_pos, hk],
 end
 
 lemma nth_set_card {n : ℕ} (hp : (set_of p).finite)
@@ -93,10 +93,10 @@ begin
   obtain hn | hn := le_or_lt n hp.to_finset.card,
   { exact nth_set_card_aux p hp _ hn },
   rw nat.sub_eq_zero_of_le hn.le,
-  simp only [finset.card_eq_zero, set.finite_to_finset_eq_empty_iff, ←set.subset_empty_iff],
+  simp only [finset.card_eq_zero, set.finite.to_finset_eq_empty, ←set.subset_empty_iff],
   convert_to _ ⊆ {i : ℕ | p i ∧ ∀ (k : ℕ), k < hp.to_finset.card → nth p k < i},
   { symmetry,
-    rw [←set.finite_to_finset_eq_empty_iff, ←finset.card_eq_zero,
+    rw [←set.finite.to_finset_eq_empty, ←finset.card_eq_zero,
         ←nat.sub_self hp.to_finset.card],
     { apply nth_set_card_aux p hp _ le_rfl },
     { exact hp.subset (λ x hx, hx.1) } },
@@ -108,7 +108,7 @@ lemma nth_set_nonempty_of_lt_card {n : ℕ} (hp : (set_of p).finite) (hlt: n < h
 begin
   have hp': {i : ℕ | p i ∧ ∀ (k : ℕ), k < n → nth p k < i}.finite,
   { exact hp.subset (λ x hx, hx.1) },
-  rw [←hp'.nonempty_to_finset, ←finset.card_pos, nth_set_card p hp],
+  rw [←hp'.to_finset_nonempty, ←finset.card_pos, nth_set_card p hp],
   exact nat.sub_pos_of_lt hlt,
 end