feat(tactic/derive_fintype): derive fintype instances (#3772)

This adds a `@[derive fintype]` implementation, like so:
```
@[derive fintype]
inductive foo (α : Type)
| A : α → foo
| B : α → α → foo
| C : α × α → foo
| D : foo
```

Author: digama0

src/data/finset/basic.lean

@@ -251,6 +251,31 @@ by rw [coe_singleton, set.singleton_subset_iff]
   {a} ⊆ s ↔ a ∈ s :=
 singleton_subset_set_iff
 
+/-! ### cons -/
+
+/-- `cons a s h` is the set `{a} ∪ s` containing `a` and the elements of `s`. It is the same as
+`insert a s` when it is defined, but unlike `insert a s` it does not require `decidable_eq α`,
+and the union is guaranteed to be disjoint.  -/
+def cons {α} (a : α) (s : finset α) (h : a ∉ s) : finset α :=
+⟨a :: s.1, multiset.nodup_cons.2 ⟨h, s.2⟩⟩
+
+@[simp] theorem mem_cons {α a s h b} : b ∈ @cons α a s h ↔ b = a ∨ b ∈ s :=
+by rcases s with ⟨⟨s⟩⟩; apply list.mem_cons_iff
+
+@[simp] theorem cons_val {a : α} {s : finset α} (h : a ∉ s) : (cons a s h).1 = a :: s.1 := rfl
+
+/-! ### disjoint union -/
+
+/-- `disj_union s t h` is the set such that `a ∈ disj_union s t h` iff `a ∈ s` or `a ∈ t`.
+It is the same as `s ∪ t`, but it does not require decidable equality on the type. The hypothesis
+ensures that the sets are disjoint. -/
+def disj_union {α} (s t : finset α) (h : ∀ a ∈ s, a ∉ t) : finset α :=
+⟨s.1 + t.1, multiset.nodup_add.2 ⟨s.2, t.2, h⟩⟩
+
+@[simp] theorem mem_disj_union {α s t h a} :
+  a ∈ @disj_union α s t h ↔ a ∈ s ∨ a ∈ t :=
+by rcases s with ⟨⟨s⟩⟩; rcases t with ⟨⟨t⟩⟩; apply list.mem_append
+
 /-! ### insert -/
 section decidable_eq
 variables [decidable_eq α]
@@ -276,6 +301,9 @@ mem_ndinsert_of_mem h
 theorem mem_of_mem_insert_of_ne {a b : α} {s : finset α} (h : b ∈ insert a s) : b ≠ a → b ∈ s :=
 (mem_insert.1 h).resolve_left
 
+@[simp] theorem cons_eq_insert {α} [decidable_eq α] (a s h) : @cons α a s h = insert a s :=
+ext $ λ a, by simp
+
 @[simp, norm_cast] lemma coe_insert (a : α) (s : finset α) :
   ↑(insert a s) = (insert a ↑s : set α) :=
 set.ext $ λ x, by simp only [mem_coe, mem_insert, set.mem_insert_iff]
@@ -289,10 +317,10 @@ eq_of_veq $ ndinsert_of_mem h
 insert_eq_of_mem $ mem_singleton_self _
 
 theorem insert.comm (a b : α) (s : finset α) : insert a (insert b s) = insert b (insert a s) :=
-ext $ λ x, by simp only [finset.mem_insert, or.left_comm]
+ext $ λ x, by simp only [mem_insert, or.left_comm]
 
 @[simp] theorem insert_idem (a : α) (s : finset α) : insert a (insert a s) = insert a s :=
-ext $ λ x, by simp only [finset.mem_insert, or.assoc.symm, or_self]
+ext $ λ x, by simp only [mem_insert, or.assoc.symm, or_self]
 
 @[simp] theorem insert_ne_empty (a : α) (s : finset α) : insert a s ≠ ∅ :=
 ne_empty_of_mem (mem_insert_self a s)
@@ -342,8 +370,8 @@ def subtype_insert_equiv_option {t : finset α} {x : α} (h : x ∉ t) :
   {i // i ∈ insert x t} ≃ option {i // i ∈ t} :=
 begin
   refine
-  { to_fun := λ y, if h : ↑y = x then none else some ⟨y, (finset.mem_insert.mp y.2).resolve_left h⟩,
-    inv_fun := λ y, y.elim ⟨x, finset.mem_insert_self _ _⟩ $ λ z, ⟨z, finset.mem_insert_of_mem z.2⟩,
+  { to_fun := λ y, if h : ↑y = x then none else some ⟨y, (mem_insert.mp y.2).resolve_left h⟩,
+    inv_fun := λ y, y.elim ⟨x, mem_insert_self _ _⟩ $ λ z, ⟨z, mem_insert_of_mem z.2⟩,
     .. },
   { intro y, by_cases h : ↑y = x,
     simp only [subtype.ext_iff, h, option.elim, dif_pos, subtype.coe_mk],
@@ -366,6 +394,9 @@ ndunion_eq_union s₁.2
 
 @[simp] theorem mem_union {a : α} {s₁ s₂ : finset α} : a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂ := mem_ndunion
 
+@[simp] theorem disj_union_eq_union {α} [decidable_eq α] (s t h) : @disj_union α s t h = s ∪ t :=
+ext $ λ a, by simp
+
 theorem mem_union_left {a : α} {s₁ : finset α} (s₂ : finset α) (h : a ∈ s₁) : a ∈ s₁ ∪ s₂ :=
 mem_union.2 $ or.inl h
 

src/data/finset/pi.lean

@@ -58,8 +58,8 @@ lemma pi_cons_injective  {a : α} {b : δ a} {s : finset α} (hs : a ∉ s) :
 assume e₁ e₂ eq,
 @multiset.pi_cons_injective α _ δ a b s.1 hs _ _ $
   funext $ assume e, funext $ assume h,
-  have pi.cons s a b e₁ e (by simpa only [mem_cons, mem_insert] using h) =
-    pi.cons s a b e₂ e (by simpa only [mem_cons, mem_insert] using h),
+  have pi.cons s a b e₁ e (by simpa only [multiset.mem_cons, mem_insert] using h) =
+    pi.cons s a b e₂ e (by simpa only [multiset.mem_cons, mem_insert] using h),
   { rw [eq] },
   this
 

src/data/multiset/nodup.lean

@@ -56,6 +56,9 @@ quot.induction_on s $ λ l, nodup_iff_count_le_one
   (d : nodup s) (h : a ∈ s) : count a s = 1 :=
 le_antisymm (nodup_iff_count_le_one.1 d a) (count_pos.2 h)
 
+lemma nodup_iff_pairwise {α} {s : multiset α} : nodup s ↔ pairwise (≠) s :=
+quotient.induction_on s $ λ l, (pairwise_coe_iff_pairwise (by exact λ a b, ne.symm)).symm
+
 lemma pairwise_of_nodup {r : α → α → Prop} {s : multiset α} :
   (∀a∈s, ∀b∈s, a ≠ b → r a b) → nodup s → pairwise r s :=
 quotient.induction_on s $ assume l h hl, ⟨l, rfl, hl.imp_of_mem $ assume a b ha hb, h a ha b hb⟩

src/data/sigma/basic.lean

@@ -84,6 +84,12 @@ end sigma
 section psigma
 variables {α : Sort*} {β : α → Sort*}
 
+/-- Nondependent eliminator for `psigma`. -/
+def psigma.elim {γ} (f : ∀ a, β a → γ) (a : psigma β) : γ :=
+psigma.cases_on a f
+
+@[simp] theorem psigma.elim_val {γ} (f : ∀ a, β a → γ) (a b) : psigma.elim f ⟨a, b⟩ = f a b := rfl
+
 instance [inhabited α] [inhabited (β (default α))] : inhabited (psigma β) :=
 ⟨⟨default α, default (β (default α))⟩⟩
 

src/tactic/default.lean

@@ -29,6 +29,7 @@ import tactic.interval_cases
 import tactic.reassoc_axiom -- most likely useful only for category_theory
 import tactic.slice
 import tactic.subtype_instance
+import tactic.derive_fintype
 import tactic.group
 import tactic.cancel_denoms
 import tactic.zify