diff --git a/Mathlib/Order/WellQuasiOrder.lean b/Mathlib/Order/WellQuasiOrder.lean
index 38967d32b4c397..0d34ea4abd0651 100644
--- a/Mathlib/Order/WellQuasiOrder.lean
+++ b/Mathlib/Order/WellQuasiOrder.lean
@@ -113,6 +113,13 @@ theorem RelIso.wellQuasiOrdered_iff {α β} {r : α → α → Prop} {s : β →
   congr! with g a b
   simp [f.map_rel_iff]
 
+theorem WellQuasiOrdered.of_surjective {α β} {r : α → α → Prop}
+    {s : β → β → Prop} (h : WellQuasiOrdered r) (f : r →r s) (hf : Function.Surjective f) :
+    WellQuasiOrdered s := by
+  intro seq
+  have ⟨_, _, hle, hr⟩ := h (Function.surjInv hf ∘ seq)
+  exact ⟨_, _, hle, by simpa [Function.surjInv_eq] using f.map_rel hr⟩
+
 /-- A typeclass for an order with a well-quasi-ordered `≤` relation.
 
 Note that this is unlike `WellFoundedLT`, which instead takes a `<` relation. -/
@@ -178,6 +185,16 @@ theorem wellQuasiOrderedLE_iff :
 instance [WellQuasiOrderedLE α] [Preorder β] [WellQuasiOrderedLE β] : WellQuasiOrderedLE (α × β) :=
   ⟨wellQuasiOrdered_le.prod wellQuasiOrdered_le⟩
 
+theorem Monotone.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective [Preorder β]
+    [WellQuasiOrderedLE α] {f : α → β} (mono : Monotone f) (hf : Function.Surjective f) :
+    WellQuasiOrderedLE β :=
+  ⟨wellQuasiOrdered_le.of_surjective ⟨_, (mono ·)⟩ hf⟩
+
+theorem OrderHom.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective [Preorder β]
+    [WellQuasiOrderedLE α] (f : α →o β) (hf : Function.Surjective f) :
+    WellQuasiOrderedLE β :=
+  f.monotone.wellQuasiOrderedLE_of_wellQuasiOrderedLE_of_surjective hf
+
 end Preorder
 
 section LinearOrder