diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index 5aae20258d..0149e4fa0e 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@@ -258,6 +258,55 @@ instance (r : α → β → Prop) [s : DecidableRel r] : DecidableRel (Option.lt
   | some _, none   => isFalse not_false
   | none,   none   => isFalse not_false
 
+namespace SomeLtNone
+
+/--
+Lifts an ordering relation to `Option` such that `none` is the *greatest* element.
+
+It can be understood as adding a distinguished greatest element, represented by `none`, to both `α`
+and `β`.
+
+Caution: Given `LT α`, `Option.SomeLtNone.lt LT.lt` differs from the `LT (Option α)` instance,
+which is implemented by `Option.lt Lt.lt`.
+
+Examples:
+ * `Option.lt (fun n k : Nat => n < k) none none = False`
+ * `Option.lt (fun n k : Nat => n < k) none (some 3) = False`
+ * `Option.lt (fun n k : Nat => n < k) (some 3) none = True`
+ * `Option.lt (fun n k : Nat => n < k) (some 4) (some 5) = True`
+ * `Option.le (fun n k : Nat => n < k) (some 5) (some 4) = False`
+ * `Option.lt (fun n k : Nat => n < k) (some 4) (some 4) = False`
+-/
+def lt {α} (r : α → β → Prop) : Option α → Option β → Prop
+  | none, _ => False
+  | some _, none => True
+  | some x, some y => r x y
+
+/--
+Lifts an ordering relation to `Option` such that `none` is the *greatest* element.
+
+It can be understood as adding a distinguished greatest element, represented by `none`, to both `α`
+and `β`.
+
+Caution: Given `LE α`, `Option.SomeLtNone.le LE.le` differs from the `LE (Option α)` instance,
+which is implemented by `Option.le LE.le`.
+
+Examples:
+ * `Option.le (fun n k : Nat => n < k) none none = True`
+ * `Option.le (fun n k : Nat => n < k) none (some 3) = False`
+ * `Option.le (fun n k : Nat => n < k) (some 3) none = True`
+ * `Option.le (fun n k : Nat => n < k) (some 4) (some 5) = True`
+ * `Option.le (fun n k : Nat => n < k) (some 5) (some 4) = False`
+ * `Option.le (fun n k : Nat => n < k) (some 4) (some 4) = True`
+-/
+def le {α} (r : α → β → Prop) : Option α → Option β → Prop
+  | none, none => True
+  | none, some _ => False
+  | some _, none => True
+  | some x, some y => r x y
+
+end SomeLtNone
+
 /--
 Applies a function to a two optional values if both are present. Otherwise, if one value is present,
 it is returned and the function is not used.
diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index 5dc9a6d998..d7fddf6851 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -1922,4 +1922,38 @@ theorem map_min [Min α] [Min β] {o o' : Option α} {f : α → β} (hf : ∀ x
     (min o o').map f = min (o.map f) (o'.map f) := by
   cases o <;> cases o' <;> simp [*]
 
+theorem wellFounded_lt {α} {rel : α → α → Prop} (h : WellFounded rel) :
+    WellFounded (Option.lt rel) := by
+  refine ⟨fun x => ?_⟩
+  have hn : Acc (Option.lt rel) none := by
+    refine Acc.intro none ?_
+    intro y hyx
+    cases y <;> cases hyx
+  cases x
+  · exact hn
+  · rename_i x
+    induction h.apply x
+    rename_i _ _ ih
+    refine Acc.intro _ (fun y hy => ?_)
+    cases y
+    · exact hn
+    · exact ih _ hy
+
+theorem SomeLtNone.wellFounded_lt {α} {r : α → α → Prop} (h : WellFounded r) :
+    WellFounded (SomeLtNone.lt r) := by
+  refine ⟨?_⟩
+  intro x
+  constructor
+  intro x' hlt
+  match x' with
+  | none => contradiction
+  | some x' =>
+    clear hlt
+    induction h.apply x'
+    rename_i ih
+    refine Acc.intro _ (fun x'' hlt' => ?_)
+    match x'' with
+    | none => contradiction
+    | some x'' => exact ih x'' hlt'
+
 end Option
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean b/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean
index 687791f718..c7ee361b3a 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean
@@ -18,73 +18,6 @@ This file provides an iterator combinator `IterM.zip` that combines two iterator
 of pairs.
 -/
 
-namespace Std.Internal.Option
-
-/- TODO: move this to Init.Data.Option -/
-namespace SomeLtNone
-
-/--
-Lifts an ordering relation to `Option`, such that `none` is the greatest element.
-
-It can be understood as adding a distinguished greatest element, represented by `none`, to both `α`
-and `β`.
-
-Caution: Given `LT α`, `Option.SomeLtNone.lt LT.lt` differs from the `LT (Option α)` instance,
-which is implemented by `Option.lt Lt.lt`.
-
-Examples:
- * `Option.lt (fun n k : Nat => n < k) none none = False`
- * `Option.lt (fun n k : Nat => n < k) none (some 3) = False`
- * `Option.lt (fun n k : Nat => n < k) (some 3) none = True`
- * `Option.lt (fun n k : Nat => n < k) (some 4) (some 5) = True`
- * `Option.lt (fun n k : Nat => n < k) (some 4) (some 4) = False`
--/
-def lt {α} (r : α → α → Prop) : Option α → Option α → Prop
-  | none, _ => false
-  | some _, none => true
-  | some a', some a => r a' a
-
-end SomeLtNone
-
-/- TODO: Move these to Init.Data.Option.Lemmas in a separate PR -/
-theorem wellFounded_lt {α} {rel : α → α → Prop} (h : WellFounded rel) :
-    WellFounded (Option.lt rel) := by
-  refine ⟨fun x => ?_⟩
-  have hn : Acc (Option.lt rel) none := by
-    refine Acc.intro none ?_
-    intro y hyx
-    cases y <;> cases hyx
-  cases x
-  · exact hn
-  · rename_i x
-    induction h.apply x
-    rename_i x' h ih
-    refine Acc.intro _ ?_
-    intro y hyx'
-    cases y
-    · exact hn
-    · exact ih _ hyx'
-
-theorem SomeLtNone.wellFounded_lt {α} {r : α → α → Prop} (h : WellFounded r) :
-    WellFounded (SomeLtNone.lt r) := by
-  refine ⟨?_⟩
-  intro x
-  constructor
-  intro x' hlt
-  match x' with
-  | none => contradiction
-  | some x' =>
-    clear hlt
-    induction h.apply x'
-    rename_i ih
-    constructor
-    intro x'' hlt'
-    match x'' with
-    | none => contradiction
-    | some x'' => exact ih x'' hlt'
-
-end Std.Internal.Option
-
 namespace Std.Iterators
 open Std.Internal
 
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
index d84d4a70dd..8497d9fed8 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
@@ -131,23 +131,12 @@ theorem _root_.Array.toList_iterM [LawfulMonad m] {array : Array β} :
     (array.iterM m).toList = pure array.toList := by
   simp [Array.iterM_eq_iterFromIdxM, Array.toList_iterFromIdxM]
 
--- Move to Init.Data.Array.Lemmas in a separate PR afterwards
-private theorem drop_toArray' {l : List α} {k : Nat} :
-    l.toArray.drop k = (l.drop k).toArray := by
-  induction l generalizing k
-  case nil => simp
-  case cons l' ih =>
-    match k with
-    | 0 => simp
-    | k' + 1 => simp [List.drop_succ_cons, ← ih]
-
 @[simp]
 theorem _root_.Array.toArray_iterFromIdxM [LawfulMonad m] {array : Array β} {pos : Nat} :
     (array.iterFromIdxM m pos).toArray = pure (array.extract pos) := by
   simp [← IterM.toArray_toList, Array.toList_iterFromIdxM]
-  rw [← Array.drop_eq_extract]
   rw (occs := [2]) [← Array.toArray_toList (xs := array)]
-  rw [drop_toArray']
+  rw [← List.toArray_drop]
 
 @[simp]
 theorem _root_.Array.toArray_toIterM [LawfulMonad m] {array : Array β} :