mathlib3

9c6816ca - chore(category_theory/monad/basic): remove some simp lemmas (#18727)

chore(category_theory/monad/basic): remove some simp lemmas (#18727) This is a backport from mathlib4, where the simpNF (correctly) linter disapproves of these lemmas. Mostly this PR exists to verify that these are not needed in the simp set. https://github.com/leanprover-community/mathlib4/pull/2969 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>