[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
X✝ Y✝ Z✝ : Monad C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
X Y : C
h : X ⟶ Y
⊢ X✝.map h ≫ (fun X => NatTrans.app f.toNatTrans X ≫ NatTrans.app g.toNatTrans X) Y =
    (fun X => NatTrans.app f.toNatTrans X ≫ NatTrans.app g.toNatTrans X) X ≫ Z✝.map h
[PROOFSTEP]
rw [assoc, f.1.naturality_assoc, g.1.naturality]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
X✝ Y✝ : Monad C
x✝ : X✝ ⟶ Y✝
⊢ (𝟙 X✝ ≫ x✝).app = x✝.app
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
X✝ Y✝ : Monad C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app (𝟙 X✝ ≫ x✝¹).toNatTrans x✝ = NatTrans.app x✝¹.toNatTrans x✝
[PROOFSTEP]
simp only [NatTrans.id_app, id_comp]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
X✝ Y✝ : Monad C
x✝ : X✝ ⟶ Y✝
⊢ (x✝ ≫ 𝟙 Y✝).app = x✝.app
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
X✝ Y✝ : Monad C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app (x✝¹ ≫ 𝟙 Y✝).toNatTrans x✝ = NatTrans.app x✝¹.toNatTrans x✝
[PROOFSTEP]
simp only [NatTrans.id_app, comp_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
W✝ X✝ Y✝ Z✝ : Monad C
x✝² : W✝ ⟶ X✝
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ((x✝² ≫ x✝¹) ≫ x✝).app = (x✝² ≫ x✝¹ ≫ x✝).app
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
W✝ X✝ Y✝ Z✝ : Monad C
x✝³ : W✝ ⟶ X✝
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : C
⊢ NatTrans.app ((x✝³ ≫ x✝²) ≫ x✝¹).toNatTrans x✝ = NatTrans.app (x✝³ ≫ x✝² ≫ x✝¹).toNatTrans x✝
[PROOFSTEP]
simp only [assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G X✝ Y✝ Z✝ : Comonad C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
X Y : C
h : X ⟶ Y
⊢ X✝.map h ≫ (fun X => NatTrans.app f.toNatTrans X ≫ NatTrans.app g.toNatTrans X) Y =
    (fun X => NatTrans.app f.toNatTrans X ≫ NatTrans.app g.toNatTrans X) X ≫ Z✝.map h
[PROOFSTEP]
rw [assoc, f.1.naturality_assoc, g.1.naturality]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G X✝ Y✝ : Comonad C
x✝ : X✝ ⟶ Y✝
⊢ (𝟙 X✝ ≫ x✝).app = x✝.app
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G X✝ Y✝ : Comonad C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app (𝟙 X✝ ≫ x✝¹).toNatTrans x✝ = NatTrans.app x✝¹.toNatTrans x✝
[PROOFSTEP]
simp only [NatTrans.id_app, id_comp]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G X✝ Y✝ : Comonad C
x✝ : X✝ ⟶ Y✝
⊢ (x✝ ≫ 𝟙 Y✝).app = x✝.app
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G X✝ Y✝ : Comonad C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app (x✝¹ ≫ 𝟙 Y✝).toNatTrans x✝ = NatTrans.app x✝¹.toNatTrans x✝
[PROOFSTEP]
simp only [NatTrans.id_app, comp_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G W✝ X✝ Y✝ Z✝ : Comonad C
x✝² : W✝ ⟶ X✝
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ((x✝² ≫ x✝¹) ≫ x✝).app = (x✝² ≫ x✝¹ ≫ x✝).app
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G W✝ X✝ Y✝ Z✝ : Comonad C
x✝³ : W✝ ⟶ X✝
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : C
⊢ NatTrans.app ((x✝³ ≫ x✝²) ≫ x✝¹).toNatTrans x✝ = NatTrans.app (x✝³ ≫ x✝² ≫ x✝¹).toNatTrans x✝
[PROOFSTEP]
simp only [assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : autoParam (∀ (X : C), NatTrans.app (Monad.η M) X ≫ NatTrans.app f.hom X = NatTrans.app (Monad.η N) X) _auto✝
f_μ :
  autoParam
    (∀ (X : C),
      NatTrans.app (Monad.μ M) X ≫ NatTrans.app f.hom X =
        (M.map (NatTrans.app f.hom X) ≫ NatTrans.app f.hom (N.obj X)) ≫ NatTrans.app (Monad.μ N) X)
    _auto✝
X : C
⊢ NatTrans.app (Monad.η N) X ≫ NatTrans.app f.inv X = NatTrans.app (Monad.η M) X
[PROOFSTEP]
simp [← f_η]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : autoParam (∀ (X : C), NatTrans.app (Monad.η M) X ≫ NatTrans.app f.hom X = NatTrans.app (Monad.η N) X) _auto✝
f_μ :
  autoParam
    (∀ (X : C),
      NatTrans.app (Monad.μ M) X ≫ NatTrans.app f.hom X =
        (M.map (NatTrans.app f.hom X) ≫ NatTrans.app f.hom (N.obj X)) ≫ NatTrans.app (Monad.μ N) X)
    _auto✝
X : C
⊢ NatTrans.app (Monad.μ N) X ≫ NatTrans.app f.inv X =
    (N.map (NatTrans.app f.inv X) ≫ NatTrans.app f.inv (M.obj X)) ≫ NatTrans.app (Monad.μ M) X
[PROOFSTEP]
rw [← NatIso.cancel_natIso_hom_right f]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : autoParam (∀ (X : C), NatTrans.app (Monad.η M) X ≫ NatTrans.app f.hom X = NatTrans.app (Monad.η N) X) _auto✝
f_μ :
  autoParam
    (∀ (X : C),
      NatTrans.app (Monad.μ M) X ≫ NatTrans.app f.hom X =
        (M.map (NatTrans.app f.hom X) ≫ NatTrans.app f.hom (N.obj X)) ≫ NatTrans.app (Monad.μ N) X)
    _auto✝
X : C
⊢ (NatTrans.app (Monad.μ N) X ≫ NatTrans.app f.inv X) ≫ NatTrans.app f.hom X =
    ((N.map (NatTrans.app f.inv X) ≫ NatTrans.app f.inv (M.obj X)) ≫ NatTrans.app (Monad.μ M) X) ≫ NatTrans.app f.hom X
[PROOFSTEP]
simp only [NatTrans.naturality, Iso.inv_hom_id_app, assoc, comp_id, f_μ, NatTrans.naturality_assoc,
  Iso.inv_hom_id_app_assoc, ← Functor.map_comp_assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : autoParam (∀ (X : C), NatTrans.app (Monad.η M) X ≫ NatTrans.app f.hom X = NatTrans.app (Monad.η N) X) _auto✝
f_μ :
  autoParam
    (∀ (X : C),
      NatTrans.app (Monad.μ M) X ≫ NatTrans.app f.hom X =
        (M.map (NatTrans.app f.hom X) ≫ NatTrans.app f.hom (N.obj X)) ≫ NatTrans.app (Monad.μ N) X)
    _auto✝
X : C
⊢ NatTrans.app (Monad.μ N) X = N.map (𝟙 (N.obj X)) ≫ NatTrans.app (Monad.μ N) X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : autoParam (∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X) _auto✝
f_δ :
  autoParam
    (∀ (X : C),
      NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
        NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X))
    _auto✝
X : C
⊢ NatTrans.app f.inv X ≫ NatTrans.app (Comonad.ε M) X = NatTrans.app (Comonad.ε N) X
[PROOFSTEP]
simp [← f_ε]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : autoParam (∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X) _auto✝
f_δ :
  autoParam
    (∀ (X : C),
      NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
        NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X))
    _auto✝
X : C
⊢ NatTrans.app f.inv X ≫ NatTrans.app (Comonad.δ M) X =
    NatTrans.app (Comonad.δ N) X ≫ NatTrans.app f.inv (N.obj X) ≫ M.map (NatTrans.app f.inv X)
[PROOFSTEP]
rw [← NatIso.cancel_natIso_hom_left f]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : autoParam (∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X) _auto✝
f_δ :
  autoParam
    (∀ (X : C),
      NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
        NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X))
    _auto✝
X : C
⊢ NatTrans.app f.hom X ≫ NatTrans.app f.inv X ≫ NatTrans.app (Comonad.δ M) X =
    NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X ≫ NatTrans.app f.inv (N.obj X) ≫ M.map (NatTrans.app f.inv X)
[PROOFSTEP]
simp only [reassoc_of% (f_δ X), Iso.hom_inv_id_app_assoc, NatTrans.naturality_assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : autoParam (∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X) _auto✝
f_δ :
  autoParam
    (∀ (X : C),
      NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
        NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X))
    _auto✝
X : C
⊢ NatTrans.app (Comonad.δ M) X =
    NatTrans.app (Comonad.δ M) X ≫ M.map (NatTrans.app f.hom X) ≫ M.map (NatTrans.app f.inv X)
[PROOFSTEP]
rw [← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : autoParam (∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X) _auto✝
f_δ :
  autoParam
    (∀ (X : C),
      NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
        NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X))
    _auto✝
X : C
⊢ NatTrans.app (Comonad.δ M) X = NatTrans.app (Comonad.δ M) X ≫ 𝟙 (M.obj (M.obj X))
[PROOFSTEP]
apply (comp_id _).symm
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), NatTrans.app (Monad.η M) X ≫ NatTrans.app f.hom X = NatTrans.app (Monad.η N) X
f_μ :
  ∀ (X : C),
    NatTrans.app (Monad.μ M) X ≫ NatTrans.app f.hom X =
      (M.map (NatTrans.app f.hom X) ≫ NatTrans.app f.hom (N.obj X)) ≫ NatTrans.app (Monad.μ N) X
⊢ (monadToFunctor C).mapIso (MonadIso.mk f) = f
[PROOFSTEP]
ext
[GOAL]
case w.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), NatTrans.app (Monad.η M) X ≫ NatTrans.app f.hom X = NatTrans.app (Monad.η N) X
f_μ :
  ∀ (X : C),
    NatTrans.app (Monad.μ M) X ≫ NatTrans.app f.hom X =
      (M.map (NatTrans.app f.hom X) ≫ NatTrans.app f.hom (N.obj X)) ≫ NatTrans.app (Monad.μ N) X
x✝ : C
⊢ NatTrans.app ((monadToFunctor C).mapIso (MonadIso.mk f)).hom x✝ = NatTrans.app f.hom x✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X
f_δ :
  ∀ (X : C),
    NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
      NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X)
⊢ (comonadToFunctor C).mapIso (ComonadIso.mk f) = f
[PROOFSTEP]
ext
[GOAL]
case w.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), NatTrans.app f.hom X ≫ NatTrans.app (Comonad.ε N) X = NatTrans.app (Comonad.ε M) X
f_δ :
  ∀ (X : C),
    NatTrans.app f.hom X ≫ NatTrans.app (Comonad.δ N) X =
      NatTrans.app (Comonad.δ M) X ≫ NatTrans.app f.hom (M.obj X) ≫ N.map (NatTrans.app f.hom X)
x✝ : C
⊢ NatTrans.app ((comonadToFunctor C).mapIso (ComonadIso.mk f)).hom x✝ = NatTrans.app f.hom x✝
[PROOFSTEP]
rfl
