From 8890a316cf0b49f6b14a695db3d04426ac91e9ce Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 8 Nov 2024 17:00:03 +1100
Subject: [PATCH 01/12] feat: sugar for SatisfiesM

.

.
---
 Batteries.lean                    |   2 +
 Batteries/Classes/SatisfiesM.lean | 117 +++++++++++++++++++++++++++++-
 Batteries/Lean/EStateM.lean       |  40 ++++++++++
 Batteries/Lean/Except.lean        |  51 ++++++++++++-
 Batteries/Lean/SatisfiesM.lean    |  28 +++++++
 BatteriesTest/satisfying.lean     |  21 ++++++
 6 files changed, 255 insertions(+), 4 deletions(-)
 create mode 100644 Batteries/Lean/EStateM.lean
 create mode 100644 Batteries/Lean/SatisfiesM.lean
 create mode 100644 BatteriesTest/satisfying.lean

diff --git a/Batteries.lean b/Batteries.lean
index 7e5c73f5fd..a370ec56d8 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -38,6 +38,7 @@ import Batteries.Data.UnionFind
 import Batteries.Data.Vector
 import Batteries.Lean.AttributeExtra
 import Batteries.Lean.Delaborator
+import Batteries.Lean.EStateM
 import Batteries.Lean.Except
 import Batteries.Lean.Expr
 import Batteries.Lean.Float
@@ -59,6 +60,7 @@ import Batteries.Lean.NameMapAttribute
 import Batteries.Lean.PersistentHashMap
 import Batteries.Lean.PersistentHashSet
 import Batteries.Lean.Position
+import Batteries.Lean.SatisfiesM
 import Batteries.Lean.Syntax
 import Batteries.Lean.System.IO
 import Batteries.Lean.TagAttribute
diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index 89f264963a..ec0330a4cf 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -1,8 +1,10 @@
 /-
 Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
+Authors: Mario Carneiro, Kim Morrison
 -/
+import Batteries.Lean.EStateM
+import Batteries.Lean.Except
 
 /-!
 ## SatisfiesM
@@ -12,6 +14,13 @@ and enables Hoare-like reasoning over monadic expressions. For example, given a
 function `f : α → m β`, to say that the return value of `f` satisfies `Q` whenever
 the input satisfies `P`, we write `∀ a, P a → SatisfiesM Q (f a)`.
 
+For any monad equipped with `Satisfying m`
+one can lift `SatisfiesM` to a monadic value in `Subtype`,
+using `satisfying x h : m {a // p a}`, where `x : m α` and `h : SatisfiesM p x`.
+This includes `Option`, `ReaderT`, `StateT`, and `ExceptT`, and the Lean monad stack.
+(Although it is not entirely clear one should treat the Lean monad stack as lawful,
+even though Lean accepts this.)
+
 ## Notes
 
 `SatisfiesM` is not yet a satisfactory solution for verifying the behaviour of large scale monadic
@@ -23,7 +32,7 @@ presumably requiring more syntactic support (and smarter `do` blocks) from Lean.
 Or it may be that such a solution will look different!
 This is an open research program, and for now one should not be overly ambitious using `SatisfiesM`.
 
-In particular lemmas about pure operations on data structures in `batteries` except for `HashMap`
+In particular lemmas about pure operations on data structures in `Batteries` except for `HashMap`
 should avoid `SatisfiesM` for now, so that it is easy to migrate to other approaches in future.
 -/
 
@@ -158,6 +167,23 @@ end SatisfiesM
   ⟨by revert x; intro | .ok _, ⟨.ok ⟨_, h⟩, rfl⟩, _, rfl => exact h,
    fun h => match x with | .ok a => ⟨.ok ⟨a, h _ rfl⟩, rfl⟩ | .error e => ⟨.error e, rfl⟩⟩
 
+@[simp] theorem SatisfiesM_EStateM_eq :
+    SatisfiesM (m := EStateM ε σ) p x ↔ ∀ s a s', x.run s = .ok a s' → p a := by
+  constructor
+  · rintro ⟨x, rfl⟩ s a s' h
+    match w : x.run s with
+    | .ok a s' => simp at h; exact h.1
+    | .error e s' => simp [w] at h
+  · intro w
+    refine ⟨?_, ?_⟩
+    · intro s
+      match q : x.run s with
+      | .ok a s' => exact .ok ⟨a, w s a s' q⟩ s'
+      | .error e s' => exact .error e s'
+    · ext s
+      rw [EStateM.run_map, EStateM.run]
+      split <;> simp_all
+
 @[simp] theorem SatisfiesM_ReaderT_eq [Monad m] :
     SatisfiesM (m := ReaderT ρ m) p x ↔ ∀ s, SatisfiesM p (x s) :=
   (exists_congr fun a => by exact ⟨fun eq _ => eq ▸ rfl, funext⟩).trans Classical.skolem.symm
@@ -174,9 +200,94 @@ theorem SatisfiesM_StateRefT_eq [Monad m] :
     show _ >>= _ = _; simp [← h]
 
 @[simp] theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
-    SatisfiesM (m := ExceptT ρ m) (α := α) p x ↔ SatisfiesM (m := m) (∀ a, · = .ok a → p a) x := by
+    SatisfiesM (m := ExceptT ρ m) (α := α) p x ↔
+      SatisfiesM (m := m) (∀ a, · = .ok a → p a) x.run := by
+  change _ ↔ SatisfiesM (m := m) (∀ a, · = .ok a → p a) x
   refine ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, eq⟩ => eq ▸ ?_⟩
   · exists (fun | .ok ⟨a, h⟩ => ⟨.ok a, fun | _, rfl => h⟩ | .error e => ⟨.error e, nofun⟩) <$> f
     show _ = _ >>= _; rw [← comp_map, map_eq_pure_bind]; congr; funext a; cases a <;> rfl
   · exists ((fun | ⟨.ok a, h⟩ => .ok ⟨a, h _ rfl⟩ | ⟨.error e, _⟩ => .error e) <$> f : m _)
     show _ >>= _ = _; simp [← comp_map, ← bind_pure_comp]; congr; funext ⟨a, h⟩; cases a <;> rfl
+
+/--
+If a monad has `Satisfying m`, then we can lift a `h : SatisfiesM (m := m) p x` predicate
+to monadic value `satisfying x p : m { x // p x }`.
+
+Reader, state, and exception monads have `Satisfying` instances if the base monad does.
+-/
+class Satisfying (m : Type u → Type v) [Functor m] where
+  /-- Lift a `SatisfiesM` predicate to a monadic value. -/
+  satisfying {p : α → Prop} (x : m α) (h : SatisfiesM (m := m) p x) :
+    { y : m {a // p a} // Subtype.val <$> y = x }
+
+export Satisfying (satisfying)
+
+instance : Satisfying Id where
+  satisfying x h := ⟨⟨x, by obtain ⟨⟨_, h⟩, rfl⟩ := h; exact h⟩, rfl⟩
+
+instance : Satisfying Option where
+  satisfying x? h :=
+  have h' := SatisfiesM_Option_eq.mp h
+  { val := match x? with
+    | none => none
+    | some x => some ⟨x, h' x rfl⟩
+    property := by cases x? <;> simp }
+
+instance : Satisfying (Except ε) where
+  satisfying x? h :=
+  have h' := SatisfiesM_Except_eq.mp h
+  { val := match x? with
+    | .ok x => .ok ⟨x, h' x rfl⟩
+    | .error e => .error e
+    property := by cases x? <;> simp }
+
+-- This will be redundant after nightly-2024-11-08.
+attribute [ext] ReaderT.ext
+
+instance [Monad m] [Satisfying m] : Satisfying (ReaderT ρ m) where
+  satisfying x h :=
+  have h' := SatisfiesM_ReaderT_eq.mp h
+  { val := fun r => (satisfying (x.run r) (h' r)).val
+    property := by
+      ext r
+      let t := satisfying (x.run r) (h' r)
+      rw [ReaderT.run_map, ← t.2]
+      rfl }
+
+instance [Monad m] [Satisfying m] : Satisfying (StateRefT' ω σ m) :=
+  inferInstanceAs <| Satisfying (ReaderT _ _)
+
+-- This will be redundant after nightly-2024-11-08.
+attribute [ext] StateT.ext
+
+instance [Monad m] [LawfulMonad m] [Satisfying m] : Satisfying (StateT ρ m) where
+  satisfying x h :=
+  have h' := SatisfiesM_StateT_eq.mp h
+  { val := fun r => (fun ⟨⟨a, r'⟩, h⟩ => ⟨⟨a, h⟩, r'⟩) <$> (satisfying (x.run r) (h' r)).1
+    property := by
+      ext r
+      rw [← (satisfying (x.run r) (h' r)).2, StateT.run_map]
+      simp [StateT.run] }
+
+instance [Monad m] [LawfulMonad m] [Satisfying m] : Satisfying (ExceptT ε m) where
+  satisfying x h :=
+  have h' := SatisfiesM_ExceptT_eq.mp h
+  have x' := satisfying x.run h'
+  { val := ExceptT.mk ((fun ⟨y, w⟩ => y.pmap fun a h => ⟨a, w _ h⟩) <$> x'.1)
+    property := by
+      ext
+      simp [← x'.2] }
+
+instance : Satisfying (EStateM ε σ) where
+  satisfying x h :=
+  have h' := SatisfiesM_EStateM_eq.mp h
+  { val := fun s => match w : x.run s with
+    | .ok a s' => .ok ⟨a, h' s a s' w⟩ s'
+    | .error e s' => .error e s'
+    property := by
+      ext s
+      rw [EStateM.run_map, EStateM.run]
+      split <;> simp_all }
+
+instance : Satisfying (EIO ε) := inferInstanceAs <| Satisfying (EStateM _ _)
+instance : Satisfying IO := inferInstanceAs <| Satisfying (EIO _)
diff --git a/Batteries/Lean/EStateM.lean b/Batteries/Lean/EStateM.lean
new file mode 100644
index 0000000000..84049c3560
--- /dev/null
+++ b/Batteries/Lean/EStateM.lean
@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+namespace EStateM
+
+namespace Result
+
+/-- Map a function over an `EStateM.Result`, preserving states and errors. -/
+def map {ε σ α β : Type u} (f : α → β) (x : Result ε σ α) : Result ε σ β :=
+  match x with
+  | .ok a s' => .ok (f a) s'
+  | .error e s' => .error e s'
+
+@[simp] theorem map_ok {ε σ α β : Type u} (f : α → β) (a : α) (s : σ) :
+    (Result.ok a s : Result ε σ α).map f = .ok (f a) s := rfl
+
+@[simp] theorem map_error {ε σ α β : Type u} (f : α → β) (e : ε) (s : σ) :
+    (Result.error e s : Result ε σ α).map f = .error e s := rfl
+
+@[simp] theorem map_eq_ok {ε σ α β : Type u} (f : α → β) (x : Result ε σ α) (b : β) (s : σ) :
+    x.map f = .ok b s ↔ ∃ a, x = .ok a s ∧ b = f a := by
+  cases x <;> simp [and_assoc, and_comm, eq_comm]
+
+@[simp] theorem map_eq_error {ε σ α β : Type u} (f : α → β) (x : Result ε σ α) (e : ε) (s : σ) :
+    x.map f = .error e s ↔ x = .error e s := by
+  cases x <;> simp [eq_comm]
+
+end Result
+
+@[simp] theorem run_map (f : α → β) (x : EStateM ε σ α) :
+    (f <$> x).run s = (x.run s).map f := rfl
+
+@[ext] theorem ext {ε σ α : Type u} (x y : EStateM ε σ α) (h : ∀ s, x.run s = y.run s) : x = y := by
+  funext s
+  exact h s
+
+end EStateM
diff --git a/Batteries/Lean/Except.lean b/Batteries/Lean/Except.lean
index 802d6b5161..e0eb4c79f5 100644
--- a/Batteries/Lean/Except.lean
+++ b/Batteries/Lean/Except.lean
@@ -7,7 +7,56 @@ import Lean.Util.Trace
 
 open Lean
 
+namespace Except
+
 /-- Visualize an `Except` using a checkmark or a cross. -/
-def Except.emoji : Except ε α → String
+def emoji : Except ε α → String
   | .error _ => crossEmoji
   | .ok _ => checkEmoji
+
+@[simp] theorem map_error {ε : Type u} (f : α → β) (e : ε) :
+    f <$> (.error e : Except ε α) = .error e := rfl
+
+@[simp] theorem map_ok {ε : Type u} (f : α → β) (x : α) :
+    f <$> (.ok x : Except ε α) = .ok (f x) := rfl
+
+/-- Map a function over an `Except` value, using a proof that the value is `.ok`. -/
+def pmap {ε : Type u} {α β : Type v} (x : Except ε α) (f : (a : α) → x = .ok a → β) : Except ε β :=
+  match x with
+  | .error e => .error e
+  | .ok a => .ok (f a rfl)
+
+@[simp] theorem pmap_error {ε : Type u} {α β : Type v} (e : ε)
+    (f : (a : α) → Except.error e = Except.ok a → β) :
+    Except.pmap (.error e) f = .error e := rfl
+
+@[simp] theorem pmap_ok {ε : Type u} {α β : Type v} (a : α)
+    (f : (a' : α) → (.ok a : Except ε α) = .ok a' → β) :
+    Except.pmap (.ok a) f = .ok (f a rfl) := rfl
+
+@[simp] theorem pmap_id {ε : Type u} {α : Type v} (x : Except ε α) :
+    x.pmap (fun a _ => a) = x := by cases x <;> simp
+
+@[simp] theorem map_pmap (g : β → γ) (x : Except ε α) (f : (a : α) → x = .ok a → β) :
+    g <$> x.pmap f = x.pmap fun a h => g (f a h) := by
+  cases x <;> simp
+
+end Except
+
+namespace ExceptT
+
+-- This will be redundant after nightly-2024-11-08.
+attribute [ext] ExceptT.ext
+
+@[simp] theorem run_mk {m : Type u → Type v} (x : m (Except ε α)) : (ExceptT.mk x).run = x := rfl
+@[simp] theorem mk_run (x : ExceptT ε m α) : ExceptT.mk (ExceptT.run x) = x := rfl
+
+@[simp]
+theorem map_mk [Monad m] [LawfulMonad m] (f : α → β) (x : m (Except ε α)) :
+    f <$> ExceptT.mk x = ExceptT.mk ((f <$> · ) <$> x) := by
+  simp only [Functor.map, Except.map, ExceptT.map, map_eq_pure_bind]
+  congr
+  funext a
+  split <;> simp
+
+end ExceptT
diff --git a/Batteries/Lean/SatisfiesM.lean b/Batteries/Lean/SatisfiesM.lean
new file mode 100644
index 0000000000..0267eef57b
--- /dev/null
+++ b/Batteries/Lean/SatisfiesM.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Batteries.Classes.SatisfiesM
+import Lean.Elab.Command
+
+/-!
+# Construct `Satisfying` instances for the Lean monad stack.
+-/
+
+open Lean Elab Term Tactic Command
+
+instance : Satisfying CoreM :=
+  inferInstanceAs <| Satisfying (ReaderT _ <| StateRefT' _ _ (EIO _))
+
+instance : Satisfying MetaM :=
+  inferInstanceAs <| Satisfying (ReaderT _ <| StateRefT' _ _ CoreM)
+
+instance : Satisfying TermElabM :=
+  inferInstanceAs <| Satisfying (ReaderT _ <| StateRefT' _ _ MetaM)
+
+instance : Satisfying TacticM :=
+  inferInstanceAs <| Satisfying (ReaderT _ $ StateRefT' _ _ TermElabM)
+
+instance : Satisfying CommandElabM :=
+  inferInstanceAs <| Satisfying (ReaderT _ $ StateRefT' _ _ (EIO _))
diff --git a/BatteriesTest/satisfying.lean b/BatteriesTest/satisfying.lean
new file mode 100644
index 0000000000..d95f8d9a40
--- /dev/null
+++ b/BatteriesTest/satisfying.lean
@@ -0,0 +1,21 @@
+import Batteries.Lean.SatisfiesM
+import Batteries.Data.Array.Monadic
+
+open Lean Meta Array Elab Term Tactic Command
+
+-- For now these live in the test file, as it's not really clear we want people relying on them!
+instance : LawfulMonad (EIO ε) := inferInstanceAs <| LawfulMonad (EStateM _ _)
+instance : LawfulMonad CoreM :=
+  inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ (EIO Exception))
+instance : LawfulMonad MetaM :=
+  inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ CoreM)
+instance : LawfulMonad TermElabM :=
+  inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ MetaM)
+instance : LawfulMonad TacticM :=
+  inferInstanceAs <| LawfulMonad (ReaderT _ $ StateRefT' _ _ $ TermElabM)
+instance : LawfulMonad CommandElabM :=
+  inferInstanceAs <| LawfulMonad (ReaderT _ $ StateRefT' _ _ $ EIO _)
+
+example (xs : Array Expr) : MetaM { ts : Array Expr // ts.size = xs.size } := do
+  let r ← satisfying (xs.mapM inferType) (size_mapM _ _)
+  return r

From ac56c2d0531db2b0efe6207cd447c4d645123317 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 8 Nov 2024 17:11:03 +1100
Subject: [PATCH 02/12] change the syntax

---
 Batteries/Classes/SatisfiesM.lean | 33 ++++++++++++++++---------------
 Batteries/Data/HashMap/Basic.lean |  2 +-
 BatteriesTest/satisfying.lean     |  2 +-
 3 files changed, 19 insertions(+), 18 deletions(-)

diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index ec0330a4cf..da0db7cfc9 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -185,14 +185,15 @@ end SatisfiesM
       split <;> simp_all
 
 @[simp] theorem SatisfiesM_ReaderT_eq [Monad m] :
-    SatisfiesM (m := ReaderT ρ m) p x ↔ ∀ s, SatisfiesM p (x s) :=
+    SatisfiesM (m := ReaderT ρ m) p x ↔ ∀ s, SatisfiesM p (x.run s) :=
   (exists_congr fun a => by exact ⟨fun eq _ => eq ▸ rfl, funext⟩).trans Classical.skolem.symm
 
 theorem SatisfiesM_StateRefT_eq [Monad m] :
-    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by simp
+    SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by simp [ReaderT.run]
 
 @[simp] theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] :
-    SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x s) := by
+    SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x.run s) := by
+  change SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x s)
   refine .trans ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, h⟩ => ?_⟩ Classical.skolem.symm
   · refine ⟨fun s => (fun ⟨⟨a, h⟩, s'⟩ => ⟨⟨a, s'⟩, h⟩) <$> f s, fun s => ?_⟩
     rw [← comp_map, map_eq_pure_bind]; rfl
@@ -217,16 +218,16 @@ Reader, state, and exception monads have `Satisfying` instances if the base mona
 -/
 class Satisfying (m : Type u → Type v) [Functor m] where
   /-- Lift a `SatisfiesM` predicate to a monadic value. -/
-  satisfying {p : α → Prop} (x : m α) (h : SatisfiesM (m := m) p x) :
+  satisfying {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) :
     { y : m {a // p a} // Subtype.val <$> y = x }
 
 export Satisfying (satisfying)
 
 instance : Satisfying Id where
-  satisfying x h := ⟨⟨x, by obtain ⟨⟨_, h⟩, rfl⟩ := h; exact h⟩, rfl⟩
+  satisfying {α p x} h := ⟨⟨x, by obtain ⟨⟨_, h⟩, rfl⟩ := h; exact h⟩, rfl⟩
 
 instance : Satisfying Option where
-  satisfying x? h :=
+  satisfying {α p x?} h :=
   have h' := SatisfiesM_Option_eq.mp h
   { val := match x? with
     | none => none
@@ -234,7 +235,7 @@ instance : Satisfying Option where
     property := by cases x? <;> simp }
 
 instance : Satisfying (Except ε) where
-  satisfying x? h :=
+  satisfying {α p x?} h :=
   have h' := SatisfiesM_Except_eq.mp h
   { val := match x? with
     | .ok x => .ok ⟨x, h' x rfl⟩
@@ -245,12 +246,12 @@ instance : Satisfying (Except ε) where
 attribute [ext] ReaderT.ext
 
 instance [Monad m] [Satisfying m] : Satisfying (ReaderT ρ m) where
-  satisfying x h :=
+  satisfying {α p x} h :=
   have h' := SatisfiesM_ReaderT_eq.mp h
-  { val := fun r => (satisfying (x.run r) (h' r)).val
+  { val := fun r => (satisfying (h' r)).val
     property := by
       ext r
-      let t := satisfying (x.run r) (h' r)
+      let t := satisfying (h' r)
       rw [ReaderT.run_map, ← t.2]
       rfl }
 
@@ -261,25 +262,25 @@ instance [Monad m] [Satisfying m] : Satisfying (StateRefT' ω σ m) :=
 attribute [ext] StateT.ext
 
 instance [Monad m] [LawfulMonad m] [Satisfying m] : Satisfying (StateT ρ m) where
-  satisfying x h :=
+  satisfying {α p x} h :=
   have h' := SatisfiesM_StateT_eq.mp h
-  { val := fun r => (fun ⟨⟨a, r'⟩, h⟩ => ⟨⟨a, h⟩, r'⟩) <$> (satisfying (x.run r) (h' r)).1
+  { val := fun r => (fun ⟨⟨a, r'⟩, h⟩ => ⟨⟨a, h⟩, r'⟩) <$> (satisfying (h' r)).1
     property := by
       ext r
-      rw [← (satisfying (x.run r) (h' r)).2, StateT.run_map]
+      rw [← (satisfying (h' r)).2, StateT.run_map]
       simp [StateT.run] }
 
 instance [Monad m] [LawfulMonad m] [Satisfying m] : Satisfying (ExceptT ε m) where
-  satisfying x h :=
+  satisfying {α p x} h :=
   have h' := SatisfiesM_ExceptT_eq.mp h
-  have x' := satisfying x.run h'
+  have x' := satisfying h'
   { val := ExceptT.mk ((fun ⟨y, w⟩ => y.pmap fun a h => ⟨a, w _ h⟩) <$> x'.1)
     property := by
       ext
       simp [← x'.2] }
 
 instance : Satisfying (EStateM ε σ) where
-  satisfying x h :=
+  satisfying {α p x} h :=
   have h' := SatisfiesM_EStateM_eq.mp h
   { val := fun s => match w : x.run s with
     | .ok a s' => .ok ⟨a, h' s a s' w⟩ s'
diff --git a/Batteries/Data/HashMap/Basic.lean b/Batteries/Data/HashMap/Basic.lean
index 3fd1d3350d..de029c4276 100644
--- a/Batteries/Data/HashMap/Basic.lean
+++ b/Batteries/Data/HashMap/Basic.lean
@@ -202,7 +202,7 @@ Applies `f` to each key-value pair `a, b` in the map. If it returns `some c` the
   have : m'.1.size > 0 := by
     have := Array.size_mapM (m := StateT (ULift Nat) Id) (go .nil) m.buckets.1
     simp [SatisfiesM_StateT_eq, SatisfiesM_Id_eq] at this
-    simp [this, Id.run, StateT.run, m.2.2, m']
+    simp [this, Id.run, m.2.2, m']
   ⟨m'.2.1, m'.1, this⟩
 where
   /-- Inner loop of `filterMap`. Note that this reverses the bucket lists,
diff --git a/BatteriesTest/satisfying.lean b/BatteriesTest/satisfying.lean
index d95f8d9a40..27c7c29e04 100644
--- a/BatteriesTest/satisfying.lean
+++ b/BatteriesTest/satisfying.lean
@@ -17,5 +17,5 @@ instance : LawfulMonad CommandElabM :=
   inferInstanceAs <| LawfulMonad (ReaderT _ $ StateRefT' _ _ $ EIO _)
 
 example (xs : Array Expr) : MetaM { ts : Array Expr // ts.size = xs.size } := do
-  let r ← satisfying (xs.mapM inferType) (size_mapM _ _)
+  let r ← satisfying (xs.size_mapM inferType)
   return r

From a61fce165fa27c6c58e858c920925faac32881b0 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 11 Nov 2024 10:50:20 +1100
Subject: [PATCH 03/12] rename to MonadSatisfying

---
 Batteries/Classes/SatisfiesM.lean | 33 ++++++++++++++++---------------
 Batteries/Lean/SatisfiesM.lean    | 22 ++++++++++-----------
 2 files changed, 28 insertions(+), 27 deletions(-)

diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index da0db7cfc9..275a1adc44 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -14,7 +14,7 @@ and enables Hoare-like reasoning over monadic expressions. For example, given a
 function `f : α → m β`, to say that the return value of `f` satisfies `Q` whenever
 the input satisfies `P`, we write `∀ a, P a → SatisfiesM Q (f a)`.
 
-For any monad equipped with `Satisfying m`
+For any monad equipped with `MonadSatisfying m`
 one can lift `SatisfiesM` to a monadic value in `Subtype`,
 using `satisfying x h : m {a // p a}`, where `x : m α` and `h : SatisfiesM p x`.
 This includes `Option`, `ReaderT`, `StateT`, and `ExceptT`, and the Lean monad stack.
@@ -211,22 +211,22 @@ theorem SatisfiesM_StateRefT_eq [Monad m] :
     show _ >>= _ = _; simp [← comp_map, ← bind_pure_comp]; congr; funext ⟨a, h⟩; cases a <;> rfl
 
 /--
-If a monad has `Satisfying m`, then we can lift a `h : SatisfiesM (m := m) p x` predicate
+If a monad has `MonadSatisfying m`, then we can lift a `h : SatisfiesM (m := m) p x` predicate
 to monadic value `satisfying x p : m { x // p x }`.
 
-Reader, state, and exception monads have `Satisfying` instances if the base monad does.
+Reader, state, and exception monads have `MonadSatisfying` instances if the base monad does.
 -/
-class Satisfying (m : Type u → Type v) [Functor m] where
+class MonadSatisfying (m : Type u → Type v) [Functor m] where
   /-- Lift a `SatisfiesM` predicate to a monadic value. -/
   satisfying {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) :
     { y : m {a // p a} // Subtype.val <$> y = x }
 
-export Satisfying (satisfying)
+export MonadSatisfying (satisfying)
 
-instance : Satisfying Id where
+instance : MonadSatisfying Id where
   satisfying {α p x} h := ⟨⟨x, by obtain ⟨⟨_, h⟩, rfl⟩ := h; exact h⟩, rfl⟩
 
-instance : Satisfying Option where
+instance : MonadSatisfying Option where
   satisfying {α p x?} h :=
   have h' := SatisfiesM_Option_eq.mp h
   { val := match x? with
@@ -234,7 +234,7 @@ instance : Satisfying Option where
     | some x => some ⟨x, h' x rfl⟩
     property := by cases x? <;> simp }
 
-instance : Satisfying (Except ε) where
+instance : MonadSatisfying (Except ε) where
   satisfying {α p x?} h :=
   have h' := SatisfiesM_Except_eq.mp h
   { val := match x? with
@@ -245,7 +245,7 @@ instance : Satisfying (Except ε) where
 -- This will be redundant after nightly-2024-11-08.
 attribute [ext] ReaderT.ext
 
-instance [Monad m] [Satisfying m] : Satisfying (ReaderT ρ m) where
+instance [Monad m] [MonadSatisfying m] : MonadSatisfying (ReaderT ρ m) where
   satisfying {α p x} h :=
   have h' := SatisfiesM_ReaderT_eq.mp h
   { val := fun r => (satisfying (h' r)).val
@@ -255,13 +255,13 @@ instance [Monad m] [Satisfying m] : Satisfying (ReaderT ρ m) where
       rw [ReaderT.run_map, ← t.2]
       rfl }
 
-instance [Monad m] [Satisfying m] : Satisfying (StateRefT' ω σ m) :=
-  inferInstanceAs <| Satisfying (ReaderT _ _)
+instance [Monad m] [MonadSatisfying m] : MonadSatisfying (StateRefT' ω σ m) :=
+  inferInstanceAs <| MonadSatisfying (ReaderT _ _)
 
 -- This will be redundant after nightly-2024-11-08.
 attribute [ext] StateT.ext
 
-instance [Monad m] [LawfulMonad m] [Satisfying m] : Satisfying (StateT ρ m) where
+instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateT ρ m) where
   satisfying {α p x} h :=
   have h' := SatisfiesM_StateT_eq.mp h
   { val := fun r => (fun ⟨⟨a, r'⟩, h⟩ => ⟨⟨a, h⟩, r'⟩) <$> (satisfying (h' r)).1
@@ -270,7 +270,7 @@ instance [Monad m] [LawfulMonad m] [Satisfying m] : Satisfying (StateT ρ m) whe
       rw [← (satisfying (h' r)).2, StateT.run_map]
       simp [StateT.run] }
 
-instance [Monad m] [LawfulMonad m] [Satisfying m] : Satisfying (ExceptT ε m) where
+instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (ExceptT ε m) where
   satisfying {α p x} h :=
   have h' := SatisfiesM_ExceptT_eq.mp h
   have x' := satisfying h'
@@ -279,7 +279,7 @@ instance [Monad m] [LawfulMonad m] [Satisfying m] : Satisfying (ExceptT ε m) wh
       ext
       simp [← x'.2] }
 
-instance : Satisfying (EStateM ε σ) where
+instance : MonadSatisfying (EStateM ε σ) where
   satisfying {α p x} h :=
   have h' := SatisfiesM_EStateM_eq.mp h
   { val := fun s => match w : x.run s with
@@ -290,5 +290,6 @@ instance : Satisfying (EStateM ε σ) where
       rw [EStateM.run_map, EStateM.run]
       split <;> simp_all }
 
-instance : Satisfying (EIO ε) := inferInstanceAs <| Satisfying (EStateM _ _)
-instance : Satisfying IO := inferInstanceAs <| Satisfying (EIO _)
+instance : MonadSatisfying (EIO ε) := inferInstanceAs <| MonadSatisfying (EStateM _ _)
+instance : MonadSatisfying BaseIO := inferInstanceAs <| MonadSatisfying (EIO _)
+instance : MonadSatisfying IO := inferInstanceAs <| MonadSatisfying (EIO _)
diff --git a/Batteries/Lean/SatisfiesM.lean b/Batteries/Lean/SatisfiesM.lean
index 0267eef57b..fd008ae1e3 100644
--- a/Batteries/Lean/SatisfiesM.lean
+++ b/Batteries/Lean/SatisfiesM.lean
@@ -7,22 +7,22 @@ import Batteries.Classes.SatisfiesM
 import Lean.Elab.Command
 
 /-!
-# Construct `Satisfying` instances for the Lean monad stack.
+# Construct `MonadSatisfying` instances for the Lean monad stack.
 -/
 
 open Lean Elab Term Tactic Command
 
-instance : Satisfying CoreM :=
-  inferInstanceAs <| Satisfying (ReaderT _ <| StateRefT' _ _ (EIO _))
+instance : MonadSatisfying CoreM :=
+  inferInstanceAs <| MonadSatisfying (ReaderT _ <| StateRefT' _ _ (EIO _))
 
-instance : Satisfying MetaM :=
-  inferInstanceAs <| Satisfying (ReaderT _ <| StateRefT' _ _ CoreM)
+instance : MonadSatisfying MetaM :=
+  inferInstanceAs <| MonadSatisfying (ReaderT _ <| StateRefT' _ _ CoreM)
 
-instance : Satisfying TermElabM :=
-  inferInstanceAs <| Satisfying (ReaderT _ <| StateRefT' _ _ MetaM)
+instance : MonadSatisfying TermElabM :=
+  inferInstanceAs <| MonadSatisfying (ReaderT _ <| StateRefT' _ _ MetaM)
 
-instance : Satisfying TacticM :=
-  inferInstanceAs <| Satisfying (ReaderT _ $ StateRefT' _ _ TermElabM)
+instance : MonadSatisfying TacticM :=
+  inferInstanceAs <| MonadSatisfying (ReaderT _ $ StateRefT' _ _ TermElabM)
 
-instance : Satisfying CommandElabM :=
-  inferInstanceAs <| Satisfying (ReaderT _ $ StateRefT' _ _ (EIO _))
+instance : MonadSatisfying CommandElabM :=
+  inferInstanceAs <| MonadSatisfying (ReaderT _ $ StateRefT' _ _ (EIO _))

From b9b7ab0efebec75abc9f06f3170c2445879a2e18 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 11 Nov 2024 10:59:55 +1100
Subject: [PATCH 04/12] two fields

---
 Batteries/Classes/SatisfiesM.lean | 72 ++++++++++++++++---------------
 BatteriesTest/satisfying.lean     |  2 +
 2 files changed, 40 insertions(+), 34 deletions(-)

diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index 275a1adc44..455a22d253 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -218,42 +218,44 @@ Reader, state, and exception monads have `MonadSatisfying` instances if the base
 -/
 class MonadSatisfying (m : Type u → Type v) [Functor m] where
   /-- Lift a `SatisfiesM` predicate to a monadic value. -/
-  satisfying {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) :
-    { y : m {a // p a} // Subtype.val <$> y = x }
+  satisfying {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : m {a // p a}
+  /-- The value of the lifted monadic value is equal to the original monadic value. -/
+  val_eq {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : Subtype.val <$> satisfying h = x
 
 export MonadSatisfying (satisfying)
 
 instance : MonadSatisfying Id where
-  satisfying {α p x} h := ⟨⟨x, by obtain ⟨⟨_, h⟩, rfl⟩ := h; exact h⟩, rfl⟩
+  satisfying {α p x} h := ⟨x, by obtain ⟨⟨_, h⟩, rfl⟩ := h; exact h⟩
+  val_eq {α p x} h := rfl
 
 instance : MonadSatisfying Option where
   satisfying {α p x?} h :=
-  have h' := SatisfiesM_Option_eq.mp h
-  { val := match x? with
+    have h' := SatisfiesM_Option_eq.mp h
+    match x? with
     | none => none
     | some x => some ⟨x, h' x rfl⟩
-    property := by cases x? <;> simp }
+  val_eq {α p x?} h := by cases x? <;> simp
 
 instance : MonadSatisfying (Except ε) where
   satisfying {α p x?} h :=
-  have h' := SatisfiesM_Except_eq.mp h
-  { val := match x? with
+    have h' := SatisfiesM_Except_eq.mp h
+    match x? with
     | .ok x => .ok ⟨x, h' x rfl⟩
     | .error e => .error e
-    property := by cases x? <;> simp }
+  val_eq {α p x?} h := by cases x? <;> simp
 
 -- This will be redundant after nightly-2024-11-08.
 attribute [ext] ReaderT.ext
 
 instance [Monad m] [MonadSatisfying m] : MonadSatisfying (ReaderT ρ m) where
   satisfying {α p x} h :=
-  have h' := SatisfiesM_ReaderT_eq.mp h
-  { val := fun r => (satisfying (h' r)).val
-    property := by
-      ext r
-      let t := satisfying (h' r)
-      rw [ReaderT.run_map, ← t.2]
-      rfl }
+    have h' := SatisfiesM_ReaderT_eq.mp h
+    fun r => satisfying (h' r)
+  val_eq {α p x} h := by
+    have h' := SatisfiesM_ReaderT_eq.mp h
+    ext r
+    rw [ReaderT.run_map, ← MonadSatisfying.val_eq (h' r)]
+    rfl
 
 instance [Monad m] [MonadSatisfying m] : MonadSatisfying (StateRefT' ω σ m) :=
   inferInstanceAs <| MonadSatisfying (ReaderT _ _)
@@ -263,32 +265,34 @@ attribute [ext] StateT.ext
 
 instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateT ρ m) where
   satisfying {α p x} h :=
-  have h' := SatisfiesM_StateT_eq.mp h
-  { val := fun r => (fun ⟨⟨a, r'⟩, h⟩ => ⟨⟨a, h⟩, r'⟩) <$> (satisfying (h' r)).1
-    property := by
-      ext r
-      rw [← (satisfying (h' r)).2, StateT.run_map]
-      simp [StateT.run] }
+    have h' := SatisfiesM_StateT_eq.mp h
+    fun r => (fun ⟨⟨a, r'⟩, h⟩ => ⟨⟨a, h⟩, r'⟩) <$> satisfying (h' r)
+  val_eq {α p x} h := by
+    have h' := SatisfiesM_StateT_eq.mp h
+    ext r
+    rw [← MonadSatisfying.val_eq (h' r), StateT.run_map]
+    simp [StateT.run]
 
 instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (ExceptT ε m) where
   satisfying {α p x} h :=
-  have h' := SatisfiesM_ExceptT_eq.mp h
-  have x' := satisfying h'
-  { val := ExceptT.mk ((fun ⟨y, w⟩ => y.pmap fun a h => ⟨a, w _ h⟩) <$> x'.1)
-    property := by
-      ext
-      simp [← x'.2] }
+    let x' := satisfying (SatisfiesM_ExceptT_eq.mp h)
+    ExceptT.mk ((fun ⟨y, w⟩ => y.pmap fun a h => ⟨a, w _ h⟩) <$> x')
+  val_eq {α p x} h:= by
+    ext
+    rw [← MonadSatisfying.val_eq (SatisfiesM_ExceptT_eq.mp h)]
+    simp
 
 instance : MonadSatisfying (EStateM ε σ) where
   satisfying {α p x} h :=
-  have h' := SatisfiesM_EStateM_eq.mp h
-  { val := fun s => match w : x.run s with
+    have h' := SatisfiesM_EStateM_eq.mp h
+    fun s => match w : x.run s with
     | .ok a s' => .ok ⟨a, h' s a s' w⟩ s'
     | .error e s' => .error e s'
-    property := by
-      ext s
-      rw [EStateM.run_map, EStateM.run]
-      split <;> simp_all }
+  val_eq {α p x} h := by
+    ext s
+    rw [EStateM.run_map, EStateM.run]
+    simp only
+    split <;> simp_all
 
 instance : MonadSatisfying (EIO ε) := inferInstanceAs <| MonadSatisfying (EStateM _ _)
 instance : MonadSatisfying BaseIO := inferInstanceAs <| MonadSatisfying (EIO _)
diff --git a/BatteriesTest/satisfying.lean b/BatteriesTest/satisfying.lean
index 27c7c29e04..96262541bd 100644
--- a/BatteriesTest/satisfying.lean
+++ b/BatteriesTest/satisfying.lean
@@ -5,6 +5,8 @@ open Lean Meta Array Elab Term Tactic Command
 
 -- For now these live in the test file, as it's not really clear we want people relying on them!
 instance : LawfulMonad (EIO ε) := inferInstanceAs <| LawfulMonad (EStateM _ _)
+instance : LawfulMonad BaseIO := inferInstanceAs <| LawfulMonad (EIO _)
+instance : LawfulMonad IO := inferInstanceAs <| LawfulMonad (EIO _)
 instance : LawfulMonad CoreM :=
   inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ (EIO Exception))
 instance : LawfulMonad MetaM :=

From 5be61c9268fa22a251a653d0be472a37b3f16d7b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 11 Nov 2024 11:25:06 +1100
Subject: [PATCH 05/12] csimp

---
 Batteries/Classes/SatisfiesM.lean | 32 +++++++++++++++++++++++++------
 Batteries/Lean/SatisfiesM.lean    |  8 ++++++++
 2 files changed, 34 insertions(+), 6 deletions(-)

diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index 455a22d253..ae47136079 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -216,7 +216,7 @@ to monadic value `satisfying x p : m { x // p x }`.
 
 Reader, state, and exception monads have `MonadSatisfying` instances if the base monad does.
 -/
-class MonadSatisfying (m : Type u → Type v) [Functor m] where
+class MonadSatisfying (m : Type u → Type v) [Functor m] [LawfulFunctor m]where
   /-- Lift a `SatisfiesM` predicate to a monadic value. -/
   satisfying {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : m {a // p a}
   /-- The value of the lifted monadic value is equal to the original monadic value. -/
@@ -224,6 +224,8 @@ class MonadSatisfying (m : Type u → Type v) [Functor m] where
 
 export MonadSatisfying (satisfying)
 
+namespace MonadSatisfying
+
 instance : MonadSatisfying Id where
   satisfying {α p x} h := ⟨x, by obtain ⟨⟨_, h⟩, rfl⟩ := h; exact h⟩
   val_eq {α p x} h := rfl
@@ -247,7 +249,7 @@ instance : MonadSatisfying (Except ε) where
 -- This will be redundant after nightly-2024-11-08.
 attribute [ext] ReaderT.ext
 
-instance [Monad m] [MonadSatisfying m] : MonadSatisfying (ReaderT ρ m) where
+instance [Monad m] [LawfulMonad m][MonadSatisfying m] : MonadSatisfying (ReaderT ρ m) where
   satisfying {α p x} h :=
     have h' := SatisfiesM_ReaderT_eq.mp h
     fun r => satisfying (h' r)
@@ -257,7 +259,7 @@ instance [Monad m] [MonadSatisfying m] : MonadSatisfying (ReaderT ρ m) where
     rw [ReaderT.run_map, ← MonadSatisfying.val_eq (h' r)]
     rfl
 
-instance [Monad m] [MonadSatisfying m] : MonadSatisfying (StateRefT' ω σ m) :=
+instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateRefT' ω σ m) :=
   inferInstanceAs <| MonadSatisfying (ReaderT _ _)
 
 -- This will be redundant after nightly-2024-11-08.
@@ -294,6 +296,24 @@ instance : MonadSatisfying (EStateM ε σ) where
     simp only
     split <;> simp_all
 
-instance : MonadSatisfying (EIO ε) := inferInstanceAs <| MonadSatisfying (EStateM _ _)
-instance : MonadSatisfying BaseIO := inferInstanceAs <| MonadSatisfying (EIO _)
-instance : MonadSatisfying IO := inferInstanceAs <| MonadSatisfying (EIO _)
+set_option linter.unusedVariables false in
+/--
+Since we assume `m` is lawful,
+we can replace the implementation of `satisfying` at runtime using the identity function
+and an unsafe "proof" via `lcProof`.
+
+This is purely a performance optimization, and could be omitted.
+-/
+unsafe def unsafeSatisfying {m : Type u → Type v} [Functor m] [LawfulFunctor m] [MonadSatisfying m]
+    {α} {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : m {a // p a} :=
+  (⟨·, lcProof⟩) <$> x
+
+/-- `unsafeSatisfying` is equivalent to `satisfying`. -/
+@[csimp] unsafe def satisfying_eq_unsafeSatisfying :
+    @satisfying = @unsafeSatisfying := by
+  funext m _ _ _ _ p x h
+  unfold unsafeSatisfying
+  conv => rhs; simp +singlePass [← MonadSatisfying.val_eq h]
+  simp
+
+end MonadSatisfying
diff --git a/Batteries/Lean/SatisfiesM.lean b/Batteries/Lean/SatisfiesM.lean
index fd008ae1e3..b08c8313e9 100644
--- a/Batteries/Lean/SatisfiesM.lean
+++ b/Batteries/Lean/SatisfiesM.lean
@@ -12,6 +12,14 @@ import Lean.Elab.Command
 
 open Lean Elab Term Tactic Command
 
+instance : LawfulMonad (EIO ε) := inferInstanceAs <| LawfulMonad (EStateM _ _)
+instance : LawfulMonad BaseIO := inferInstanceAs <| LawfulMonad (EIO _)
+instance : LawfulMonad IO := inferInstanceAs <| LawfulMonad (EIO _)
+
+instance : MonadSatisfying (EIO ε) := inferInstanceAs <| MonadSatisfying (EStateM _ _)
+instance : MonadSatisfying BaseIO := inferInstanceAs <| MonadSatisfying (EIO _)
+instance : MonadSatisfying IO := inferInstanceAs <| MonadSatisfying (EIO _)
+
 instance : MonadSatisfying CoreM :=
   inferInstanceAs <| MonadSatisfying (ReaderT _ <| StateRefT' _ _ (EIO _))
 

From 05150c74f9a8ac68234eec4695b829bde7778fe4 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 11 Nov 2024 11:30:20 +1100
Subject: [PATCH 06/12] nolints

---
 Batteries/Classes/SatisfiesM.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index ae47136079..ca6618127b 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Kim Morrison
 -/
 import Batteries.Lean.EStateM
 import Batteries.Lean.Except
+import Batteries.Tactic.Lint
 
 /-!
 ## SatisfiesM
@@ -304,12 +305,13 @@ and an unsafe "proof" via `lcProof`.
 
 This is purely a performance optimization, and could be omitted.
 -/
+@[nolint unusedArguments]
 unsafe def unsafeSatisfying {m : Type u → Type v} [Functor m] [LawfulFunctor m] [MonadSatisfying m]
     {α} {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : m {a // p a} :=
   (⟨·, lcProof⟩) <$> x
 
 /-- `unsafeSatisfying` is equivalent to `satisfying`. -/
-@[csimp] unsafe def satisfying_eq_unsafeSatisfying :
+@[csimp, nolint defLemma] unsafe def satisfying_eq_unsafeSatisfying :
     @satisfying = @unsafeSatisfying := by
   funext m _ _ _ _ p x h
   unfold unsafeSatisfying

From 952e9b1bebeaa5a6474f53bcdcbd9a4d2563263e Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 11 Nov 2024 13:34:50 +1100
Subject: [PATCH 07/12] remove @[simp]

---
 Batteries/Classes/SatisfiesM.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index ca6618127b..56285891ee 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -168,7 +168,7 @@ end SatisfiesM
   ⟨by revert x; intro | .ok _, ⟨.ok ⟨_, h⟩, rfl⟩, _, rfl => exact h,
    fun h => match x with | .ok a => ⟨.ok ⟨a, h _ rfl⟩, rfl⟩ | .error e => ⟨.error e, rfl⟩⟩
 
-@[simp] theorem SatisfiesM_EStateM_eq :
+theorem SatisfiesM_EStateM_eq :
     SatisfiesM (m := EStateM ε σ) p x ↔ ∀ s a s', x.run s = .ok a s' → p a := by
   constructor
   · rintro ⟨x, rfl⟩ s a s' h

From 976e40eb5e7f0b94fe8e00ef3b5a8259cb9ecbc0 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 11 Nov 2024 21:10:57 +1100
Subject: [PATCH 08/12] remove the csimp; let's do this in a separate PR

---
 Batteries/Classes/SatisfiesM.lean | 21 ---------------------
 1 file changed, 21 deletions(-)

diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index 56285891ee..0fe80e1f14 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -297,25 +297,4 @@ instance : MonadSatisfying (EStateM ε σ) where
     simp only
     split <;> simp_all
 
-set_option linter.unusedVariables false in
-/--
-Since we assume `m` is lawful,
-we can replace the implementation of `satisfying` at runtime using the identity function
-and an unsafe "proof" via `lcProof`.
-
-This is purely a performance optimization, and could be omitted.
--/
-@[nolint unusedArguments]
-unsafe def unsafeSatisfying {m : Type u → Type v} [Functor m] [LawfulFunctor m] [MonadSatisfying m]
-    {α} {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : m {a // p a} :=
-  (⟨·, lcProof⟩) <$> x
-
-/-- `unsafeSatisfying` is equivalent to `satisfying`. -/
-@[csimp, nolint defLemma] unsafe def satisfying_eq_unsafeSatisfying :
-    @satisfying = @unsafeSatisfying := by
-  funext m _ _ _ _ p x h
-  unfold unsafeSatisfying
-  conv => rhs; simp +singlePass [← MonadSatisfying.val_eq h]
-  simp
-
 end MonadSatisfying

From 1331cd95306aba2954410afe54b63dbad4ae92a7 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 11 Nov 2024 05:10:54 -0800
Subject: [PATCH 09/12] Update Batteries/Classes/SatisfiesM.lean

---
 Batteries/Classes/SatisfiesM.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean
index 0fe80e1f14..834cbbea68 100644
--- a/Batteries/Classes/SatisfiesM.lean
+++ b/Batteries/Classes/SatisfiesM.lean
@@ -217,7 +217,7 @@ to monadic value `satisfying x p : m { x // p x }`.
 
 Reader, state, and exception monads have `MonadSatisfying` instances if the base monad does.
 -/
-class MonadSatisfying (m : Type u → Type v) [Functor m] [LawfulFunctor m]where
+class MonadSatisfying (m : Type u → Type v) [Functor m] [LawfulFunctor m] where
   /-- Lift a `SatisfiesM` predicate to a monadic value. -/
   satisfying {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : m {a // p a}
   /-- The value of the lifted monadic value is equal to the original monadic value. -/

From 71779f2f4a730db8e5296356940bb39ab950d396 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 12 Nov 2024 14:13:37 +1100
Subject: [PATCH 10/12] move lawfulmonad instances

---
 Batteries/Lean/SatisfiesM.lean |  5 +----
 BatteriesTest/satisfying.lean  | 15 ---------------
 2 files changed, 1 insertion(+), 19 deletions(-)

diff --git a/Batteries/Lean/SatisfiesM.lean b/Batteries/Lean/SatisfiesM.lean
index b08c8313e9..b686913c27 100644
--- a/Batteries/Lean/SatisfiesM.lean
+++ b/Batteries/Lean/SatisfiesM.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.Lean.LawfulMonad
 import Lean.Elab.Command
 
 /-!
@@ -12,10 +13,6 @@ import Lean.Elab.Command
 
 open Lean Elab Term Tactic Command
 
-instance : LawfulMonad (EIO ε) := inferInstanceAs <| LawfulMonad (EStateM _ _)
-instance : LawfulMonad BaseIO := inferInstanceAs <| LawfulMonad (EIO _)
-instance : LawfulMonad IO := inferInstanceAs <| LawfulMonad (EIO _)
-
 instance : MonadSatisfying (EIO ε) := inferInstanceAs <| MonadSatisfying (EStateM _ _)
 instance : MonadSatisfying BaseIO := inferInstanceAs <| MonadSatisfying (EIO _)
 instance : MonadSatisfying IO := inferInstanceAs <| MonadSatisfying (EIO _)
diff --git a/BatteriesTest/satisfying.lean b/BatteriesTest/satisfying.lean
index 96262541bd..eadfbc6a66 100644
--- a/BatteriesTest/satisfying.lean
+++ b/BatteriesTest/satisfying.lean
@@ -3,21 +3,6 @@ import Batteries.Data.Array.Monadic
 
 open Lean Meta Array Elab Term Tactic Command
 
--- For now these live in the test file, as it's not really clear we want people relying on them!
-instance : LawfulMonad (EIO ε) := inferInstanceAs <| LawfulMonad (EStateM _ _)
-instance : LawfulMonad BaseIO := inferInstanceAs <| LawfulMonad (EIO _)
-instance : LawfulMonad IO := inferInstanceAs <| LawfulMonad (EIO _)
-instance : LawfulMonad CoreM :=
-  inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ (EIO Exception))
-instance : LawfulMonad MetaM :=
-  inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ CoreM)
-instance : LawfulMonad TermElabM :=
-  inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ MetaM)
-instance : LawfulMonad TacticM :=
-  inferInstanceAs <| LawfulMonad (ReaderT _ $ StateRefT' _ _ $ TermElabM)
-instance : LawfulMonad CommandElabM :=
-  inferInstanceAs <| LawfulMonad (ReaderT _ $ StateRefT' _ _ $ EIO _)
-
 example (xs : Array Expr) : MetaM { ts : Array Expr // ts.size = xs.size } := do
   let r ← satisfying (xs.size_mapM inferType)
   return r

From 5aacdf5a05a3b98f88338e191857dd2ed17689f8 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 12 Nov 2024 14:14:34 +1100
Subject: [PATCH 11/12] move instances

---
 Batteries.lean                  |  1 +
 Batteries/Lean/LawfulMonad.lean | 28 ++++++++++++++++++++++++++++
 2 files changed, 29 insertions(+)
 create mode 100644 Batteries/Lean/LawfulMonad.lean

diff --git a/Batteries.lean b/Batteries.lean
index a370ec56d8..e6464503cb 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -46,6 +46,7 @@ import Batteries.Lean.HashMap
 import Batteries.Lean.HashSet
 import Batteries.Lean.IO.Process
 import Batteries.Lean.Json
+import Batteries.Lean.LawfulMonad
 import Batteries.Lean.Meta.Basic
 import Batteries.Lean.Meta.DiscrTree
 import Batteries.Lean.Meta.Expr
diff --git a/Batteries/Lean/LawfulMonad.lean b/Batteries/Lean/LawfulMonad.lean
new file mode 100644
index 0000000000..e0260e4e01
--- /dev/null
+++ b/Batteries/Lean/LawfulMonad.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Batteries.Classes.SatisfiesM
+import Lean.Elab.Command
+
+/-!
+# Construct `LawfulMonad` instances for the Lean monad stack.
+-/
+
+open Lean Elab Term Tactic Command
+
+instance : LawfulMonad (EIO ε) := inferInstanceAs <| LawfulMonad (EStateM _ _)
+instance : LawfulMonad BaseIO := inferInstanceAs <| LawfulMonad (EIO _)
+instance : LawfulMonad IO := inferInstanceAs <| LawfulMonad (EIO _)
+
+instance : LawfulMonad CoreM :=
+  inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ (EIO Exception))
+instance : LawfulMonad MetaM :=
+  inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ CoreM)
+instance : LawfulMonad TermElabM :=
+  inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ MetaM)
+instance : LawfulMonad TacticM :=
+  inferInstanceAs <| LawfulMonad (ReaderT _ $ StateRefT' _ _ $ TermElabM)
+instance : LawfulMonad CommandElabM :=
+  inferInstanceAs <| LawfulMonad (ReaderT _ $ StateRefT' _ _ $ EIO _)

From abc7187ee8778494171a15c6db6f6f939dd93274 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 13 Nov 2024 11:11:37 +1100
Subject: [PATCH 12/12] another monad

---
 Batteries/Lean/LawfulMonad.lean | 2 ++
 Batteries/Lean/SatisfiesM.lean  | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/Batteries/Lean/LawfulMonad.lean b/Batteries/Lean/LawfulMonad.lean
index e0260e4e01..a69d5ad18f 100644
--- a/Batteries/Lean/LawfulMonad.lean
+++ b/Batteries/Lean/LawfulMonad.lean
@@ -16,6 +16,8 @@ instance : LawfulMonad (EIO ε) := inferInstanceAs <| LawfulMonad (EStateM _ _)
 instance : LawfulMonad BaseIO := inferInstanceAs <| LawfulMonad (EIO _)
 instance : LawfulMonad IO := inferInstanceAs <| LawfulMonad (EIO _)
 
+instance : LawfulMonad (EST ε σ) := inferInstanceAs <| LawfulMonad (EStateM _ _)
+
 instance : LawfulMonad CoreM :=
   inferInstanceAs <| LawfulMonad (ReaderT _ <| StateRefT' _ _ (EIO Exception))
 instance : LawfulMonad MetaM :=
diff --git a/Batteries/Lean/SatisfiesM.lean b/Batteries/Lean/SatisfiesM.lean
index b686913c27..189e138091 100644
--- a/Batteries/Lean/SatisfiesM.lean
+++ b/Batteries/Lean/SatisfiesM.lean
@@ -17,6 +17,8 @@ instance : MonadSatisfying (EIO ε) := inferInstanceAs <| MonadSatisfying (EStat
 instance : MonadSatisfying BaseIO := inferInstanceAs <| MonadSatisfying (EIO _)
 instance : MonadSatisfying IO := inferInstanceAs <| MonadSatisfying (EIO _)
 
+instance : MonadSatisfying (EST ε σ) := inferInstanceAs <| MonadSatisfying (EStateM _ _)
+
 instance : MonadSatisfying CoreM :=
   inferInstanceAs <| MonadSatisfying (ReaderT _ <| StateRefT' _ _ (EIO _))