feat: missing WellFoundedLT instances (#5899)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Data/DFinsupp/WellFounded.lean

@@ -235,10 +235,10 @@ protected theorem DFinsupp.wellFoundedLT [∀ i, Zero (α i)] [∀ i, Preorder (
     exact ⟨i, fun j hj ↦ Quot.sound (he j hj), hl⟩⟩
 #align dfinsupp.well_founded_lt DFinsupp.wellFoundedLT
 
-instance DFinsupp.well_founded_lt' [∀ i, CanonicallyOrderedAddMonoid (α i)]
+instance DFinsupp.wellFoundedLT' [∀ i, CanonicallyOrderedAddMonoid (α i)]
     [∀ i, WellFoundedLT (α i)] : WellFoundedLT (Π₀ i, α i) :=
   DFinsupp.wellFoundedLT fun _i a => (zero_le a).not_lt
-#align dfinsupp.well_founded_lt' DFinsupp.well_founded_lt'
+#align dfinsupp.well_founded_lt' DFinsupp.wellFoundedLT'
 
 instance Pi.wellFoundedLT [Finite ι] [∀ i, Preorder (α i)] [hw : ∀ i, WellFoundedLT (α i)] :
     WellFoundedLT (∀ i, α i) :=
@@ -261,4 +261,3 @@ instance DFinsupp.wellFoundedLT_of_finite [Finite ι] [∀ i, Zero (α i)] [∀
   have := Fintype.ofFinite ι
   ⟨InvImage.wf equivFunOnFintype Pi.wellFoundedLT.wf⟩
 #align dfinsupp.well_founded_lt_of_finite DFinsupp.wellFoundedLT_of_finite
-

Mathlib/Order/Hom/Basic.lean

@@ -687,6 +687,15 @@ protected def dual : αᵒᵈ ↪o βᵒᵈ :=
   ⟨f.toEmbedding, f.map_rel_iff⟩
 #align order_embedding.dual OrderEmbedding.dual
 
+/-- A preorder which embeds into a well-founded preorder is itself well-founded. -/
+protected theorem wellFoundedLT [WellFoundedLT β] : WellFoundedLT α where
+  wf := f.wellFounded IsWellFounded.wf
+
+/-- A preorder which embeds into a preorder in which `(· > ·)` is well-founded
+also has `(· > ·)` well-founded. -/
+protected theorem wellFoundedGT [WellFoundedGT β] : WellFoundedGT α :=
+  @OrderEmbedding.wellFoundedLT αᵒᵈ _ _ _ f.dual _
+
 /-- A version of `WithBot.map` for order embeddings. -/
 @[simps (config := { fullyApplied := false })]
 protected def withBotMap (f : α ↪o β) : WithBot α ↪o WithBot β :=

Mathlib/Order/RelClasses.lean

@@ -521,6 +521,24 @@ theorem Subrelation.isWellFounded (r : α → α → Prop) [IsWellFounded α r]
   ⟨h.wf IsWellFounded.wf⟩
 #align subrelation.is_well_founded Subrelation.isWellFounded
 
+instance Prod.wellFoundedLT [PartialOrder α] [WellFoundedLT α] [Preorder β] [WellFoundedLT β] :
+    WellFoundedLT (α × β) where
+  wf := by
+    refine @Subrelation.wf (α × β) (Prod.Lex (· < ·) (· < ·)) (· < ·) ?_ IsWellFounded.wf
+    rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ w
+    simp only [Prod.mk_lt_mk] at w
+    rcases eq_or_ne a₁ a₂ with rfl | ha
+    · right
+      simpa using w
+    · left
+      rcases w with ⟨a_lt, _⟩ | ⟨a_le, _⟩
+      · assumption
+      · exact Ne.lt_of_le ha a_le
+
+instance Prod.wellFoundedGT [PartialOrder α] [WellFoundedGT α] [Preorder β] [WellFoundedGT β] :
+    WellFoundedGT (α × β) :=
+  @Prod.wellFoundedLT αᵒᵈ βᵒᵈ _ _ _ _
+
 namespace Set
 
 /-- An unbounded or cofinal set. -/