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

@@ -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.