[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f
[PROOFSTEP]
dsimp
  -- Porting note: unfold comp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X ⟶ Y
⊢ NatTrans.app (Monad.η T) X ≫ T.map f ≫ NatTrans.app (Monad.μ T) Y = f
[PROOFSTEP]
rw [← T.η.naturality_assoc f, T.left_unit]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : Kleisli T
f : X ⟶ Y
⊢ (𝟭 C).map f ≫ 𝟙 (T.obj Y) = f
[PROOFSTEP]
apply Category.comp_id
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
W✝ X✝ Y✝ Z✝ : Kleisli T
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
simp only [Functor.map_comp, Category.assoc, Monad.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
W✝ X✝ Y✝ Z✝ : Kleisli T
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ f ≫ T.map g ≫ NatTrans.app (Monad.μ T) Y✝ ≫ T.map h ≫ NatTrans.app (Monad.μ T) Z✝ =
    f ≫ T.map g ≫ T.map (T.map h) ≫ NatTrans.app (Monad.μ T) (T.obj Z✝) ≫ NatTrans.app (Monad.μ T) Z✝
[PROOFSTEP]
erw [T.μ.naturality_assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ { obj := fun X => X, map := fun {X Y} f => f ≫ NatTrans.app (Monad.η T) Y }.map (f ≫ g) =
    { obj := fun X => X, map := fun {X Y} f => f ≫ NatTrans.app (Monad.η T) Y }.map f ≫
      { obj := fun X => X, map := fun {X Y} f => f ≫ NatTrans.app (Monad.η T) Y }.map g
[PROOFSTEP]
change _ = (f ≫ (Monad.η T).app Y) ≫ T.map (g ≫ (Monad.η T).app Z) ≫ T.μ.app Z
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ { obj := fun X => X, map := fun {X Y} f => f ≫ NatTrans.app (Monad.η T) Y }.map (f ≫ g) =
    (f ≫ NatTrans.app (Monad.η T) Y) ≫ T.map (g ≫ NatTrans.app (Monad.η T) Z) ≫ NatTrans.app (Monad.μ T) Z
[PROOFSTEP]
simp [← T.η.naturality g]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ Z
⊢ { obj := fun X => T.obj X, map := fun {x Y} f => T.map f ≫ NatTrans.app (Monad.μ T) Y }.map (f ≫ g) =
    { obj := fun X => T.obj X, map := fun {x Y} f => T.map f ≫ NatTrans.app (Monad.μ T) Y }.map f ≫
      { obj := fun X => T.obj X, map := fun {x Y} f => T.map f ≫ NatTrans.app (Monad.μ T) Y }.map g
[PROOFSTEP]
change T.map (f ≫ T.map g ≫ T.μ.app Z) ≫ T.μ.app Z = _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ Z
⊢ T.map (f ≫ T.map g ≫ NatTrans.app (Monad.μ T) Z) ≫ NatTrans.app (Monad.μ T) Z =
    { obj := fun X => T.obj X, map := fun {x Y} f => T.map f ≫ NatTrans.app (Monad.μ T) Y }.map f ≫
      { obj := fun X => T.obj X, map := fun {x Y} f => T.map f ≫ NatTrans.app (Monad.μ T) Y }.map g
[PROOFSTEP]
simp only [Functor.map_comp, Category.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ Z
⊢ T.map f ≫ T.map (T.map g) ≫ T.map (NatTrans.app (Monad.μ T) Z) ≫ NatTrans.app (Monad.μ T) Z =
    T.map f ≫ NatTrans.app (Monad.μ T) Y ≫ T.map g ≫ NatTrans.app (Monad.μ T) Z
[PROOFSTEP]
erw [← T.μ.naturality_assoc g, T.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ Z
⊢ T.map f ≫ T.map (T.map g) ≫ NatTrans.app (Monad.μ T) (T.obj Z) ≫ NatTrans.app (Monad.μ T) Z =
    T.map f ≫ (T.toFunctor ⋙ T.toFunctor).map g ≫ NatTrans.app (Monad.μ T) (T.obj Z) ≫ NatTrans.app (Monad.μ T) Z
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : C
Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ (fromKleisli T).obj Z
⊢ ↑((fun X Y => Equiv.refl (X ⟶ T.obj Y)) X Z).symm (f ≫ g) =
    (toKleisli T).map f ≫ ↑((fun X Y => Equiv.refl (X ⟶ T.obj Y)) Y Z).symm g
[PROOFSTEP]
change f ≫ g = (f ≫ T.η.app Y) ≫ T.map g ≫ T.μ.app Z
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : C
Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ (fromKleisli T).obj Z
⊢ f ≫ g = (f ≫ NatTrans.app (Monad.η T) Y) ≫ T.map g ≫ NatTrans.app (Monad.μ T) Z
[PROOFSTEP]
rw [Category.assoc, ← T.η.naturality_assoc g, Functor.id_map]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : C
Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ (fromKleisli T).obj Z
⊢ f ≫ g = f ≫ g ≫ NatTrans.app (Monad.η T) ((fromKleisli T).obj Z) ≫ NatTrans.app (Monad.μ T) Z
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
T : Monad C
X Y : C
Z : Kleisli T
f : X ⟶ Y
g : Y ⟶ (fromKleisli T).obj Z
⊢ f ≫ g = f ≫ g ≫ NatTrans.app (Monad.η T) (T.obj Z) ≫ NatTrans.app (Monad.μ T) Z
[PROOFSTEP]
simp [Monad.left_unit]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X✝ Y✝ : Cokleisli U
f : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f = f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X✝ Y✝ : Cokleisli U
f : X✝ ⟶ Y✝
⊢ NatTrans.app (Comonad.δ U) X✝ ≫ U.map (NatTrans.app (Comonad.ε U) X✝) ≫ f = f
[PROOFSTEP]
rw [U.right_counit_assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X Y Z W : Cokleisli U
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
change
  U.δ.app X ≫ U.map (U.δ.app X ≫ U.map f ≫ g) ≫ h =
    U.δ.app X ≫
      U.map f ≫
        (U.δ.app Y ≫ U.map g ≫ h)
          -- Porting note: something was broken here and was easier just to redo from scratch
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X Y Z W : Cokleisli U
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
⊢ NatTrans.app (Comonad.δ U) X ≫ U.map (NatTrans.app (Comonad.δ U) X ≫ U.map f ≫ g) ≫ h =
    NatTrans.app (Comonad.δ U) X ≫ U.map f ≫ NatTrans.app (Comonad.δ U) Y ≫ U.map g ≫ h
[PROOFSTEP]
simp only [Functor.map_comp, ← Category.assoc, eq_whisker]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X Y Z W : Cokleisli U
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
⊢ (((NatTrans.app (Comonad.δ U) X ≫ U.map (NatTrans.app (Comonad.δ U) X)) ≫ U.map (U.map f)) ≫ U.map g) ≫ h =
    (((NatTrans.app (Comonad.δ U) X ≫ U.map f) ≫ NatTrans.app (Comonad.δ U) Y) ≫ U.map g) ≫ h
[PROOFSTEP]
simp only [Category.assoc, U.δ.naturality, Functor.comp_map, U.coassoc_assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X Y x✝ : C
f : X ⟶ Y
g : Y ⟶ x✝
⊢ { obj := fun X => X, map := fun {X x} f => NatTrans.app (Comonad.ε U) X ≫ f }.map (f ≫ g) =
    { obj := fun X => X, map := fun {X x} f => NatTrans.app (Comonad.ε U) X ≫ f }.map f ≫
      { obj := fun X => X, map := fun {X x} f => NatTrans.app (Comonad.ε U) X ≫ f }.map g
[PROOFSTEP]
change U.ε.app X ≫ f ≫ g = U.δ.app X ≫ U.map (U.ε.app X ≫ f) ≫ U.ε.app Y ≫ g
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X Y x✝ : C
f : X ⟶ Y
g : Y ⟶ x✝
⊢ NatTrans.app (Comonad.ε U) X ≫ f ≫ g =
    NatTrans.app (Comonad.δ U) X ≫ U.map (NatTrans.app (Comonad.ε U) X ≫ f) ≫ NatTrans.app (Comonad.ε U) Y ≫ g
[PROOFSTEP]
simp [← U.ε.naturality g]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X Y x✝ : Cokleisli U
f : X ⟶ Y
g : Y ⟶ x✝
⊢ { obj := fun X => U.obj X, map := fun {X x} f => NatTrans.app (Comonad.δ U) X ≫ U.map f }.map (f ≫ g) =
    { obj := fun X => U.obj X, map := fun {X x} f => NatTrans.app (Comonad.δ U) X ≫ U.map f }.map f ≫
      { obj := fun X => U.obj X, map := fun {X x} f => NatTrans.app (Comonad.δ U) X ≫ U.map f }.map g
[PROOFSTEP]
change U.δ.app X ≫ U.map (U.δ.app X ≫ U.map f ≫ g) = (U.δ.app X ≫ U.map f) ≫ (U.δ.app Y ≫ U.map g)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X Y x✝ : Cokleisli U
f : X ⟶ Y
g : Y ⟶ x✝
⊢ NatTrans.app (Comonad.δ U) X ≫ U.map (NatTrans.app (Comonad.δ U) X ≫ U.map f ≫ g) =
    (NatTrans.app (Comonad.δ U) X ≫ U.map f) ≫ NatTrans.app (Comonad.δ U) Y ≫ U.map g
[PROOFSTEP]
simp only [Functor.map_comp, ← Category.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X Y x✝ : Cokleisli U
f : X ⟶ Y
g : Y ⟶ x✝
⊢ ((NatTrans.app (Comonad.δ U) X ≫ U.map (NatTrans.app (Comonad.δ U) X)) ≫ U.map (U.map f)) ≫ U.map g =
    ((NatTrans.app (Comonad.δ U) X ≫ U.map f) ≫ NatTrans.app (Comonad.δ U) Y) ≫ U.map g
[PROOFSTEP]
rw [Comonad.coassoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X Y x✝ : Cokleisli U
f : X ⟶ Y
g : Y ⟶ x✝
⊢ ((NatTrans.app (Comonad.δ U) X ≫ NatTrans.app (Comonad.δ U) (U.obj X)) ≫ U.map (U.map f)) ≫ U.map g =
    ((NatTrans.app (Comonad.δ U) X ≫ U.map f) ≫ NatTrans.app (Comonad.δ U) Y) ≫ U.map g
[PROOFSTEP]
simp only [Category.assoc, NatTrans.naturality, Functor.comp_map]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X : Cokleisli U
Y x✝ : C
f : (fromCokleisli U).obj X ⟶ Y
g : Y ⟶ x✝
⊢ ↑((fun X Y => Equiv.refl (U.obj X ⟶ Y)) X x✝) (f ≫ g) =
    ↑((fun X Y => Equiv.refl (U.obj X ⟶ Y)) X Y) f ≫ (toCokleisli U).map g
[PROOFSTEP]
change f ≫ g = U.δ.app X ≫ U.map f ≫ U.ε.app Y ≫ g
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X : Cokleisli U
Y x✝ : C
f : (fromCokleisli U).obj X ⟶ Y
g : Y ⟶ x✝
⊢ f ≫ g = NatTrans.app (Comonad.δ U) X ≫ U.map f ≫ NatTrans.app (Comonad.ε U) Y ≫ g
[PROOFSTEP]
erw [← Category.assoc (U.map f), U.ε.naturality]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X : Cokleisli U
Y x✝ : C
f : (fromCokleisli U).obj X ⟶ Y
g : Y ⟶ x✝
⊢ f ≫ g = NatTrans.app (Comonad.δ U) X ≫ (NatTrans.app (Comonad.ε U) ((fromCokleisli U).obj X) ≫ (𝟭 C).map f) ≫ g
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
U : Comonad C
X : Cokleisli U
Y x✝ : C
f : (fromCokleisli U).obj X ⟶ Y
g : Y ⟶ x✝
⊢ f ≫ g = NatTrans.app (Comonad.δ U) X ≫ (NatTrans.app (Comonad.ε U) (U.obj X) ≫ f) ≫ g
[PROOFSTEP]
simp only [← Category.assoc, Comonad.left_counit, Category.id_comp]
