refactor(data/set/finite): reorganize and put emphasis on fintype instances (#14136)

I went through `data/set/finite` and reorganized it by rough topic (and moved some lemmas to their proper homes; closes #11177). Two important parts of this module are (1) `fintype` instances for various set constructions and (2) ways to create `set.finite` terms. This change puts the module closer to following a design where the `set.finite` terms are created in a formulaic way from the `fintype` instances. One tool for this is a `set.finite_of_fintype` constructor, which lets typeclass inference do most of the work.

Included in this commit is changing `set.infinite` to be protected so that it does not conflict with `infinite`.

Author: kmill

archive/100-theorems-list/83_friendship_graphs.lean

@@ -76,7 +76,7 @@ theorem adj_matrix_sq_of_ne {v w : V} (hvw : v ≠ w) :
   ((G.adj_matrix R) ^ 2) v w = 1 :=
 begin
   rw [sq, ← nat.cast_one, ← hG hvw],
-  simp [common_neighbors, neighbor_finset_eq_filter, finset.filter_filter, finset.filter_inter,
+  simp [common_neighbors, neighbor_finset_eq_filter, finset.filter_filter,
     and_comm, ← neighbor_finset_def],
 end
 

src/analysis/locally_convex/weak_dual.lean

@@ -100,7 +100,7 @@ begin
     simp only [id.def],
     let U' := hU₁.to_finset,
     by_cases hU₃ : U.fst.nonempty,
-    { have hU₃' : U'.nonempty := (set.finite.to_finset.nonempty hU₁).mpr hU₃,
+    { have hU₃' : U'.nonempty := hU₁.nonempty_to_finset.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/configuration.lean

@@ -435,11 +435,11 @@ begin
   classical,
   have h1 : fintype.card {q // q ≠ p} + 1 = fintype.card P,
   { apply (eq_tsub_iff_add_eq_of_le (nat.succ_le_of_lt (fintype.card_pos_iff.mpr ⟨p⟩))).mp,
-    convert (fintype.card_subtype_compl).trans (congr_arg _ (fintype.card_subtype_eq p)) },
+    convert (fintype.card_subtype_compl _).trans (congr_arg _ (fintype.card_subtype_eq p)) },
   have h2 : ∀ l : {l : L // p ∈ l}, fintype.card {q // q ∈ l.1 ∧ q ≠ p} = order P L,
   { intro l,
     rw [←fintype.card_congr (equiv.subtype_subtype_equiv_subtype_inter _ _),
-        fintype.card_subtype_compl, ←nat.card_eq_fintype_card],
+      fintype.card_subtype_compl (λ (x : subtype (∈ l.val)), x.val = p), ←nat.card_eq_fintype_card],
     refine tsub_eq_of_eq_add ((point_count_eq P l.1).trans _),
     rw ← fintype.card_subtype_eq (⟨p, l.2⟩ : {q : P // q ∈ l.1}),
     simp_rw subtype.ext_iff_val },

src/combinatorics/simple_graph/basic.lean

@@ -755,7 +755,7 @@ by { ext, simp }
 
 lemma neighbor_finset_compl [decidable_eq V] [decidable_rel G.adj] (v : V) :
   Gᶜ.neighbor_finset v = (G.neighbor_finset v)ᶜ \ {v} :=
-by simp only [neighbor_finset, neighbor_set_compl, set.to_finset_sdiff, set.to_finset_compl,
+by simp only [neighbor_finset, neighbor_set_compl, set.to_finset_diff, set.to_finset_compl,
     set.to_finset_singleton]
 
 @[simp]
@@ -917,17 +917,17 @@ begin
   { rw finset.insert_subset,
     split,
     { simpa, },
-    { rw [neighbor_finset, ← set.subset_iff_to_finset_subset],
+    { rw [neighbor_finset, set.to_finset_mono],
       exact G.common_neighbors_subset_neighbor_set_left _ _ } }
 end
 
 lemma card_common_neighbors_top [decidable_eq V] {v w : V} (h : v ≠ w) :
   fintype.card ((⊤ : simple_graph V).common_neighbors v w) = fintype.card V - 2 :=
 begin
-  simp only [common_neighbors_top_eq, ← set.to_finset_card, set.to_finset_sdiff],
+  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.subset_iff_to_finset_subset, set.subset_univ] },
+  { simp only [set.to_finset_mono, set.subset_univ] },
 end
 
 end finite

src/combinatorics/simple_graph/strongly_regular.lean

@@ -134,7 +134,7 @@ lemma is_SRG_with.card_common_neighbors_eq_of_adj_compl (h : G.is_SRG_with n k 
   fintype.card ↥(Gᶜ.common_neighbors v w) = n - (2 * k - μ) - 2 :=
 begin
   simp only [←set.to_finset_card, common_neighbors, set.to_finset_inter, neighbor_set_compl,
-    set.to_finset_sdiff, set.to_finset_singleton, set.to_finset_compl, ←neighbor_finset_def],
+    set.to_finset_diff, set.to_finset_singleton, set.to_finset_compl, ←neighbor_finset_def],
   simp_rw compl_neighbor_finset_sdiff_inter_eq,
   have hne : v ≠ w := ne_of_adj _ ha,
   rw compl_adj at ha,
@@ -153,7 +153,7 @@ lemma is_SRG_with.card_common_neighbors_eq_of_not_adj_compl (h : G.is_SRG_with n
   fintype.card ↥(Gᶜ.common_neighbors v w) = n - (2 * k - ℓ) :=
 begin
   simp only [←set.to_finset_card, common_neighbors, set.to_finset_inter, neighbor_set_compl,
-    set.to_finset_sdiff, set.to_finset_singleton, set.to_finset_compl, ←neighbor_finset_def],
+    set.to_finset_diff, set.to_finset_singleton, set.to_finset_compl, ←neighbor_finset_def],
   simp only [not_and, not_not, compl_adj] at hna,
   have h2' := hna hn,
   simp_rw [compl_neighbor_finset_sdiff_inter_eq, sdiff_compl_neighbor_finset_inter_eq h2'],

src/data/fintype/basic.lean

@@ -641,6 +641,13 @@ 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
 
+/-- Membership of a set with a `fintype` instance is decidable.
+
+Using this as an instance leads to potential loops with `subtype.fintype` under certain decidability
+assumptions, so it should only be declared a local instance. -/
+def decidable_mem_of_fintype [decidable_eq α] (s : set α) [fintype s] (a) : decidable (a ∈ s) :=
+decidable_of_iff _ mem_to_finset
+
 -- We use an arbitrary `[fintype s]` instance here,
 -- not necessarily coming from a `[fintype α]`.
 @[simp]
@@ -667,9 +674,46 @@ by simp only [finset.ssubset_def, to_finset_mono, ssubset_def]
   disjoint s.to_finset t.to_finset ↔ disjoint s t :=
 by simp only [disjoint_iff_disjoint_coe, coe_to_finset]
 
+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 }
+
+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 :=
+by { ext, 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 :=
+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 :=
+by { ext, simp }
+
 theorem to_finset_compl [decidable_eq α] [fintype α] (s : set α) [fintype s] [fintype ↥sᶜ] :
   (sᶜ).to_finset = s.to_finsetᶜ :=
-by { ext a, simp }
+by { ext, simp }
+
+/- TODO Without the coercion arrow (`↥`) there is an elaboration bug;
+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 α] :
+  (set.univ : set α).to_finset = finset.univ :=
+by { ext, 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 }
+
+/- TODO The `↥` circumvents an elaboration bug. See comment on `set.to_finset_univ`. -/
+lemma to_finset_singleton (a : α) [fintype ↥({a} : set α)] : ({a} : set α).to_finset = {a} :=
+by { ext, simp }
+
+/- TODO The `↥` circumvents an elaboration bug. See comment on `set.to_finset_univ`. -/
+@[simp] lemma to_finset_insert [decidable_eq α] {a : α} {s : set α}
+  [fintype ↥(insert a s : set α)] [fintype s] :
+  (insert a s).to_finset = insert a s.to_finset :=
+by { ext, simp }
 
 lemma filter_mem_univ_eq_to_finset [fintype α] (s : set α) [fintype s] [decidable_pred (∈ s)] :
   finset.univ.filter (∈ s) = s.to_finset :=
@@ -1168,23 +1212,12 @@ 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)
 
-/- TODO Without the coercion arrow (`↥`) there is an elaboration bug;
-it essentially infers `fintype.{v} (set.univ.{u} : set α)` with `v` and `u` distinct.
-Reported in leanprover-community/lean#672 -/
-@[simp] lemma set.to_finset_univ [fintype ↥(set.univ : set α)] [fintype α] :
-  (set.univ : set α).to_finset = finset.univ :=
-by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] }
-
 @[simp] lemma set.to_finset_eq_empty_iff {s : set α} [fintype s] : s.to_finset = ∅ ↔ s = ∅ :=
-by simp [ext_iff, set.ext_iff]
+by simp only [ext_iff, set.ext_iff, set.mem_to_finset, not_mem_empty, set.mem_empty_eq]
 
 @[simp] lemma set.to_finset_empty : (∅ : set α).to_finset = ∅ :=
 set.to_finset_eq_empty_iff.mpr rfl
 
-@[simp] lemma set.to_finset_range [decidable_eq α] [fintype β] (f : β → α) [fintype (set.range f)] :
-  (set.range f).to_finset = finset.univ.image f :=
-by simp [ext_iff]
-
 /-- 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)
@@ -1412,6 +1445,26 @@ begin
   simp
 end
 
+@[simp]
+lemma fintype.card_subtype_compl [fintype α]
+  (p : α → Prop) [fintype {x // p x}] [fintype {x // ¬ p x}] :
+  fintype.card {x // ¬ p x} = fintype.card α - fintype.card {x // p x} :=
+begin
+  classical,
+  rw [fintype.card_of_subtype (set.to_finset pᶜ), set.to_finset_compl p, finset.card_compl,
+      fintype.card_of_subtype (set.to_finset p)];
+  intro; simp only [set.mem_to_finset, set.mem_compl_eq]; refl,
+end
+
+/-- If two subtypes of a fintype have equal cardinality, so do their complements. -/
+lemma fintype.card_compl_eq_card_compl [fintype α]
+  (p q : α → Prop)
+  [fintype {x // p x}] [fintype {x // ¬ p x}]
+  [fintype {x // q x}] [fintype {x // ¬ q x}]
+  (h : fintype.card {x // p x} = fintype.card {x // q x}) :
+  fintype.card {x // ¬ p x} = fintype.card {x // ¬ q x} :=
+by simp only [fintype.card_subtype_compl, h]
+
 theorem fintype.card_quotient_le [fintype α] (s : setoid α) [decidable_rel ((≈) : α → α → Prop)] :
   fintype.card (quotient s) ≤ fintype.card α :=
 fintype.card_le_of_surjective _ (surjective_quotient_mk _)

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 [←set.finite.to_finset.nonempty hp'', ←finset.card_pos, hk],
+  rwa [←hp''.nonempty_to_finset, ←finset.card_pos, hk],
 end
 
 lemma nth_set_card {n : ℕ} (hp : (set_of p).finite)
@@ -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'^.to_finset.nonempty, ←finset.card_pos, nth_set_card p hp],
+  rw [←hp'.nonempty_to_finset, ←finset.card_pos, nth_set_card p hp],
   exact nat.sub_pos_of_lt hlt,
 end