diff --git a/Std/Classes/LawfulMonad.lean b/Std/Classes/LawfulMonad.lean
index c40a817581..ca1a603e24 100644
--- a/Std/Classes/LawfulMonad.lean
+++ b/Std/Classes/LawfulMonad.lean
@@ -52,6 +52,20 @@ instance : LawfulMonad Option := LawfulMonad.mk'
 instance : LawfulApplicative Option := inferInstance
 instance : LawfulFunctor Option := inferInstance
 
+instance : LawfulMonad (EStateM ε σ) := .mk'
+  (id_map := fun x => funext <| fun s => by
+    dsimp only [EStateM.instMonadEStateM, EStateM.map]
+    match x s with
+    | .ok _ _ => rfl
+    | .error _ _ => rfl)
+  (pure_bind := fun _ _ => rfl)
+  (bind_assoc := fun x _ _ => funext <| fun s => by
+    dsimp only [EStateM.instMonadEStateM, EStateM.bind]
+    match x s with
+    | .ok _ _ => rfl
+    | .error _ _ => rfl)
+  (map_const := fun _ _ => rfl)
+
 /-!
 ## SatisfiesM