[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
j : J
⊢ (NatTrans.app (η T) c.pt ≫ IsLimit.lift t (newCone D c)) ≫ NatTrans.app c.π j = 𝟙 c.pt ≫ NatTrans.app c.π j
[PROOFSTEP]
rw [Category.assoc, t.fac, newCone_π_app, ← T.η.naturality_assoc, Functor.id_map, (D.obj j).unit]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
j : J
⊢ NatTrans.app c.π j ≫ 𝟙 (D.obj j).A = 𝟙 c.pt ≫ NatTrans.app c.π j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
j : J
⊢ NatTrans.app c.π j ≫ 𝟙 (D.obj j).A = 𝟙 c.pt ≫ NatTrans.app c.π j
[PROOFSTEP]
simp
  -- See library note [dsimp, simp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
j : J
⊢ (NatTrans.app (μ T) c.pt ≫ IsLimit.lift t (newCone D c)) ≫ NatTrans.app c.π j =
    (T.map (IsLimit.lift t (newCone D c)) ≫ IsLimit.lift t (newCone D c)) ≫ NatTrans.app c.π j
[PROOFSTEP]
rw [Category.assoc, Category.assoc, t.fac (newCone D c), newCone_π_app, ← Functor.map_comp_assoc, t.fac (newCone D c),
  newCone_π_app, ← T.μ.naturality_assoc, (D.obj j).assoc, Functor.map_comp, Category.assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
j : J
⊢ (T.toFunctor ⋙ T.toFunctor).map (NatTrans.app c.π j) ≫ T.map (D.obj j).a ≫ (D.obj j).a =
    T.map (T.map (NatTrans.app c.π j)) ≫ T.map (D.obj j).a ≫ (D.obj j).a
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (conePoint D c t)).map f ≫ (fun j => Algebra.Hom.mk (NatTrans.app c.π j)) Y =
    (fun j => Algebra.Hom.mk (NatTrans.app c.π j)) X ≫ D.map f
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
X Y : J
f : X ⟶ Y
⊢ (((Functor.const J).obj (conePoint D c t)).map f ≫ (fun j => Algebra.Hom.mk (NatTrans.app c.π j)) Y).f =
    ((fun j => Algebra.Hom.mk (NatTrans.app c.π j)) X ≫ D.map f).f
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
X Y : J
f : X ⟶ Y
⊢ 𝟙 c.pt ≫ NatTrans.app c.π Y = NatTrans.app c.π X ≫ (D.map f).f
[PROOFSTEP]
erw [c.w f]
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
X Y : J
f : X ⟶ Y
⊢ 𝟙 c.pt ≫ NatTrans.app c.π Y = NatTrans.app c.π Y
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
s : Cone D
j : J
⊢ (T.map (IsLimit.lift t ((forget T).mapCone s)) ≫ (liftedCone D c t).pt.a) ≫ NatTrans.app c.π j =
    (s.pt.a ≫ IsLimit.lift t ((forget T).mapCone s)) ≫ NatTrans.app c.π j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
s : Cone D
j : J
⊢ (T.map (IsLimit.lift t ((forget T).mapCone s)) ≫ IsLimit.lift t (newCone D c)) ≫ NatTrans.app c.π j =
    (s.pt.a ≫ IsLimit.lift t ((forget T).mapCone s)) ≫ NatTrans.app c.π j
[PROOFSTEP]
rw [Category.assoc, Category.assoc, t.fac, newCone_π_app, ← Functor.map_comp_assoc, t.fac, Functor.mapCone_π_app]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
s : Cone D
j : J
⊢ T.map ((forget T).map (NatTrans.app s.π j)) ≫ (D.obj j).a = s.pt.a ≫ (forget T).map (NatTrans.app s.π j)
[PROOFSTEP]
apply (s.π.app j).h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝ : Category.{v, u} J✝
D : J✝ ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
s : Cone D
m : s.pt ⟶ (liftedCone D c t).pt
J : ∀ (j : J✝), m ≫ NatTrans.app (liftedCone D c t).π j = NatTrans.app s.π j
⊢ m = (fun s => Algebra.Hom.mk (IsLimit.lift t ((forget T).mapCone s))) s
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝ : Category.{v, u} J✝
D : J✝ ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
s : Cone D
m : s.pt ⟶ (liftedCone D c t).pt
J : ∀ (j : J✝), m ≫ NatTrans.app (liftedCone D c t).π j = NatTrans.app s.π j
⊢ m.f = ((fun s => Algebra.Hom.mk (IsLimit.lift t ((forget T).mapCone s))) s).f
[PROOFSTEP]
apply t.hom_ext
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝ : Category.{v, u} J✝
D : J✝ ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
s : Cone D
m : s.pt ⟶ (liftedCone D c t).pt
J : ∀ (j : J✝), m ≫ NatTrans.app (liftedCone D c t).π j = NatTrans.app s.π j
⊢ ∀ (j : J✝),
    m.f ≫ NatTrans.app c.π j =
      ((fun s => Algebra.Hom.mk (IsLimit.lift t ((forget T).mapCone s))) s).f ≫ NatTrans.app c.π j
[PROOFSTEP]
intro j
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝ : Category.{v, u} J✝
D : J✝ ⥤ Algebra T
c : Cone (D ⋙ forget T)
t : IsLimit c
s : Cone D
m : s.pt ⟶ (liftedCone D c t).pt
J : ∀ (j : J✝), m ≫ NatTrans.app (liftedCone D c t).π j = NatTrans.app s.π j
j : J✝
⊢ m.f ≫ NatTrans.app c.π j =
    ((fun s => Algebra.Hom.mk (IsLimit.lift t ((forget T).mapCone s))) s).f ≫ NatTrans.app c.π j
[PROOFSTEP]
simpa [t.fac ((forget T).mapCone s) j] using congr_arg Algebra.Hom.f (J j)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
⊢ NatTrans.app (η T) c.pt ≫ lambda c t = 𝟙 c.pt
[PROOFSTEP]
apply t.hom_ext
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
⊢ ∀ (j : J), NatTrans.app c.ι j ≫ NatTrans.app (η T) c.pt ≫ lambda c t = NatTrans.app c.ι j ≫ 𝟙 c.pt
[PROOFSTEP]
intro j
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ NatTrans.app c.ι j ≫ NatTrans.app (η T) c.pt ≫ lambda c t = NatTrans.app c.ι j ≫ 𝟙 c.pt
[PROOFSTEP]
rw [show c.ι.app j ≫ T.η.app c.pt ≫ _ = T.η.app (D.obj j).A ≫ _ ≫ _ from T.η.naturality_assoc _ _, commuting,
  Algebra.unit_assoc (D.obj j)]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ NatTrans.app c.ι j = NatTrans.app c.ι j ≫ 𝟙 c.pt
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ NatTrans.app c.ι j = NatTrans.app c.ι j ≫ 𝟙 c.pt
[PROOFSTEP]
simp
  -- See library note [dsimp, simp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
⊢ NatTrans.app (μ T) c.pt ≫ lambda c t = T.map (lambda c t) ≫ lambda c t
[PROOFSTEP]
refine' (isColimitOfPreserves _ (isColimitOfPreserves _ t)).hom_ext fun j => _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ NatTrans.app (T.mapCocone (T.mapCocone c)).ι j ≫ NatTrans.app (μ T) c.pt ≫ lambda c t =
    NatTrans.app (T.mapCocone (T.mapCocone c)).ι j ≫ T.map (lambda c t) ≫ lambda c t
[PROOFSTEP]
rw [Functor.mapCocone_ι_app, Functor.mapCocone_ι_app,
  show (T : C ⥤ C).map ((T : C ⥤ C).map _) ≫ _ ≫ _ = _ from T.μ.naturality_assoc _ _, ← Functor.map_comp_assoc,
  commuting, Functor.map_comp, Category.assoc, commuting]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ NatTrans.app (μ T) ((D ⋙ forget T).obj j) ≫ (D.obj j).a ≫ NatTrans.app c.ι j =
    T.map (D.obj j).a ≫ (D.obj j).a ≫ NatTrans.app c.ι j
[PROOFSTEP]
apply (D.obj j).assoc_assoc _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ D.map f ≫ (fun j => Algebra.Hom.mk (NatTrans.app c.ι j)) B =
    (fun j => Algebra.Hom.mk (NatTrans.app c.ι j)) A ≫ ((Functor.const J).obj (coconePoint c t)).map f
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ (D.map f ≫ (fun j => Algebra.Hom.mk (NatTrans.app c.ι j)) B).f =
    ((fun j => Algebra.Hom.mk (NatTrans.app c.ι j)) A ≫ ((Functor.const J).obj (coconePoint c t)).map f).f
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ (D.map f).f ≫ NatTrans.app c.ι B = NatTrans.app c.ι A ≫ 𝟙 c.pt
[PROOFSTEP]
rw [comp_id]
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ (D.map f).f ≫ NatTrans.app c.ι B = NatTrans.app c.ι A
[PROOFSTEP]
apply c.w
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ NatTrans.app (T.mapCocone c).ι j ≫ T.map (IsColimit.desc t ((forget T).mapCocone s)) ≫ s.pt.a =
    NatTrans.app (T.mapCocone c).ι j ≫ (liftedCocone c t).pt.a ≫ IsColimit.desc t ((forget T).mapCocone s)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map (NatTrans.app c.ι j) ≫ T.map (IsColimit.desc t ((forget T).mapCocone s)) ≫ s.pt.a =
    T.map (NatTrans.app c.ι j) ≫ lambda c t ≫ IsColimit.desc t ((forget T).mapCocone s)
[PROOFSTEP]
rw [← Functor.map_comp_assoc, ← Category.assoc, t.fac, commuting, Category.assoc, t.fac]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map (NatTrans.app ((forget T).mapCocone s).ι j) ≫ s.pt.a = (D.obj j).a ≫ NatTrans.app ((forget T).mapCocone s).ι j
[PROOFSTEP]
apply Algebra.Hom.h
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝² : Category.{v, u} J✝
D : J✝ ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
m : (liftedCocone c t).pt ⟶ s.pt
J : ∀ (j : J✝), NatTrans.app (liftedCocone c t).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => Algebra.Hom.mk (IsColimit.desc t ((forget T).mapCocone s))) s
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝² : Category.{v, u} J✝
D : J✝ ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
m : (liftedCocone c t).pt ⟶ s.pt
J : ∀ (j : J✝), NatTrans.app (liftedCocone c t).ι j ≫ m = NatTrans.app s.ι j
⊢ m.f = ((fun s => Algebra.Hom.mk (IsColimit.desc t ((forget T).mapCocone s))) s).f
[PROOFSTEP]
apply t.hom_ext
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝² : Category.{v, u} J✝
D : J✝ ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
m : (liftedCocone c t).pt ⟶ s.pt
J : ∀ (j : J✝), NatTrans.app (liftedCocone c t).ι j ≫ m = NatTrans.app s.ι j
⊢ ∀ (j : J✝),
    NatTrans.app c.ι j ≫ m.f =
      NatTrans.app c.ι j ≫ ((fun s => Algebra.Hom.mk (IsColimit.desc t ((forget T).mapCocone s))) s).f
[PROOFSTEP]
intro j
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J✝ : Type u
inst✝² : Category.{v, u} J✝
D : J✝ ⥤ Algebra T
c : Cocone (D ⋙ forget T)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
m : (liftedCocone c t).pt ⟶ s.pt
J : ∀ (j : J✝), NatTrans.app (liftedCocone c t).ι j ≫ m = NatTrans.app s.ι j
j : J✝
⊢ NatTrans.app c.ι j ≫ m.f =
    NatTrans.app c.ι j ≫ ((fun s => Algebra.Hom.mk (IsColimit.desc t ((forget T).mapCocone s))) s).f
[PROOFSTEP]
simpa using congr_arg Algebra.Hom.f (J j)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
c : Cocone (D ⋙ forget T)
t : IsColimit c
A B : J
f : A ⟶ B
⊢ D.map f ≫ (fun j => Algebra.Hom.mk (NatTrans.app c.ι j)) B =
    (fun j => Algebra.Hom.mk (NatTrans.app c.ι j)) A ≫ ((Functor.const J).obj (coconePoint c t)).map f
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
c : Cocone (D ⋙ forget T)
t : IsColimit c
A B : J
f : A ⟶ B
⊢ (D.map f ≫ (fun j => Algebra.Hom.mk (NatTrans.app c.ι j)) B).f =
    ((fun j => Algebra.Hom.mk (NatTrans.app c.ι j)) A ≫ ((Functor.const J).obj (coconePoint c t)).map f).f
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ Algebra T
inst✝¹ : PreservesColimit (D ⋙ forget T) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ forget T) ⋙ T.toFunctor) T.toFunctor
c : Cocone (D ⋙ forget T)
t : IsColimit c
A B : J
f : A ⟶ B
⊢ (D.map f).f ≫ NatTrans.app c.ι B = NatTrans.app c.ι A ≫ 𝟙 c.pt
[PROOFSTEP]
erw [comp_id, c.w]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : PreservesColimitsOfShape J T.toFunctor
⊢ {K : J ⥤ Algebra T} → CreatesColimit K (forget T)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : PreservesColimitsOfSize.{v, u, v₁, v₁, u₁, u₁} T.toFunctor
⊢ {J : Type u} → [inst : Category.{v, u} J] → CreatesColimitsOfShape J (forget T)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
⊢ CreatesColimit K R
[PROOFSTEP]
letI A := Monad.comparison (Adjunction.ofRightAdjoint R)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
A : D ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) :=
  Monad.comparison (Adjunction.ofRightAdjoint R)
⊢ CreatesColimit K R
[PROOFSTEP]
letI B := Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
A : D ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) :=
  Monad.comparison (Adjunction.ofRightAdjoint R)
B : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ⥤ C :=
  Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ CreatesColimit K R
[PROOFSTEP]
let i : (K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙ Monad.forget _ ≅ K ⋙ R :=
  Functor.associator _ _ _ ≪≫ isoWhiskerLeft K (Monad.comparisonForget (Adjunction.ofRightAdjoint R))
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
A : D ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) :=
  Monad.comparison (Adjunction.ofRightAdjoint R)
B : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ⥤ C :=
  Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
i : (K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙
    Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ≅
  K ⋙ R :=
  Functor.associator K (Monad.comparison (Adjunction.ofRightAdjoint R))
      (Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ≪≫
    isoWhiskerLeft K (Monad.comparisonForget (Adjunction.ofRightAdjoint R))
⊢ CreatesColimit K R
[PROOFSTEP]
letI :
  PreservesColimit ((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)))
    (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  by
  dsimp
  refine' preservesColimitOfIsoDiagram _ i.symm
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
A : D ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) :=
  Monad.comparison (Adjunction.ofRightAdjoint R)
B : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ⥤ C :=
  Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
i : (K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙
    Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ≅
  K ⋙ R :=
  Functor.associator K (Monad.comparison (Adjunction.ofRightAdjoint R))
      (Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ≪≫
    isoWhiskerLeft K (Monad.comparisonForget (Adjunction.ofRightAdjoint R))
⊢ PreservesColimit ((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)))
    (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
A : D ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) :=
  Monad.comparison (Adjunction.ofRightAdjoint R)
B : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ⥤ C :=
  Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
i : (K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙
    Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ≅
  K ⋙ R :=
  Functor.associator K (Monad.comparison (Adjunction.ofRightAdjoint R))
      (Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ≪≫
    isoWhiskerLeft K (Monad.comparisonForget (Adjunction.ofRightAdjoint R))
⊢ PreservesColimit
    ((K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙
      Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)))
    (leftAdjoint R ⋙ R)
[PROOFSTEP]
refine' preservesColimitOfIsoDiagram _ i.symm
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
A : D ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) :=
  Monad.comparison (Adjunction.ofRightAdjoint R)
B : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ⥤ C :=
  Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
i : (K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙
    Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ≅
  K ⋙ R :=
  Functor.associator K (Monad.comparison (Adjunction.ofRightAdjoint R))
      (Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ≪≫
    isoWhiskerLeft K (Monad.comparisonForget (Adjunction.ofRightAdjoint R))
this : PreservesColimit ((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)))
  (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  id (preservesColimitOfIsoDiagram (leftAdjoint R ⋙ R) i.symm)
⊢ CreatesColimit K R
[PROOFSTEP]
letI :
  PreservesColimit
    (((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ⋙
      (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor)
    (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  by
  dsimp
  refine' preservesColimitOfIsoDiagram _ (isoWhiskerRight i (leftAdjoint R ⋙ R)).symm
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
A : D ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) :=
  Monad.comparison (Adjunction.ofRightAdjoint R)
B : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ⥤ C :=
  Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
i : (K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙
    Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ≅
  K ⋙ R :=
  Functor.associator K (Monad.comparison (Adjunction.ofRightAdjoint R))
      (Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ≪≫
    isoWhiskerLeft K (Monad.comparisonForget (Adjunction.ofRightAdjoint R))
this : PreservesColimit ((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)))
  (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  id (preservesColimitOfIsoDiagram (leftAdjoint R ⋙ R) i.symm)
⊢ PreservesColimit
    (((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ⋙
      (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor)
    (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
A : D ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) :=
  Monad.comparison (Adjunction.ofRightAdjoint R)
B : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ⥤ C :=
  Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
i : (K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙
    Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ≅
  K ⋙ R :=
  Functor.associator K (Monad.comparison (Adjunction.ofRightAdjoint R))
      (Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ≪≫
    isoWhiskerLeft K (Monad.comparisonForget (Adjunction.ofRightAdjoint R))
this : PreservesColimit ((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)))
  (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  id (preservesColimitOfIsoDiagram (leftAdjoint R ⋙ R) i.symm)
⊢ PreservesColimit
    (((K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙
        Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ⋙
      leftAdjoint R ⋙ R)
    (leftAdjoint R ⋙ R)
[PROOFSTEP]
refine' preservesColimitOfIsoDiagram _ (isoWhiskerRight i (leftAdjoint R ⋙ R)).symm
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
A : D ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) :=
  Monad.comparison (Adjunction.ofRightAdjoint R)
B : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ⥤ C :=
  Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
i : (K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙
    Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ≅
  K ⋙ R :=
  Functor.associator K (Monad.comparison (Adjunction.ofRightAdjoint R))
      (Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ≪≫
    isoWhiskerLeft K (Monad.comparisonForget (Adjunction.ofRightAdjoint R))
this✝ : PreservesColimit ((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)))
  (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  id (preservesColimitOfIsoDiagram (leftAdjoint R ⋙ R) i.symm)
this : PreservesColimit
  (((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ⋙
    (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor)
  (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  id (preservesColimitOfIsoDiagram (leftAdjoint R ⋙ R) (isoWhiskerRight i (leftAdjoint R ⋙ R)).symm)
⊢ CreatesColimit K R
[PROOFSTEP]
letI : CreatesColimit (K ⋙ A) B := CategoryTheory.Monad.forgetCreatesColimit _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
A : D ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) :=
  Monad.comparison (Adjunction.ofRightAdjoint R)
B : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ⥤ C :=
  Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
i : (K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙
    Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ≅
  K ⋙ R :=
  Functor.associator K (Monad.comparison (Adjunction.ofRightAdjoint R))
      (Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ≪≫
    isoWhiskerLeft K (Monad.comparisonForget (Adjunction.ofRightAdjoint R))
this✝¹ : PreservesColimit ((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)))
  (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  id (preservesColimitOfIsoDiagram (leftAdjoint R ⋙ R) i.symm)
this✝ : PreservesColimit
  (((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ⋙
    (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor)
  (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  id (preservesColimitOfIsoDiagram (leftAdjoint R ⋙ R) (isoWhiskerRight i (leftAdjoint R ⋙ R)).symm)
this : CreatesColimit (K ⋙ A) B := Monad.forgetCreatesColimit (K ⋙ A)
⊢ CreatesColimit K R
[PROOFSTEP]
letI : CreatesColimit K (A ⋙ B) := CategoryTheory.compCreatesColimit _ _
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
A : D ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) :=
  Monad.comparison (Adjunction.ofRightAdjoint R)
B : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ⥤ C :=
  Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
i : (K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙
    Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ≅
  K ⋙ R :=
  Functor.associator K (Monad.comparison (Adjunction.ofRightAdjoint R))
      (Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ≪≫
    isoWhiskerLeft K (Monad.comparisonForget (Adjunction.ofRightAdjoint R))
this✝² : PreservesColimit ((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)))
  (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  id (preservesColimitOfIsoDiagram (leftAdjoint R ⋙ R) i.symm)
this✝¹ : PreservesColimit
  (((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ⋙
    (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor)
  (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  id (preservesColimitOfIsoDiagram (leftAdjoint R ⋙ R) (isoWhiskerRight i (leftAdjoint R ⋙ R)).symm)
this✝ : CreatesColimit (K ⋙ A) B := Monad.forgetCreatesColimit (K ⋙ A)
this : CreatesColimit K (A ⋙ B) := compCreatesColimit A B
⊢ CreatesColimit K R
[PROOFSTEP]
let e := (Monad.comparisonForget (Adjunction.ofRightAdjoint R))
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (leftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ leftAdjoint R ⋙ R) (leftAdjoint R ⋙ R)
A : D ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) :=
  Monad.comparison (Adjunction.ofRightAdjoint R)
B : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ⥤ C :=
  Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
i : (K ⋙ Monad.comparison (Adjunction.ofRightAdjoint R)) ⋙
    Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ≅
  K ⋙ R :=
  Functor.associator K (Monad.comparison (Adjunction.ofRightAdjoint R))
      (Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ≪≫
    isoWhiskerLeft K (Monad.comparisonForget (Adjunction.ofRightAdjoint R))
this✝² : PreservesColimit ((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)))
  (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  id (preservesColimitOfIsoDiagram (leftAdjoint R ⋙ R) i.symm)
this✝¹ : PreservesColimit
  (((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R))) ⋙
    (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor)
  (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor :=
  id (preservesColimitOfIsoDiagram (leftAdjoint R ⋙ R) (isoWhiskerRight i (leftAdjoint R ⋙ R)).symm)
this✝ : CreatesColimit (K ⋙ A) B := Monad.forgetCreatesColimit (K ⋙ A)
this : CreatesColimit K (A ⋙ B) := compCreatesColimit A B
e : Monad.comparison (Adjunction.ofRightAdjoint R) ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint R)) ≅
  R :=
  Monad.comparisonForget (Adjunction.ofRightAdjoint R)
⊢ CreatesColimit K R
[PROOFSTEP]
apply createsColimitOfNatIso e
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : MonadicRightAdjoint R
inst✝ : PreservesColimitsOfShape J R
⊢ PreservesColimitsOfShape J (leftAdjoint R)
[PROOFSTEP]
apply (Adjunction.leftAdjointPreservesColimits (Adjunction.ofRightAdjoint R)).1
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : MonadicRightAdjoint R
inst✝ : PreservesColimitsOfShape J R
this : PreservesColimitsOfShape J (leftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape
⊢ PreservesColimitsOfShape J (leftAdjoint R ⋙ R)
[PROOFSTEP]
apply CategoryTheory.Limits.compPreservesColimitsOfShape _ _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
⊢ HasColimit F
[PROOFSTEP]
let c := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ leftAdjoint R) := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
⊢ HasColimit F
[PROOFSTEP]
letI : PreservesColimitsOfShape J _ := (Adjunction.ofRightAdjoint R).leftAdjointPreservesColimits.1
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ leftAdjoint R) := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape J (leftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape
⊢ HasColimit F
[PROOFSTEP]
let t : IsColimit c := isColimitOfPreserves (leftAdjoint R) (colimit.isColimit _)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ leftAdjoint R) := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape J (leftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape
t : IsColimit c := isColimitOfPreserves (leftAdjoint R) (colimit.isColimit (F ⋙ R))
⊢ HasColimit F
[PROOFSTEP]
apply HasColimit.mk ⟨_, (IsColimit.precomposeInvEquiv _ _).symm t⟩
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ leftAdjoint R) := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape J (leftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape
t : IsColimit c := isColimitOfPreserves (leftAdjoint R) (colimit.isColimit (F ⋙ R))
⊢ (F ⋙ R) ⋙ leftAdjoint R ≅ F
[PROOFSTEP]
apply (isoWhiskerLeft F (asIso (Adjunction.ofRightAdjoint R).counit) : _) ≪≫ F.rightUnitor
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
⊢ PreservesLimit K (leftAdjoint R)
[PROOFSTEP]
let F := Functor.empty.{v} D
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
F : Discrete PEmpty ⥤ D := Functor.empty D
⊢ PreservesLimit K (leftAdjoint R)
[PROOFSTEP]
letI : PreservesLimit (F ⋙ R) (leftAdjoint R) := by
  constructor
  intro c h
  haveI : HasLimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
  haveI : HasLimit F := hasLimit_of_reflective F R
  apply isLimitChangeEmptyCone D (limit.isLimit F)
  apply (asIso ((Adjunction.ofRightAdjoint R).counit.app _)).symm.trans
  apply (leftAdjoint R).mapIso
  letI := monadicCreatesLimits.{v, v} R
  let A := (CategoryTheory.preservesLimitOfCreatesLimitAndHasLimit F R)
  apply (A.preserves (limit.isLimit F)).conePointUniqueUpToIso h
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
F : Discrete PEmpty ⥤ D := Functor.empty D
⊢ PreservesLimit (F ⋙ R) (leftAdjoint R)
[PROOFSTEP]
constructor
[GOAL]
case preserves
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
F : Discrete PEmpty ⥤ D := Functor.empty D
⊢ {c : Cone (F ⋙ R)} → IsLimit c → IsLimit ((leftAdjoint R).mapCone c)
[PROOFSTEP]
intro c h
[GOAL]
case preserves
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
F : Discrete PEmpty ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
⊢ IsLimit ((leftAdjoint R).mapCone c)
[PROOFSTEP]
haveI : HasLimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
[GOAL]
case preserves
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
F : Discrete PEmpty ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this : HasLimit (F ⋙ R)
⊢ IsLimit ((leftAdjoint R).mapCone c)
[PROOFSTEP]
haveI : HasLimit F := hasLimit_of_reflective F R
[GOAL]
case preserves
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
F : Discrete PEmpty ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ IsLimit ((leftAdjoint R).mapCone c)
[PROOFSTEP]
apply isLimitChangeEmptyCone D (limit.isLimit F)
[GOAL]
case preserves.hi
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
F : Discrete PEmpty ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ (limit.cone F).pt ≅ ((leftAdjoint R).mapCone c).pt
[PROOFSTEP]
apply (asIso ((Adjunction.ofRightAdjoint R).counit.app _)).symm.trans
[GOAL]
case preserves.hi
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
F : Discrete PEmpty ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ (R ⋙ leftAdjoint R).obj (limit.cone F).1 ≅ ((leftAdjoint R).mapCone c).pt
[PROOFSTEP]
apply (leftAdjoint R).mapIso
[GOAL]
case preserves.hi
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
F : Discrete PEmpty ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ R.obj (limit.cone F).1 ≅ c.pt
[PROOFSTEP]
letI := monadicCreatesLimits.{v, v} R
[GOAL]
case preserves.hi
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
F : Discrete PEmpty ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝¹ : HasLimit (F ⋙ R)
this✝ : HasLimit F
this : CreatesLimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := monadicCreatesLimits R
⊢ R.obj (limit.cone F).1 ≅ c.pt
[PROOFSTEP]
let A := (CategoryTheory.preservesLimitOfCreatesLimitAndHasLimit F R)
[GOAL]
case preserves.hi
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
F : Discrete PEmpty ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝¹ : HasLimit (F ⋙ R)
this✝ : HasLimit F
this : CreatesLimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := monadicCreatesLimits R
A : PreservesLimit F R := preservesLimitOfCreatesLimitAndHasLimit F R
⊢ R.obj (limit.cone F).1 ≅ c.pt
[PROOFSTEP]
apply (A.preserves (limit.isLimit F)).conePointUniqueUpToIso h
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u
inst✝¹ : Category.{v, u} J
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty ⥤ C
F : Discrete PEmpty ⥤ D := Functor.empty D
this : PreservesLimit (F ⋙ R) (leftAdjoint R) :=
  {
    preserves := fun {c} h =>
      isLimitChangeEmptyCone D (limit.isLimit F) ((leftAdjoint R).mapCone c)
        ((asIso (NatTrans.app (Adjunction.ofRightAdjoint R).counit (limit.cone F).1)).symm ≪≫
          (leftAdjoint R).mapIso
            (let A := preservesLimitOfCreatesLimitAndHasLimit F R;
            IsLimit.conePointUniqueUpToIso (PreservesLimit.preserves (limit.isLimit F)) h)) }
⊢ PreservesLimit K (leftAdjoint R)
[PROOFSTEP]
apply preservesLimitOfIsoDiagram _ (Functor.emptyExt (F ⋙ R) _)
