diff --git a/Mathlib.lean b/Mathlib.lean
index 1b6a334980933..27b1d9c134998 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -995,6 +995,7 @@ import Mathlib.CategoryTheory.Monad.Adjunction
 import Mathlib.CategoryTheory.Monad.Algebra
 import Mathlib.CategoryTheory.Monad.Basic
 import Mathlib.CategoryTheory.Monad.Coequalizer
+import Mathlib.CategoryTheory.Monad.EquivMon
 import Mathlib.CategoryTheory.Monad.Kleisli
 import Mathlib.CategoryTheory.Monad.Limits
 import Mathlib.CategoryTheory.Monad.Products
diff --git a/Mathlib/CategoryTheory/Monad/Basic.lean b/Mathlib/CategoryTheory/Monad/Basic.lean
index ab82e50c7d8ce..c4a5b373997b0 100644
--- a/Mathlib/CategoryTheory/Monad/Basic.lean
+++ b/Mathlib/CategoryTheory/Monad/Basic.lean
@@ -135,10 +135,13 @@ def Comonad.Simps.δ : (G : C ⥤ C) ⟶ (G : C ⥤ C) ⋙ (G : C ⥤ C) :=
   G.δ
 #align category_theory.comonad.simps.δ CategoryTheory.Comonad.Simps.δ
 
-initialize_simps_projections CategoryTheory.Monad (toFunctor → coe, η' → η, μ' → μ)
+initialize_simps_projections CategoryTheory.Monad
+  (obj → obj, map → map, toFunctor → coe, η' → η, μ' → μ)
 
-initialize_simps_projections CategoryTheory.Comonad (toFunctor → coe, ε' → ε, δ' → δ)
+initialize_simps_projections CategoryTheory.Comonad
+  (obj → obj, map → map, toFunctor → coe, ε' → ε, δ' → δ)
 
+-- Porting note: investigate whether this can be a `simp` lemma?
 @[reassoc]
 theorem Monad.assoc (T : Monad C) (X : C) :
     (T : C ⥤ C).map (T.μ.app X) ≫ T.μ.app _ = T.μ.app _ ≫ T.μ.app _ :=
@@ -179,7 +182,7 @@ theorem Comonad.right_counit (G : Comonad C) (X : C) :
 @[ext]
 structure MonadHom (T₁ T₂ : Monad C) extends NatTrans (T₁ : C ⥤ C) T₂ where
   app_η : ∀ X, T₁.η.app X ≫ app X = T₂.η.app X := by aesop_cat
-  app_μ : ∀ X, T₁.μ.app X ≫ app X = ((T₁ : C ⥤ C).map (app X) ≫ app _) ≫ T₂.μ.app X := by
+  app_μ : ∀ X, T₁.μ.app X ≫ app X = (T₁.map (app X) ≫ app _) ≫ T₂.μ.app X := by
     aesop_cat
 #align category_theory.monad_hom CategoryTheory.MonadHom
 
@@ -189,7 +192,7 @@ initialize_simps_projections MonadHom (+toNatTrans, -app)
 @[ext]
 structure ComonadHom (M N : Comonad C) extends NatTrans (M : C ⥤ C) N where
   app_ε : ∀ X, app X ≫ N.ε.app X = M.ε.app X := by aesop_cat
-  app_δ : ∀ X, app X ≫ N.δ.app X = M.δ.app X ≫ app _ ≫ (N : C ⥤ C).map (app X) := by aesop_cat
+  app_δ : ∀ X, app X ≫ N.δ.app X = M.δ.app X ≫ app _ ≫ N.map (app X) := by aesop_cat
 #align category_theory.comonad_hom CategoryTheory.ComonadHom
 
 initialize_simps_projections ComonadHom (+toNatTrans, -app)
diff --git a/Mathlib/CategoryTheory/Monad/EquivMon.lean b/Mathlib/CategoryTheory/Monad/EquivMon.lean
new file mode 100644
index 0000000000000..f870f788a24d0
--- /dev/null
+++ b/Mathlib/CategoryTheory/Monad/EquivMon.lean
@@ -0,0 +1,127 @@
+/-
+Copyright (c) 2020 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Topaz
+
+! This file was ported from Lean 3 source module category_theory.monad.equiv_mon
+! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Monad.Basic
+import Mathlib.CategoryTheory.Monoidal.End
+import Mathlib.CategoryTheory.Monoidal.Mon_
+
+/-!
+
+# The equivalence between `Monad C` and `Mon_ (C ⥤ C)`.
+
+A monad "is just" a monoid in the category of endofunctors.
+
+# Definitions/Theorems
+
+1. `toMon` associates a monoid object in `C ⥤ C` to any monad on `C`.
+2. `monadToMon` is the functorial version of `toMon`.
+3. `ofMon` associates a monad on `C` to any monoid object in `C ⥤ C`.
+4. `monadMonEquiv` is the equivalence between `Monad C` and `Mon_ (C ⥤ C)`.
+
+-/
+
+set_option linter.uppercaseLean3 false
+
+namespace CategoryTheory
+
+open Category
+
+universe v u -- morphism levels before object levels. See note [category_theory universes].
+
+variable {C : Type u} [Category.{v} C]
+
+namespace Monad
+
+attribute [local instance] endofunctorMonoidalCategory
+
+/-- To every `Monad C` we associated a monoid object in `C ⥤ C`.-/
+@[simps]
+def toMon (M : Monad C) : Mon_ (C ⥤ C) where
+  X := (M : C ⥤ C)
+  one := M.η
+  mul := M.μ
+  mul_assoc := by ext; simp [M.assoc]
+#align category_theory.Monad.to_Mon CategoryTheory.Monad.toMon
+
+variable (C)
+
+/-- Passing from `Monad C` to `Mon_ (C ⥤ C)` is functorial. -/
+@[simps]
+def monadToMon : Monad C ⥤ Mon_ (C ⥤ C) where
+  obj := toMon
+  map f := { hom := f.toNatTrans }
+#align category_theory.Monad.Monad_to_Mon CategoryTheory.Monad.monadToMon
+
+variable {C}
+
+/-- To every monoid object in `C ⥤ C` we associate a `Monad C`. -/
+@[simps η μ]
+def ofMon (M : Mon_ (C ⥤ C)) : Monad C where
+  toFunctor := M.X
+  η' := M.one
+  μ' := M.mul
+  left_unit' := fun X => by
+    -- Porting note: now using `erw`
+    erw [← NatTrans.id_hcomp_app M.one, ← NatTrans.comp_app, M.mul_one]
+    rfl
+  right_unit' := fun X => by
+    -- Porting note: now using `erw`
+    erw [← NatTrans.hcomp_id_app M.one, ← NatTrans.comp_app, M.one_mul]
+    rfl
+  assoc' := fun X => by
+    rw [← NatTrans.hcomp_id_app, ← NatTrans.comp_app]
+    -- Porting note: had to add this step:
+    erw [M.mul_assoc]
+    simp
+#align category_theory.Monad.of_Mon CategoryTheory.Monad.ofMon
+
+-- Porting note: `@[simps]` fails to generate `ofMon_obj`:
+@[simp] lemma ofMon_obj (M : Mon_ (C ⥤ C)) (X : C) : (ofMon M).obj X = M.X.obj X := rfl
+
+variable (C)
+
+/-- Passing from `Mon_ (C ⥤ C)` to `Monad C` is functorial. -/
+@[simps]
+def monToMonad : Mon_ (C ⥤ C) ⥤ Monad C where
+  obj := ofMon
+  map {X Y} f :=
+    { f.hom with
+      app_η := by
+        intro X
+        erw [← NatTrans.comp_app, f.one_hom]
+        rfl
+      app_μ := by
+        intro Z
+        erw [← NatTrans.comp_app, f.mul_hom]
+        dsimp
+        simp only [NatTrans.naturality, NatTrans.hcomp_app, assoc, NatTrans.comp_app,
+          ofMon_μ] }
+#align category_theory.Monad.Mon_to_Monad CategoryTheory.Monad.monToMonad
+
+/-- Oh, monads are just monoids in the category of endofunctors (equivalence of categories). -/
+@[simps]
+def monadMonEquiv : Monad C ≌ Mon_ (C ⥤ C) where
+  functor := monadToMon _
+  inverse := monToMonad _
+  unitIso :=
+  { hom := { app := fun _ => { app := fun _ => 𝟙 _ } }
+    inv := { app := fun _ => { app := fun _ => 𝟙 _ } } }
+  counitIso :=
+  { hom := { app := fun _ => { hom := 𝟙 _ } }
+    inv := { app := fun _ => { hom := 𝟙 _ } } }
+#align category_theory.Monad.Monad_Mon_equiv CategoryTheory.Monad.monadMonEquiv
+
+-- Sanity check
+example (A : Monad C) {X : C} : ((monadMonEquiv C).unitIso.app A).hom.app X = 𝟙 _ :=
+  rfl
+
+end Monad
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/End.lean b/Mathlib/CategoryTheory/Monoidal/End.lean
index 8d09ba5be4f3c..3f358f88a03db 100644
--- a/Mathlib/CategoryTheory/Monoidal/End.lean
+++ b/Mathlib/CategoryTheory/Monoidal/End.lean
@@ -46,6 +46,40 @@ open CategoryTheory.MonoidalCategory
 
 attribute [local instance] endofunctorMonoidalCategory
 
+@[simp] theorem endofunctorMonoidalCategory_tensorUnit_obj (X : C) :
+    (𝟙_ (C ⥤ C)).obj X = X := rfl
+
+@[simp] theorem endofunctorMonoidalCategory_tensorUnit_map {X Y : C} (f : X ⟶ Y) :
+    (𝟙_ (C ⥤ C)).map f = f := rfl
+
+@[simp] theorem endofunctorMonoidalCategory_tensorObj_obj (F G : C ⥤ C) (X : C) :
+    (F ⊗ G).obj X = G.obj (F.obj X) := rfl
+
+@[simp] theorem endofunctorMonoidalCategory_tensorObj_map (F G : C ⥤ C) {X Y : C} (f : X ⟶ Y) :
+    (F ⊗ G).map f = G.map (F.map f) := rfl
+
+@[simp] theorem endofunctorMonoidalCategory_tensorMap_app
+    {F G H K : C ⥤ C} {α : F ⟶ G} {β : H ⟶ K} (X : C) :
+    (α ⊗ β).app X = β.app (F.obj X) ≫ K.map (α.app X) := rfl
+
+@[simp] theorem endofunctorMonoidalCategory_associator_hom_app (F G H : C ⥤ C) (X : C) :
+  (α_ F G H).hom.app X = 𝟙 _ := rfl
+
+@[simp] theorem endofunctorMonoidalCategory_associator_inv_app (F G H : C ⥤ C) (X : C) :
+  (α_ F G H).inv.app X = 𝟙 _ := rfl
+
+@[simp] theorem endofunctorMonoidalCategory_leftUnitor_hom_app (F : C ⥤ C) (X : C) :
+  (λ_ F).hom.app X = 𝟙 _ := rfl
+
+@[simp] theorem endofunctorMonoidalCategory_leftUnitor_inv_app (F : C ⥤ C) (X : C) :
+  (λ_ F).inv.app X = 𝟙 _ := rfl
+
+@[simp] theorem endofunctorMonoidalCategory_rightUnitor_hom_app (F : C ⥤ C) (X : C) :
+  (ρ_ F).hom.app X = 𝟙 _ := rfl
+
+@[simp] theorem endofunctorMonoidalCategory_rightUnitor_inv_app (F : C ⥤ C) (X : C) :
+  (ρ_ F).inv.app X = 𝟙 _ := rfl
+
 -- porting note: used `dsimp [endofunctorMonoidalCategory]` when necessary instead
 -- attribute [local reducible] endofunctorMonoidalCategory
 
@@ -53,41 +87,25 @@ attribute [local instance] endofunctorMonoidalCategory
 -/
 @[simps!]
 def tensoringRightMonoidal [MonoidalCategory.{v} C] : MonoidalFunctor C (C ⥤ C) :=
-  {-- We could avoid needing to do this explicitly by
-      -- constructing a partially applied analogue of `associatorNatIso`.
-      tensoringRight C with
+  { tensoringRight C with
     ε := (rightUnitorNatIso C).inv
-    μ := fun X Y =>
-      { app := fun Z => (α_ Z X Y).hom
-        naturality := fun Z Z' f => by
-          dsimp [endofunctorMonoidalCategory]
-          rw [associator_naturality]
-          simp }
+    μ := fun X Y => { app := fun Z => (α_ Z X Y).hom  }
     μ_natural := fun f g => by
       ext Z
-      dsimp [endofunctorMonoidalCategory]
+      dsimp
       simp only [← id_tensor_comp_tensor_id g f, id_tensor_comp, ← tensor_id, Category.assoc,
         associator_naturality, associator_naturality_assoc]
     associativity := fun X Y Z => by
       ext W
-      dsimp [endofunctorMonoidalCategory]
       simp [pentagon]
-    left_unitality := fun X => by
-      ext Y
-      dsimp [endofunctorMonoidalCategory]
-      rw [Category.id_comp, triangle, ← tensor_comp]
-      aesop_cat
-    right_unitality := fun X => by
-      ext Y; dsimp [endofunctorMonoidalCategory]
-      rw [tensor_id, Category.comp_id, rightUnitor_tensor_inv, Category.assoc,
-        Iso.inv_hom_id_assoc, ← id_tensor_comp, Iso.inv_hom_id, tensor_id]
-    ε_isIso := by infer_instance
     μ_isIso := fun X Y =>
-      ⟨⟨{   app := fun Z => (α_ Z X Y).inv
-            naturality := fun Z Z' f => by
-              dsimp [endofunctorMonoidalCategory]
-              rw [← associator_inv_naturality]
-              simp },
+      -- We could avoid needing to do this explicitly by
+      -- constructing a partially applied analogue of `associatorNatIso`.
+      ⟨⟨{ app := fun Z => (α_ Z X Y).inv
+          naturality := fun Z Z' f => by
+            dsimp
+            rw [← associator_inv_naturality]
+            simp },
           by aesop_cat⟩⟩ }
 #align category_theory.tensoring_right_monoidal CategoryTheory.tensoringRightMonoidal
 
@@ -146,7 +164,7 @@ theorem μ_naturality₂ {m n m' n' : M} (f : m ⟶ m') (g : n ⟶ n') (X : C) :
     (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (F.μ m' n').app X =
       (F.μ m n).app X ≫ (F.map (f ⊗ g)).app X := by
   have := congr_app (F.toLaxMonoidalFunctor.μ_natural f g) X
-  dsimp [endofunctorMonoidalCategory] at this
+  dsimp at this
   simpa using this
 #align category_theory.μ_naturality₂ CategoryTheory.μ_naturality₂
 
@@ -186,7 +204,7 @@ theorem μ_inv_naturalityᵣ {m n n' : M} (g : n ⟶ n') (X : C) :
 theorem left_unitality_app (n : M) (X : C) :
     (F.obj n).map (F.ε.app X) ≫ (F.μ (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X = 𝟙 _ := by
   have := congr_app (F.toLaxMonoidalFunctor.left_unitality n) X
-  dsimp [endofunctorMonoidalCategory] at this
+  dsimp at this
   simpa using this.symm
 #align category_theory.left_unitality_app CategoryTheory.left_unitality_app
 
@@ -207,14 +225,13 @@ theorem obj_ε_inv_app (n : M) (X : C) :
     (F.obj n).map (F.εIso.inv.app X) = (F.μ (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X := by
   rw [← cancel_mono ((F.obj n).map (F.ε.app X)), ← Functor.map_comp]
   simp
-  rfl
 #align category_theory.obj_ε_inv_app CategoryTheory.obj_ε_inv_app
 
 @[reassoc]
 theorem right_unitality_app (n : M) (X : C) :
     F.ε.app ((F.obj n).obj X) ≫ (F.μ n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X = 𝟙 _ := by
   have := congr_app (F.toLaxMonoidalFunctor.right_unitality n) X
-  dsimp [endofunctorMonoidalCategory] at this
+  dsimp at this
   simpa using this.symm
 #align category_theory.right_unitality_app CategoryTheory.right_unitality_app
 
@@ -232,7 +249,6 @@ theorem ε_inv_app_obj (n : M) (X : C) :
     F.εIso.inv.app ((F.obj n).obj X) = (F.μ n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X := by
   rw [← cancel_mono (F.ε.app ((F.obj n).obj X)), ε_inv_hom_app]
   simp
-  rfl
 #align category_theory.ε_inv_app_obj CategoryTheory.ε_inv_app_obj
 
 @[reassoc]
@@ -241,7 +257,7 @@ theorem associativity_app (m₁ m₂ m₃ : M) (X : C) :
         (F.μ (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
       (F.μ m₂ m₃).app ((F.obj m₁).obj X) ≫ (F.μ m₁ (m₂ ⊗ m₃)).app X := by
   have := congr_app (F.toLaxMonoidalFunctor.associativity m₁ m₂ m₃) X
-  dsimp [endofunctorMonoidalCategory] at this
+  dsimp at this
   simpa using this
 #align category_theory.associativity_app CategoryTheory.associativity_app
 
@@ -253,9 +269,6 @@ theorem obj_μ_app (m₁ m₂ m₃ : M) (X : C) :
         (F.μ m₁ (m₂ ⊗ m₃)).app X ≫
           (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (F.μIso (m₁ ⊗ m₂) m₃).inv.app X := by
   rw [← associativity_app_assoc]
-  dsimp [endofunctorMonoidalCategory]
-  simp
-  dsimp [endofunctorMonoidalCategory]
   simp
 #align category_theory.obj_μ_app CategoryTheory.obj_μ_app
 
@@ -277,7 +290,6 @@ theorem obj_μ_inv_app (m₁ m₂ m₃ : M) (X : C) :
       simp
     · refine' IsIso.inv_eq_of_hom_inv_id _
       simp
-      rfl
 #align category_theory.obj_μ_inv_app CategoryTheory.obj_μ_inv_app
 
 @[reassoc (attr := simp)]
diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/Mathlib/CategoryTheory/Shift/Basic.lean
index d5eafe8c54025..04dff1ba62032 100644
--- a/Mathlib/CategoryTheory/Shift/Basic.lean
+++ b/Mathlib/CategoryTheory/Shift/Basic.lean
@@ -144,12 +144,10 @@ def hasShiftMk (h : ShiftMkCore C A) : HasShift C A :=
         rintro ⟨n⟩
         ext X
         simp [endofunctorMonoidalCategory, h.zero_add_inv_app, ← Functor.map_comp]
-        rfl
       right_unitality := by
         rintro ⟨n⟩
         ext X
-        simp [endofunctorMonoidalCategory, h.add_zero_inv_app]
-        rfl }⟩
+        simp [endofunctorMonoidalCategory, h.add_zero_inv_app]}⟩
 #align category_theory.has_shift_mk CategoryTheory.hasShiftMk
 
 end