diff --git a/src/analysis/inner_product_space/gram_schmidt_ortho.lean b/src/analysis/inner_product_space/gram_schmidt_ortho.lean
index 91957da899ecd..12eff1b6066b1 100644
--- a/src/analysis/inner_product_space/gram_schmidt_ortho.lean
+++ b/src/analysis/inner_product_space/gram_schmidt_ortho.lean
@@ -81,7 +81,7 @@ begin
   clear h₀ a b,
   intros a b h₀,
   revert a,
-  apply well_founded.induction (@is_well_order.wf ι (<) _) b,
+  apply well_founded.induction (@is_well_founded.wf ι (<) _) b,
   intros b ih a h₀,
   simp only [gram_schmidt_def 𝕜 f b, inner_sub_right, inner_sum,
     orthogonal_projection_singleton, inner_smul_right],
diff --git a/src/data/nat/part_enat.lean b/src/data/nat/part_enat.lean
index 4e8bd8705cb63..c22ddee0b6d57 100644
--- a/src/data/nat/part_enat.lean
+++ b/src/data/nat/part_enat.lean
@@ -492,7 +492,8 @@ begin
   exact inv_image.wf _ (with_top.well_founded_lt nat.lt_wf)
 end
 
-instance : is_well_order part_enat (<) := ⟨lt_wf⟩
+instance : well_founded_lt part_enat := ⟨lt_wf⟩
+instance : is_well_order part_enat (<) := { }
 instance : has_well_founded part_enat := ⟨(<), lt_wf⟩
 
 section find
diff --git a/src/data/pi/lex.lean b/src/data/pi/lex.lean
index ef90361179189..c6ac718a57a90 100644
--- a/src/data/pi/lex.lean
+++ b/src/data/pi/lex.lean
@@ -84,7 +84,7 @@ partial_order_of_SO (<)
 noncomputable instance [linear_order ι] [is_well_order ι (<)] [∀ a, linear_order (β a)] :
   linear_order (lex (Π i, β i)) :=
 @linear_order_of_STO' (Πₗ i, β i) (<)
-  { to_is_trichotomous := is_trichotomous_lex _ _ is_well_order.wf } (classical.dec_rel _)
+  { to_is_trichotomous := is_trichotomous_lex _ _ is_well_founded.wf } (classical.dec_rel _)
 
 lemma lex.le_of_forall_le [linear_order ι] [is_well_order ι (<)] [Π a, linear_order (β a)]
   {a b : lex (Π i, β i)} (h : ∀ i, a i ≤ b i) : a ≤ b :=
diff --git a/src/data/sum/order.lean b/src/data/sum/order.lean
index 727f2d1b9860c..fa415e8e8a7f4 100644
--- a/src/data/sum/order.lean
+++ b/src/data/sum/order.lean
@@ -88,7 +88,7 @@ instance [is_trichotomous α r] [is_trichotomous β s] : is_trichotomous (α ⊕
 end⟩
 
 instance [is_well_order α r] [is_well_order β s] : is_well_order (α ⊕ β) (sum.lex r s) :=
-{ wf := sum.lex_wf is_well_order.wf is_well_order.wf }
+{ wf := sum.lex_wf is_well_founded.wf is_well_founded.wf }
 
 end lex
 
diff --git a/src/order/conditionally_complete_lattice.lean b/src/order/conditionally_complete_lattice.lean
index 1436435eb6a8d..d0cd695289dae 100644
--- a/src/order/conditionally_complete_lattice.lean
+++ b/src/order/conditionally_complete_lattice.lean
@@ -687,7 +687,8 @@ lemma exists_lt_of_cinfi_lt [nonempty ι] {f : ι → α} (h : infi f < a) : ∃
 open function
 variables [is_well_order α (<)]
 
-lemma Inf_eq_argmin_on (hs : s.nonempty) : Inf s = argmin_on id (@is_well_order.wf α (<) _) s hs :=
+lemma Inf_eq_argmin_on (hs : s.nonempty) :
+  Inf s = argmin_on id (@is_well_founded.wf α (<) _) s hs :=
 is_least.cInf_eq ⟨argmin_on_mem _ _ _ _, λ a ha, argmin_on_le id _ _ ha⟩
 
 lemma is_least_Inf (hs : s.nonempty) : is_least s (Inf s) :=
diff --git a/src/order/initial_seg.lean b/src/order/initial_seg.lean
index 20c1eca7531c7..27b3920a62acd 100644
--- a/src/order/initial_seg.lean
+++ b/src/order/initial_seg.lean
@@ -106,7 +106,7 @@ end⟩
 
 instance [is_well_order β s] : subsingleton (r ≼i s) :=
 ⟨λ a, @subsingleton.elim _ (unique_of_trichotomous_of_irrefl
-  (@rel_embedding.well_founded _ _ r s a is_well_order.wf)) a⟩
+  (@rel_embedding.well_founded _ _ r s a is_well_founded.wf)) a⟩
 
 protected theorem eq [is_well_order β s] (f g : r ≼i s) (a) : f a = g a :=
 by rw subsingleton.elim f g
@@ -130,7 +130,7 @@ rel_iso.coe_fn_injective rfl
 theorem eq_or_principal [is_well_order β s] (f : r ≼i s) :
   surjective f ∨ ∃ b, ∀ x, s x b ↔ ∃ y, f y = x :=
 or_iff_not_imp_right.2 $ λ h b,
-acc.rec_on (is_well_order.wf.apply b : acc s b) $ λ x H IH,
+acc.rec_on (is_well_founded.wf.apply b : acc s b) $ λ x H IH,
 not_forall_not.1 $ λ hn,
 h ⟨x, λ y, ⟨(IH _), λ ⟨a, e⟩, by rw ← e; exact
   (trichotomous _ _).resolve_right
@@ -363,13 +363,13 @@ namespace rel_embedding
 gaps, to obtain an initial segment. Here, we construct the collapsed order embedding pointwise,
 but the proof of the fact that it is an initial segment will be given in `collapse`. -/
 noncomputable def collapse_F [is_well_order β s] (f : r ↪r s) : Π a, {b // ¬ s (f a) b} :=
-(rel_embedding.well_founded f $ is_well_order.wf).fix $ λ a IH, begin
+(rel_embedding.well_founded f $ is_well_founded.wf).fix $ λ a IH, begin
   let S := {b | ∀ a h, s (IH a h).1 b},
   have : f a ∈ S, from λ a' h, ((trichotomous _ _)
     .resolve_left $ λ h', (IH a' h).2 $ trans (f.map_rel_iff.2 h) h')
     .resolve_left $ λ h', (IH a' h).2 $ h' ▸ f.map_rel_iff.2 h,
-  exact ⟨is_well_order.wf.min S ⟨_, this⟩,
-   is_well_order.wf.not_lt_min _ _ this⟩
+  exact ⟨is_well_founded.wf.min S ⟨_, this⟩,
+   is_well_founded.wf.not_lt_min _ _ this⟩
 end
 
 theorem collapse_F.lt [is_well_order β s] (f : r ↪r s) {a : α}
@@ -393,15 +393,15 @@ noncomputable def collapse [is_well_order β s] (f : r ↪r s) : r ≼i s :=
 by haveI := rel_embedding.is_well_order f; exact
 ⟨rel_embedding.of_monotone
   (λ a, (collapse_F f a).1) (λ a b, collapse_F.lt f),
-λ a b, acc.rec_on (is_well_order.wf.apply b : acc s b) (λ b H IH a h, begin
+λ a b, acc.rec_on (is_well_founded.wf.apply b : acc s b) (λ b H IH a h, begin
   let S := {a | ¬ s (collapse_F f a).1 b},
   have : S.nonempty := ⟨_, asymm h⟩,
-  existsi (is_well_order.wf : well_founded r).min S this,
+  existsi (is_well_founded.wf : well_founded r).min S this,
   refine ((@trichotomous _ s _ _ _).resolve_left _).resolve_right _,
-  { exact (is_well_order.wf : well_founded r).min_mem S this },
+  { exact (is_well_founded.wf : well_founded r).min_mem S this },
   { refine collapse_F.not_lt f _ (λ a' h', _),
     by_contradiction hn,
-    exact is_well_order.wf.not_lt_min S this hn h' }
+    exact is_well_founded.wf.not_lt_min S this hn h' }
 end) a⟩
 
 theorem collapse_apply [is_well_order β s] (f : r ↪r s)
diff --git a/src/order/rel_classes.lean b/src/order/rel_classes.lean
index ff13b8dab2aa1..6b4677f24d302 100644
--- a/src/order/rel_classes.lean
+++ b/src/order/rel_classes.lean
@@ -278,10 +278,12 @@ theorem well_founded_lt_dual_iff (α : Type*) [has_lt α] : well_founded_lt α
 
 /-- A well order is a well-founded linear order. -/
 @[algebra] class is_well_order (α : Type u) (r : α → α → Prop)
-  extends is_strict_total_order' α r : Prop :=
-(wf : well_founded r)
+  extends is_trichotomous α r, is_trans α r, is_well_founded α r : Prop
 
 @[priority 100] -- see Note [lower instance priority]
+instance is_well_order.is_strict_total_order' {α} (r : α → α → Prop) [is_well_order α r] :
+  is_strict_total_order' α r := { }
+@[priority 100] -- see Note [lower instance priority]
 instance is_well_order.is_strict_total_order {α} (r : α → α → Prop) [is_well_order α r] :
   is_strict_total_order α r := by apply_instance
 @[priority 100] -- see Note [lower instance priority]
@@ -370,7 +372,6 @@ subsingleton.is_well_order _
 @[priority 100]
 instance is_empty.is_well_order [is_empty α] (r : α → α → Prop) : is_well_order α r :=
 { trichotomous := is_empty_elim,
-  irrefl       := is_empty_elim,
   trans        := is_empty_elim,
   wf           := well_founded_of_empty r }
 
@@ -390,8 +391,6 @@ instance prod.lex.is_well_order [is_well_order α r] [is_well_order β s] :
       | or.inr (or.inl e) := e ▸ or.inr $ or.inl rfl
       end
     end,
-  irrefl := λ ⟨a₁, a₂⟩ h, by cases h with _ _ _ _ h _ _ _ h;
-     [exact irrefl _ h, exact irrefl _ h],
   trans := λ a b c h₁ h₂, begin
     cases h₁ with a₁ a₂ b₁ b₂ ab a₁ b₁ b₂ ab;
     cases h₂ with _ _ c₁ c₂ bc _ _ c₂ bc,
@@ -400,7 +399,7 @@ instance prod.lex.is_well_order [is_well_order α r] [is_well_order β s] :
     { exact prod.lex.left _ _ bc },
     { exact prod.lex.right _ (trans ab bc) }
   end,
-  wf := prod.lex_wf is_well_order.wf is_well_order.wf }
+  wf := prod.lex_wf is_well_founded.wf is_well_founded.wf }
 
 instance inv_image.is_well_founded (r : α → α → Prop) [is_well_founded α r] (f : β → α) :
   is_well_founded _ (inv_image r f) :=
@@ -620,7 +619,7 @@ instance order_dual.is_total_le [has_le α] [is_total α (≤)] : is_total αᵒ
 @is_total.swap α _ _
 
 instance : well_founded_lt ℕ := ⟨nat.lt_wf⟩
-instance nat.lt.is_well_order : is_well_order ℕ (<) := ⟨nat.lt_wf⟩
+instance nat.lt.is_well_order : is_well_order ℕ (<) := { }
 
 instance [linear_order α] [h : is_well_order α (<)] : is_well_order αᵒᵈ (>) := h
 instance [linear_order α] [h : is_well_order α (>)] : is_well_order αᵒᵈ (<) := h
diff --git a/src/order/well_founded_set.lean b/src/order/well_founded_set.lean
index ccf5bec5dbd20..d80a49d86ad96 100644
--- a/src/order/well_founded_set.lean
+++ b/src/order/well_founded_set.lean
@@ -895,7 +895,7 @@ begin
   { intros f hf, existsi rel_embedding.refl (≤),
     simp only [is_empty.forall_iff, implies_true_iff, forall_const, finset.not_mem_empty], },
   { intros x s hx ih f hf,
-    obtain ⟨g, hg⟩ := (is_well_order.wf.is_wf (set.univ : set _)).is_pwo.exists_monotone_subseq
+    obtain ⟨g, hg⟩ := (is_well_founded.wf.is_wf (set.univ : set _)).is_pwo.exists_monotone_subseq
       ((λ mo : Π s : σ, α s, mo x) ∘ f) (set.subset_univ _),
     obtain ⟨g', hg'⟩ := ih (f ∘ g) (set.subset_univ _),
     refine ⟨g'.trans g, λ a b hab, _⟩,
diff --git a/src/set_theory/cardinal/basic.lean b/src/set_theory/cardinal/basic.lean
index c1fefbd2392df..04449d9b69cf8 100644
--- a/src/set_theory/cardinal/basic.lean
+++ b/src/set_theory/cardinal/basic.lean
@@ -532,8 +532,8 @@ protected theorem lt_wf : @well_founded cardinal.{u} (<) :=
 end⟩
 
 instance : has_well_founded cardinal.{u} := ⟨(<), cardinal.lt_wf⟩
-
-instance wo : @is_well_order cardinal.{u} (<) := ⟨cardinal.lt_wf⟩
+instance : well_founded_lt cardinal.{u} := ⟨cardinal.lt_wf⟩
+instance wo : @is_well_order cardinal.{u} (<) := { }
 
 instance : conditionally_complete_linear_order_bot cardinal :=
 is_well_order.conditionally_complete_linear_order_bot _
diff --git a/src/set_theory/cardinal/cofinality.lean b/src/set_theory/cardinal/cofinality.lean
index 2ffcc6ffca341..fde623782191d 100644
--- a/src/set_theory/cardinal/cofinality.lean
+++ b/src/set_theory/cardinal/cofinality.lean
@@ -172,11 +172,11 @@ begin
       exact irrefl _ h } },
   { intro a,
     have : {b : S | ¬ r b a}.nonempty := let ⟨b, bS, ba⟩ := hS a in ⟨⟨b, bS⟩, ba⟩,
-    let b := (is_well_order.wf).min _ this,
-    have ba : ¬r b a := (is_well_order.wf).min_mem _ this,
+    let b := (is_well_founded.wf).min _ this,
+    have ba : ¬r b a := (is_well_founded.wf).min_mem _ this,
     refine ⟨b, ⟨b.2, λ c, not_imp_not.1 $ λ h, _⟩, ba⟩,
     rw [show ∀b:S, (⟨b, b.2⟩:S) = b, by intro b; cases b; refl],
-    exact (is_well_order.wf).not_lt_min _ this
+    exact (is_well_founded.wf).not_lt_min _ this
       (is_order_connected.neg_trans h ba) }
 end
 
diff --git a/src/set_theory/ordinal/basic.lean b/src/set_theory/ordinal/basic.lean
index 0817e24c9a2a5..87aae5edf6b63 100644
--- a/src/set_theory/ordinal/basic.lean
+++ b/src/set_theory/ordinal/basic.lean
@@ -678,7 +678,8 @@ instance : linear_order ordinal :=
   decidable_le := classical.dec_rel _,
   ..ordinal.partial_order }
 
-instance : is_well_order ordinal (<) := ⟨lt_wf⟩
+instance : well_founded_lt ordinal := ⟨lt_wf⟩
+instance : is_well_order ordinal (<) := { }
 
 instance : conditionally_complete_linear_order_bot ordinal :=
 is_well_order.conditionally_complete_linear_order_bot _
@@ -705,10 +706,8 @@ private theorem succ_le_iff' {a b : ordinal} : a + 1 ≤ b ↔ a < b :=
     (λ x, ⟨λ _, ⟨x, rfl⟩, λ _, sum.lex.sep _ _⟩)
     (λ x, sum.lex_inr_inr.trans ⟨false.elim, λ ⟨x, H⟩, sum.inl_ne_inr H⟩)⟩⟩),
 induction_on a $ λ α r hr, induction_on b $ λ β s hs ⟨⟨f, t, hf⟩⟩, begin
-  refine ⟨⟨@rel_embedding.of_monotone (α ⊕ punit) β _ _
-    (@sum.lex.is_well_order _ _ _ _ hr _).1.1
-    (@is_asymm_of_is_trans_of_is_irrefl _ _ hs.1.2.2 hs.1.2.1)
-    (sum.rec _ _) (λ a b, _), λ a b, _⟩⟩,
+  haveI := hs,
+  refine ⟨⟨@rel_embedding.of_monotone (α ⊕ punit) β _ _ _ _ (sum.rec _ _) (λ a b, _), λ a b, _⟩⟩,
   { exact f }, { exact λ _, t },
   { rcases a with a|_; rcases b with b|_,
     { simpa only [sum.lex_inl_inl] using f.map_rel_iff.2 },
@@ -716,7 +715,7 @@ induction_on a $ λ α r hr, induction_on b $ λ β s hs ⟨⟨f, t, hf⟩⟩, b
     { exact false.elim ∘ sum.lex_inr_inl },
     { exact false.elim ∘ sum.lex_inr_inr.1 } },
   { rcases a with a|_,
-    { intro h, have := @principal_seg.init _ _ _ _ hs.1.2.2 ⟨f, t, hf⟩ _ _ h,
+    { intro h, have := @principal_seg.init _ _ _ _ _ ⟨f, t, hf⟩ _ _ h,
       cases this with w h, exact ⟨sum.inl w, h⟩ },
     { intro h, cases (hf b).1 h with w h, exact ⟨sum.inl w, h⟩ } }
 end⟩
diff --git a/src/set_theory/ordinal/natural_ops.lean b/src/set_theory/ordinal/natural_ops.lean
index 82ebecb84eab6..c57041816c21d 100644
--- a/src/set_theory/ordinal/natural_ops.lean
+++ b/src/set_theory/ordinal/natural_ops.lean
@@ -66,6 +66,7 @@ variables {a b c : nat_ordinal.{u}}
 @[simp] theorem to_ordinal_to_nat_ordinal (a : nat_ordinal) : a.to_ordinal.to_nat_ordinal = a := rfl
 
 theorem lt_wf : @well_founded nat_ordinal (<) := ordinal.lt_wf
+instance : well_founded_lt nat_ordinal := ordinal.well_founded_lt
 instance : is_well_order nat_ordinal (<) := ordinal.has_lt.lt.is_well_order
 
 @[simp] theorem to_ordinal_zero : to_ordinal 0 = 0 := rfl
diff --git a/src/set_theory/ordinal/notation.lean b/src/set_theory/ordinal/notation.lean
index 3694d168a3204..1d81c754c5b62 100644
--- a/src/set_theory/ordinal/notation.lean
+++ b/src/set_theory/ordinal/notation.lean
@@ -1020,6 +1020,7 @@ instance : has_zero nonote := ⟨⟨0, NF.zero⟩⟩
 instance : inhabited nonote := ⟨0⟩
 
 theorem lt_wf : @well_founded nonote (<) := inv_image.wf repr ordinal.lt_wf
+instance : well_founded_lt nonote := ⟨lt_wf⟩
 instance : has_well_founded nonote := ⟨(<), lt_wf⟩
 
 /-- Convert a natural number to an ordinal notation -/
@@ -1038,7 +1039,7 @@ theorem cmp_compares : ∀ a b : nonote, (cmp a b).compares a b
 end
 
 instance : linear_order nonote := linear_order_of_compares cmp cmp_compares
-instance : is_well_order nonote (<) := ⟨lt_wf⟩
+instance : is_well_order nonote (<) := { }
 
 /-- Asserts that `repr a < ω ^ repr b`. Used in `nonote.rec_on` -/
 def below (a b : nonote) : Prop := NF_below a.1 (repr b)
diff --git a/src/topology/metric_space/emetric_paracompact.lean b/src/topology/metric_space/emetric_paracompact.lean
index e98eeb0e4256e..5048b2434f82d 100644
--- a/src/topology/metric_space/emetric_paracompact.lean
+++ b/src/topology/metric_space/emetric_paracompact.lean
@@ -47,7 +47,7 @@ begin
   simp only [Union_eq_univ_iff] at hcov,
   -- choose a well founded order on `S`
   letI : linear_order ι := linear_order_of_STO' well_ordering_rel,
-  have wf : well_founded ((<) : ι → ι → Prop) := @is_well_order.wf ι well_ordering_rel _,
+  have wf : well_founded ((<) : ι → ι → Prop) := @is_well_founded.wf ι well_ordering_rel _,
   -- Let `ind x` be the minimal index `s : S` such that `x ∈ s`.
   set ind : α → ι := λ x, wf.min {i : ι | x ∈ s i} (hcov x),
   have mem_ind : ∀ x, x ∈ s (ind x), from λ x, wf.min_mem _ (hcov x),