[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
α β : Type u
f : α → β
a : (ofTypeFunctor m ⋙ ofTypeFunctor m).obj α
⊢ ((ofTypeFunctor m ⋙ ofTypeFunctor m).map f ≫ joinM) a = (joinM ≫ (ofTypeFunctor m).map f) a
[PROOFSTEP]
apply joinM_map_map
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
α : Type u
a : (ofTypeFunctor m).obj ((ofTypeFunctor m ⋙ ofTypeFunctor m).obj α)
⊢ ((ofTypeFunctor m).map (NatTrans.app (NatTrans.mk (@joinM m inst✝¹)) α) ≫
        NatTrans.app (NatTrans.mk (@joinM m inst✝¹)) α)
      a =
    (NatTrans.app (NatTrans.mk (@joinM m inst✝¹)) ((ofTypeFunctor m).obj α) ≫
        NatTrans.app (NatTrans.mk (@joinM m inst✝¹)) α)
      a
[PROOFSTEP]
apply joinM_map_joinM
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
α : Type u
a : (𝟭 (Type u)).obj ((ofTypeFunctor m).obj α)
⊢ (NatTrans.app (NatTrans.mk (@pure m Applicative.toPure)) ((ofTypeFunctor m).obj α) ≫
        NatTrans.app (NatTrans.mk (@joinM m inst✝¹)) α)
      a =
    𝟙 ((𝟭 (Type u)).obj ((ofTypeFunctor m).obj α)) a
[PROOFSTEP]
apply joinM_pure
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
α : Type u
a : (ofTypeFunctor m).obj ((𝟭 (Type u)).obj α)
⊢ ((ofTypeFunctor m).map (NatTrans.app (NatTrans.mk (@pure m Applicative.toPure)) α) ≫
        NatTrans.app (NatTrans.mk (@joinM m inst✝¹)) α)
      a =
    𝟙 ((ofTypeFunctor m).obj ((𝟭 (Type u)).obj α)) a
[PROOFSTEP]
apply joinM_map_pure
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : KleisliCat m
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) =
    { obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g
[PROOFSTEP]
funext t
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : KleisliCat m
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) t =
    ({ obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g) t
[PROOFSTEP]
change _ = joinM (g <$> (f t))
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : KleisliCat m
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) t = joinM (g <$> f t)
[PROOFSTEP]
simp only [joinM, seq_bind_eq, Function.comp.left_id]
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : KleisliCat m
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ (f ≫ g) t = f t >>= g
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) =
    { obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g
[PROOFSTEP]
letI : _root_.Monad (ofTypeMonad m).obj := show _root_.Monad m from inferInstance
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
this : _root_.Monad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) =
    { obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g
[PROOFSTEP]
letI : LawfulMonad (ofTypeMonad m).obj := show LawfulMonad m from inferInstance
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
this✝ : _root_.Monad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
this : LawfulMonad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) =
    { obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g
[PROOFSTEP]
funext t
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
this✝ : _root_.Monad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
this : LawfulMonad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ { obj := fun X => X, map := fun {X Y} f => f }.map (f ≫ g) t =
    ({ obj := fun X => X, map := fun {X Y} f => f }.map f ≫ { obj := fun X => X, map := fun {X Y} f => f }.map g) t
[PROOFSTEP]
dsimp
  -- Porting note: missing tactic `unfold_projs`, using `change` instead.
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
this✝ : _root_.Monad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
this : LawfulMonad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ (f ≫ g) t = (f ≫ g) t
[PROOFSTEP]
change joinM (g <$> (f t)) = _
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
this✝ : _root_.Monad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
this : LawfulMonad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ joinM (g <$> f t) = (f ≫ g) t
[PROOFSTEP]
simp only [joinM, seq_bind_eq, Function.comp.left_id]
[GOAL]
case h
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ Z✝ : Kleisli (ofTypeMonad m)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
this✝ : _root_.Monad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
this : LawfulMonad (ofTypeMonad m).toFunctor.toPrefunctor.obj :=
  let_fun this := inferInstance;
  this
t : { obj := fun X => X, map := fun {X Y} f => f }.obj X✝
⊢ f t >>= g = (f ≫ g) t
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
⊢ 𝟭 (KleisliCat m) ≅
    Functor.mk { obj := fun X => X, map := fun {X Y} f => f } ⋙
      Functor.mk { obj := fun X => X, map := fun {X Y} f => f }
[PROOFSTEP]
refine' NatIso.ofComponents (fun X => Iso.refl X) fun f => _
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f : X✝ ⟶ Y✝
⊢ (𝟭 (KleisliCat m)).map f ≫ ((fun X => Iso.refl X) Y✝).hom =
    ((fun X => Iso.refl X) X✝).hom ≫
      (Functor.mk { obj := fun X => X, map := fun {X Y} f => f } ⋙
            Functor.mk { obj := fun X => X, map := fun {X Y} f => f }).map
        f
[PROOFSTEP]
change f >=> pure = pure >=> f
[GOAL]
m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f : X✝ ⟶ Y✝
⊢ f >=> pure = pure >=> f
[PROOFSTEP]
simp [functor_norm]
