lt -> gt

Co-authored-by: Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

Author: SnirBroshi

Mathlib/Order/WellFounded.lean

@@ -136,7 +136,7 @@ theorem wellFoundedLT_iff_exists_minimal [Preorder α] :
     WellFoundedLT α ↔ ∀ s : Set α, s.Nonempty → ∃ m, Minimal (· ∈ s) m := by
   simp only [isWellFounded_iff, wellFounded_iff_has_min, not_lt_iff_le_imp_ge, Minimal]
 
-theorem isWellOrder_iff_exists_not_lt_and_eq_or_lt :
+theorem isWellOrder_iff_exists_not_lt_and_eq_or_gt :
     IsWellOrder α r ↔ ∀ s : Set α, s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m ∧ (m = x ∨ r m x) := by
   refine ⟨fun h s hs ↦ ?_, fun h ↦ { wf := ?_, trichotomous a b := ?_ }⟩
   · grind [h.wf.has_min, trichotomous_of r]