feat(data/fintype): well_foundedness lemmas on fintypes (#1156)

* feat(data/fintype): well_foundedness lemmas on fintypes

* Update fintype.lean

* minor fixes

src/data/fintype.lean

@@ -684,6 +684,23 @@ lemma bijective_bij_inv (f_bij : bijective f) : bijective (bij_inv f_bij) :=
 
 end bijection_inverse
 
+lemma well_founded_of_trans_of_irrefl [fintype α] (r : α → α → Prop)
+  [is_trans α r] [is_irrefl α r] : well_founded r :=
+by classical; exact
+have ∀ x y, r x y → (univ.filter (λ z, r z x)).card < (univ.filter (λ z, r z y)).card,
+  from λ x y hxy, finset.card_lt_card $
+    by simp only [finset.lt_iff_ssubset.symm, lt_iff_le_not_le,
+      finset.le_iff_subset, finset.subset_iff, mem_filter, true_and, mem_univ, hxy];
+    exact ⟨λ z hzx, trans hzx hxy, not_forall_of_exists_not ⟨x, not_imp.2 ⟨hxy, irrefl x⟩⟩⟩,
+subrelation.wf this (measure_wf _)
+
+lemma preorder.well_founded [fintype α] [preorder α] : well_founded ((<) : α → α → Prop) :=
+well_founded_of_trans_of_irrefl _
+
+@[instance, priority 0] lemma linear_order.is_well_order [fintype α] [linear_order α] :
+  is_well_order α (<) :=
+{ wf := preorder.well_founded }
+
 end fintype
 
 class infinite (α : Type*) : Prop :=