chore(data/fintype/card): instance well_founded_of_trans_of_irrefl

src/data/dfinsupp/well_founded.lean

@@ -171,9 +171,9 @@ begin
   obtain h | ⟨⟨x⟩⟩ := is_empty_or_nonempty (Π i, α i),
   { convert empty_wf, ext1 x, exact (h.1 x).elim },
   letI : Π i, has_zero (α i) := λ i, ⟨(hs i).min ⊤ ⟨x i, trivial⟩⟩,
-  haveI := is_trans.swap r, haveI := is_irrefl.swap r, haveI := fintype.of_finite ι,
+  haveI := is_strict_order.swap r, haveI := fintype.of_finite ι,
   refine inv_image.wf equiv_fun_on_fintype.symm (lex.well_founded' (λ i a, _) hs _),
-  exacts [(hs i).not_lt_min ⊤ _ trivial, finite.well_founded_of_trans_of_irrefl r.swap],
+  exacts [(hs i).not_lt_min ⊤ _ trivial, (finite.is_well_founded_of_strict_order r.swap).wf],
 end
 
 instance pi.lex.well_founded_lt [linear_order ι] [finite ι] [Π i, has_lt (α i)]

src/data/fin/tuple/bubble_sort_induction.lean

@@ -40,7 +40,7 @@ lemma bubble_sort_induction' {n : ℕ} {α : Type*} [linear_order α] {f : fin n
 begin
   letI := @preorder.lift _ (lex (fin n → α)) _ (λ σ : equiv.perm (fin n), to_lex (f ∘ σ)),
   refine @well_founded.induction_bot' _ _ _
-    (@finite.preorder.well_founded_lt (equiv.perm (fin n)) _ _)
+    (@finite.is_well_founded_of_strict_order _ _ (<) _).wf
     (equiv.refl _) (sort f) P (λ σ, f ∘ σ) (λ σ hσ hfσ, _) hf,
   obtain ⟨i, j, hij₁, hij₂⟩ := antitone_pair_of_not_sorted' hσ,
   exact ⟨σ * equiv.swap i j, pi.lex_desc hij₁ hij₂, h σ i j hij₁ hij₂ hfσ⟩,

src/data/fintype/card.lean

@@ -716,27 +716,19 @@ end
 namespace finite
 variables [finite α]
 
-lemma well_founded_of_trans_of_irrefl (r : α → α → Prop) [is_trans α r] [is_irrefl α r] :
-  well_founded r :=
-by classical; casesI nonempty_fintype α; exact
+instance is_well_founded_of_strict_order (r : α → α → Prop) [is_strict_order α r] :
+  is_well_founded α r :=
+⟨by classical; casesI nonempty_fintype α; 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 _)
+subrelation.wf this (measure_wf _)⟩
 
-lemma preorder.well_founded_lt [preorder α] : well_founded ((<) : α → α → Prop) :=
-well_founded_of_trans_of_irrefl _
+@[priority 10] instance linear_order.is_well_order_lt [linear_order α] : is_well_order α (<) := { }
 
-lemma preorder.well_founded_gt [preorder α] : well_founded ((>) : α → α → Prop) :=
-well_founded_of_trans_of_irrefl _
-
-@[priority 10] instance linear_order.is_well_order_lt [linear_order α] : is_well_order α (<) :=
-{ wf := preorder.well_founded_lt }
-
-@[priority 10] instance linear_order.is_well_order_gt [linear_order α] : is_well_order α (>) :=
-{ wf := preorder.well_founded_gt }
+@[priority 10] instance linear_order.is_well_order_gt [linear_order α] : is_well_order α (>) := { }
 
 end finite
 
@@ -767,8 +759,8 @@ lemma finset.exists_minimal {α : Type*} [preorder α] (s : finset α) (h : s.no
   ∃ m ∈ s, ∀ x ∈ s, ¬ (x < m) :=
 begin
   obtain ⟨c, hcs : c ∈ s⟩ := h,
-  have : well_founded (@has_lt.lt {x // x ∈ s} _) := finite.well_founded_of_trans_of_irrefl _,
-  obtain ⟨⟨m, hms : m ∈ s⟩, -, H⟩ := this.has_min set.univ ⟨⟨c, hcs⟩, trivial⟩,
+  have : well_founded_lt {x // x ∈ s} := by apply_instance,
+  obtain ⟨⟨m, hms : m ∈ s⟩, -, H⟩ := this.wf.has_min set.univ ⟨⟨c, hcs⟩, trivial⟩,
   exact ⟨m, hms, λ x hx hxm, H ⟨x, hx⟩ trivial hxm⟩,
 end
 

src/topology/noetherian_space.lean

@@ -174,7 +174,7 @@ end
 
 @[priority 100]
 instance finite.to_noetherian_space [finite α] : noetherian_space α :=
-⟨finite.well_founded_of_trans_of_irrefl _⟩
+⟨is_well_founded.wf⟩
 
 lemma noetherian_space.exists_finset_irreducible [noetherian_space α] (s : closeds α) :
   ∃ S : finset (closeds α), (∀ k : S, is_irreducible (k : set α)) ∧ s = S.sup id :=