From d8fcfead97932432a46e9ca7ac86572de0c65ebd Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Tue, 28 Jan 2025 12:59:55 +1100
Subject: [PATCH] feat: add `LawfulMonad` helper simp lemmas (#6805)

This PR adds to helper lemmas in the `LawfulMonad` namespace, which
sometimes fire via `simp` when the original versions taking
`LawfulApplicative` or `Functor` do not fire.
---
 src/Init/Control/Lawful/Basic.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean
index b457183645..f62b57eb96 100644
--- a/src/Init/Control/Lawful/Basic.lean
+++ b/src/Init/Control/Lawful/Basic.lean
@@ -136,6 +136,23 @@ theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y
 theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by
   simp [map]
 
+/--
+This is just a duplicate of `LawfulApplicative.map_pure`,
+but sometimes applies when that doesn't.
+
+It is named with a prime to avoid conflict with the inherited field `LawfulMonad.map_pure`.
+-/
+@[simp] theorem LawfulMonad.map_pure' [Monad m] [LawfulMonad m] {a : α} :
+    (f <$> pure a : m β) = pure (f a) := by
+  simp only [map_pure]
+
+/--
+This is just a duplicate of `Functor.map_map`, but sometimes applies when that doesn't.
+-/
+@[simp] theorem LawfulMonad.map_map {m} [Monad m] [LawfulMonad m] {x : m α} :
+    g <$> f <$> x = (fun a => g (f a)) <$> x := by
+  simp only [Functor.map_map]
+
 /--
 An alternative constructor for `LawfulMonad` which has more
 defaultable fields in the common case.