chore: move List.lt_iff_lex_lt to a more logical location (#3403)

leanprover-community · Apr 12, 2023 · 85a0b4c · 85a0b4c
1 parent 375149c
commit 85a0b4c
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 19 deletions.
diff --git a/Mathlib/Data/List/Lex.lean b/Mathlib/Data/List/Lex.lean
@@ -192,4 +192,18 @@ instance LE' [LinearOrder α] : LE (List α) :=
   Preorder.toLE
 #align list.has_le' List.LE'
 
+theorem lt_iff_lex_lt [LinearOrder α] (l l' : List α) : lt l l' ↔ Lex (· < ·) l l' := by
+  constructor <;>
+  intro h
+  · induction h with
+    | nil b bs => exact Lex.nil
+    | @head a as b bs hab => apply Lex.rel; assumption
+    | @tail a as b bs hab hba _ ih =>
+      have heq : a = b := _root_.le_antisymm (le_of_not_lt hba) (le_of_not_lt hab)
+      subst b; apply Lex.cons; assumption
+  · induction h with
+    | @nil a as => apply lt.nil
+    | @cons a as bs _ ih => apply lt.tail <;> simp [ih]
+    | @rel a as b bs h => apply lt.head; assumption
+
 end List
diff --git a/Mathlib/Data/String/Basic.lean b/Mathlib/Data/String/Basic.lean
@@ -226,25 +226,6 @@ theorem popn_empty {n : ℕ} : "".popn n = "" := by
   simp [popn]
 #align string.popn_empty String.popn_empty
 
-end String
-
-theorem List.lt_iff_lex_lt [LinearOrder α] (l l' : List α) :
-    lt l l' ↔ Lex (· < ·) l l' := by
-  constructor <;>
-  intro h
-  · induction h with
-    | nil b bs => exact Lex.nil
-    | @head a as b bs hab => apply Lex.rel; assumption
-    | @tail a as b bs hab hba _ ih =>
-      have heq : a = b := _root_.le_antisymm (le_of_not_lt hba) (le_of_not_lt hab)
-      subst b; apply Lex.cons; assumption
-  · induction h with
-    | @nil a as => apply lt.nil
-    | @cons a as bs _ ih => apply lt.tail <;> simp [ih]
-    | @rel a as b bs h => apply lt.head; assumption
-
-namespace String
-
 instance : LinearOrder String where
   le_refl a := le_iff_toList_le.mpr le_rfl
   le_trans a b c := by