move, cleanup

Author: kim-em

Batteries.lean

@@ -11,6 +11,7 @@ import Batteries.Control.ForInStep
 import Batteries.Control.ForInStep.Basic
 import Batteries.Control.ForInStep.Lemmas
 import Batteries.Control.Lemmas
+import Batteries.Control.Monad
 import Batteries.Control.Nondet.Basic
 import Batteries.Data.Array
 import Batteries.Data.AssocList

Batteries/Control/Monad.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+-- Note: this will be replaced by `_root_.map_inj_right_of_nonempty` in nightly-2025-02-07
+theorem _root_.LawfulFunctor.map_inj_right_of_nonempty [Functor f] [LawfulFunctor f] [Nonempty α]
+    {g : α → β} (h : ∀ {x y : α}, g x = g y → x = y) {x y : f α} :
+    g <$> x = g <$> y ↔ x = y := by
+  constructor
+  · open Classical in
+    let g' a := if h : ∃ b, g b = a then h.choose else Classical.ofNonempty
+    have g'g a : g' (g a) = a := by
+      simp only [exists_apply_eq_apply, ↓reduceDIte, g']
+      exact h (_ : ∃ b, g b = g a).choose_spec
+    intro h'
+    simpa only [Functor.map_map, g'g, id_map'] using congrArg (g' <$> ·) h'
+  · intro h'
+    rw [h']
+
+-- Note: this will be replaced by `_root_.map_inj_right` in nightly-2025-02-07
+theorem _root_.LawfulMonad.map_inj_right [Monad m] [LawfulMonad m]
+    {f : α → β} (h : ∀ {x y : α}, f x = f y → x = y) {x y : m α} :
+    f <$> x = f <$> y ↔ x = y := by
+  by_cases hempty : Nonempty α
+  · exact LawfulFunctor.map_inj_right_of_nonempty h
+  · constructor
+    · intro h'
+      have (z : m α) : z = (do let a ← z; let b ← pure (f a); x) := by
+        conv => lhs; rw [← bind_pure z]
+        congr; funext a
+        exact (hempty ⟨a⟩).elim
+      rw [this x, this y]
+      rw [← bind_assoc, ← map_eq_pure_bind, h', map_eq_pure_bind, bind_assoc]
+    · intro h'
+      rw [h']

Batteries/Data/Vector/Monadic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Batteries.Classes.SatisfiesM
+import Batteries.Control.Monad
 import Batteries.Data.Array.Monadic
 
 namespace Vector
@@ -29,36 +30,6 @@ theorem toArray_mapIdxM [Monad m] [LawfulMonad m] (a : Vector α n) (f : Nat →
     toArray <$> a.mapIdxM f = a.toArray.mapIdxM f := by
   exact toArray_mapFinIdxM _ _
 
-theorem _root_.LawfulFunctor.map_inj_right_of_nonempty [Functor f] [LawfulFunctor f] [Nonempty α]
-    {g : α → β} (h : ∀ {x y : α}, g x = g y → x = y) {x y : f α} :
-    g <$> x = g <$> y ↔ x = y := by
-  constructor
-  · open Classical in
-    let g' a := if h : ∃ b, g b = a then h.choose else Classical.ofNonempty
-    have g'g a : g' (g a) = a := by
-      simp only [exists_apply_eq_apply, ↓reduceDIte, g']
-      exact h (_ : ∃ b, g b = g a).choose_spec
-    intro h'
-    simpa only [Functor.map_map, g'g, id_map'] using congrArg (g' <$> ·) h'
-  · intro h'
-    rw [h']
-
-theorem _root_.LawfulMonad.map_inj_right [Monad m] [LawfulMonad m]
-    {f : α → β} (h : ∀ {x y : α}, f x = f y → x = y) {x y : m α} :
-    f <$> x = f <$> y ↔ x = y := by
-  by_cases hempty : Nonempty α
-  · exact LawfulFunctor.map_inj_right_of_nonempty h
-  · constructor
-    · intro h'
-      have (z : m α) : z = (do let a ← z; let b ← pure (f a); x) := by
-        conv => lhs; rw [← bind_pure z]
-        congr; funext a
-        exact (hempty ⟨a⟩).elim
-      rw [this x, this y]
-      rw [← bind_assoc, ← map_eq_pure_bind, h', map_eq_pure_bind, bind_assoc]
-    · intro h'
-      rw [h']
-
 theorem mapM_mk [Monad m] [LawfulMonad m] [MonadSatisfying m]
     (a : Array α) (h : a.size = n) (f : α → m β) :
     (Vector.mk a h).mapM f =