feat: simp lemmas for LawfulApplicative

src/Init/Control/Lawful/Basic.lean

@@ -110,6 +110,19 @@ attribute [simp] map_pure seq_pure
 @[simp] theorem pure_id_seq [Applicative f] [LawfulApplicative f] (x : f α) : pure id <*> x = x := by
   simp [pure_seq]
 
+@[simp] theorem pure_seqRight [Applicative f] [LawfulApplicative f] (x : α) (y : f β) : pure x *> y = y := by
+  simp [seqRight_eq]
+
+@[simp] theorem seqLeft_pure [Applicative f] [LawfulApplicative f] (x : f α) (y : β) : x <* pure y = x := by
+  simp [seqLeft_eq]
+
+@[simp] theorem seqRight_pure_unit [Applicative f] [LawfulApplicative f] (x : f Unit) : x *> pure () = x := by
+  simp [seqRight_eq]
+
+@[simp] theorem pure_unit_seqLeft [Applicative f] [LawfulApplicative f] (x : f Unit) : pure () <* x = x := by
+  simp [seqLeft_eq, pure_seq, map_pure]
+  apply LawfulFunctor.id_map
+
 /--
 Lawful monads are those that satisfy a certain behavioral specification. While all instances of
 `Monad` should satisfy these laws, not all implementations are required to prove this.