diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean
index 2d7db8d758..c4d4d71d4d 100644
--- a/src/Init/Control/Lawful/Basic.lean
+++ b/src/Init/Control/Lawful/Basic.lean
@@ -133,6 +133,9 @@ theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y
   rw [← bind_pure_comp]
   simp only [bind_assoc, pure_bind]
 
+@[simp] theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by
+  simp [map]
+
 /--
 An alternative constructor for `LawfulMonad` which has more
 defaultable fields in the common case.
diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean
index c239c19ee2..8bc92c091f 100644
--- a/src/Init/Control/Lawful/Instances.lean
+++ b/src/Init/Control/Lawful/Instances.lean
@@ -84,6 +84,11 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
   pure_bind      := by intros; apply ext; simp [run_bind]
   bind_assoc     := by intros; apply ext; simp [run_bind]; apply bind_congr; intro a; cases a <;> simp
 
+@[simp] theorem map_throw [Monad m] [LawfulMonad m] {α β : Type _} (f : α → β) (e : ε) :
+    f <$> (throw e : ExceptT ε m α) = (throw e : ExceptT ε m β) := by
+  simp only [ExceptT.instMonad, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
+    pure_bind]
+
 end ExceptT
 
 /-! # Except -/