[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Monad C
⊢ MonoidalCategory.tensorHom (μ M) (𝟙 M.toFunctor) ≫ μ M =
    (MonoidalCategory.associator M.toFunctor M.toFunctor M.toFunctor).hom ≫
      MonoidalCategory.tensorHom (𝟙 M.toFunctor) (μ M) ≫ μ M
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u
inst✝ : Category.{v, u} C
M : Monad C
x✝ : C
⊢ NatTrans.app (MonoidalCategory.tensorHom (μ M) (𝟙 M.toFunctor) ≫ μ M) x✝ =
    NatTrans.app
      ((MonoidalCategory.associator M.toFunctor M.toFunctor M.toFunctor).hom ≫
        MonoidalCategory.tensorHom (𝟙 M.toFunctor) (μ M) ≫ μ M)
      x✝
[PROOFSTEP]
simp [M.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ M.X.map (NatTrans.app M.mul X) ≫ NatTrans.app M.mul X = NatTrans.app M.mul (M.X.obj X) ≫ NatTrans.app M.mul X
[PROOFSTEP]
rw [← NatTrans.hcomp_id_app, ← NatTrans.comp_app]
  -- Porting note: had to add this step:
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ NatTrans.app ((M.mul ◫ 𝟙 M.X) ≫ M.mul) X = NatTrans.app M.mul (M.X.obj X) ≫ NatTrans.app M.mul X
[PROOFSTEP]
erw [M.mul_assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ NatTrans.app ((MonoidalCategory.associator M.X M.X M.X).hom ≫ MonoidalCategory.tensorHom (𝟙 M.X) M.mul ≫ M.mul) X =
    NatTrans.app M.mul (M.X.obj X) ≫ NatTrans.app M.mul X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ NatTrans.app M.one (M.X.obj X) ≫ NatTrans.app M.mul X = 𝟙 ((𝟭 C).obj (M.X.obj X))
[PROOFSTEP]
erw [← NatTrans.id_hcomp_app M.one, ← NatTrans.comp_app, M.mul_one]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ NatTrans.app (MonoidalCategory.rightUnitor M.X).hom X = 𝟙 ((𝟭 C).obj (M.X.obj X))
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ M.X.map (NatTrans.app M.one X) ≫ NatTrans.app M.mul X = 𝟙 (M.X.obj ((𝟭 C).obj X))
[PROOFSTEP]
erw [← NatTrans.hcomp_id_app M.one, ← NatTrans.comp_app, M.one_mul]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
M : Mon_ (C ⥤ C)
X : C
⊢ NatTrans.app (MonoidalCategory.leftUnitor M.X).hom X = 𝟙 (M.X.obj ((𝟭 C).obj X))
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Mon_ (C ⥤ C)
f : X ⟶ Y
src✝ : X.X ⟶ Y.X := f.hom
⊢ ∀ (X_1 : C), NatTrans.app (η (ofMon X)) X_1 ≫ NatTrans.app (NatTrans.mk src✝.app) X_1 = NatTrans.app (η (ofMon Y)) X_1
[PROOFSTEP]
intro X
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : Mon_ (C ⥤ C)
f : X✝ ⟶ Y
src✝ : X✝.X ⟶ Y.X := f.hom
X : C
⊢ NatTrans.app (η (ofMon X✝)) X ≫ NatTrans.app (NatTrans.mk src✝.app) X = NatTrans.app (η (ofMon Y)) X
[PROOFSTEP]
erw [← NatTrans.comp_app, f.one_hom]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : Mon_ (C ⥤ C)
f : X✝ ⟶ Y
src✝ : X✝.X ⟶ Y.X := f.hom
X : C
⊢ NatTrans.app Y.one X = NatTrans.app (η (ofMon Y)) X
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Mon_ (C ⥤ C)
f : X ⟶ Y
src✝ : X.X ⟶ Y.X := f.hom
⊢ ∀ (X_1 : C),
    NatTrans.app (μ (ofMon X)) X_1 ≫ NatTrans.app (NatTrans.mk src✝.app) X_1 =
      ((ofMon X).toFunctor.map (NatTrans.app (NatTrans.mk src✝.app) X_1) ≫
          NatTrans.app (NatTrans.mk src✝.app) ((ofMon Y).toFunctor.obj X_1)) ≫
        NatTrans.app (μ (ofMon Y)) X_1
[PROOFSTEP]
intro Z
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Mon_ (C ⥤ C)
f : X ⟶ Y
src✝ : X.X ⟶ Y.X := f.hom
Z : C
⊢ NatTrans.app (μ (ofMon X)) Z ≫ NatTrans.app (NatTrans.mk src✝.app) Z =
    ((ofMon X).toFunctor.map (NatTrans.app (NatTrans.mk src✝.app) Z) ≫
        NatTrans.app (NatTrans.mk src✝.app) ((ofMon Y).toFunctor.obj Z)) ≫
      NatTrans.app (μ (ofMon Y)) Z
[PROOFSTEP]
erw [← NatTrans.comp_app, f.mul_hom]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Mon_ (C ⥤ C)
f : X ⟶ Y
src✝ : X.X ⟶ Y.X := f.hom
Z : C
⊢ NatTrans.app (MonoidalCategory.tensorHom f.hom f.hom ≫ Y.mul) Z =
    ((ofMon X).toFunctor.map (NatTrans.app (NatTrans.mk src✝.app) Z) ≫
        NatTrans.app (NatTrans.mk src✝.app) ((ofMon Y).toFunctor.obj Z)) ≫
      NatTrans.app (μ (ofMon Y)) Z
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : Mon_ (C ⥤ C)
f : X ⟶ Y
src✝ : X.X ⟶ Y.X := f.hom
Z : C
⊢ (NatTrans.app f.hom (X.X.obj Z) ≫ Y.X.map (NatTrans.app f.hom Z)) ≫ NatTrans.app Y.mul Z =
    ((ofMon X).toFunctor.map (NatTrans.app f.hom Z) ≫ NatTrans.app f.hom (Y.X.obj Z)) ≫ NatTrans.app Y.mul Z
[PROOFSTEP]
simp only [NatTrans.naturality, NatTrans.hcomp_app, assoc, NatTrans.comp_app, ofMon_μ]
