[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) _)


[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a b c d : WithTerminal C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases a
[GOAL]
case of
C : Type u
inst✝ : Category.{v, u} C
b c d : WithTerminal C
g : b ⟶ c
h : c ⟶ d
a✝ : C
f : of a✝ ⟶ b
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases b
[GOAL]
case star
C : Type u
inst✝ : Category.{v, u} C
b c d : WithTerminal C
g : b ⟶ c
h : c ⟶ d
f : star ⟶ b
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases b
[GOAL]
case of.of
C : Type u
inst✝ : Category.{v, u} C
c d : WithTerminal C
h : c ⟶ d
a✝¹ a✝ : C
g : of a✝ ⟶ c
f : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case of.star
C : Type u
inst✝ : Category.{v, u} C
c d : WithTerminal C
h : c ⟶ d
a✝ : C
g : star ⟶ c
f : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case star.of
C : Type u
inst✝ : Category.{v, u} C
c d : WithTerminal C
h : c ⟶ d
a✝ : C
g : of a✝ ⟶ c
f : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case star.star
C : Type u
inst✝ : Category.{v, u} C
c d : WithTerminal C
h : c ⟶ d
g : star ⟶ c
f : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case of.of.of
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝ ⟶ d
g : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.of.star
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
h : star ⟶ d
g : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.star.of
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
a✝¹ : C
f : of a✝¹ ⟶ star
a✝ : C
h : of a✝ ⟶ d
g : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.star.star
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
a✝ : C
f : of a✝ ⟶ star
h : star ⟶ d
g : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.of.of
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
a✝¹ : C
f : star ⟶ of a✝¹
a✝ : C
h : of a✝ ⟶ d
g : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.of.star
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
a✝ : C
f : star ⟶ of a✝
h : star ⟶ d
g : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.star.of
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
f : star ⟶ star
a✝ : C
h : of a✝ ⟶ d
g : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.star.star
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
f : star ⟶ star
h : star ⟶ d
g : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝³ a✝² : C
f : of a✝³ ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝³ a✝² : C
f : of a✝³ ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : of a✝² ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : of a✝² ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : of a✝ ⟶ star
g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : of a✝ ⟶ star
g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : star ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : star ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : star ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : star ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.of.of
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.of.of
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.of.star
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.of.star
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.star.of
C : Type u
inst✝ : Category.{v, u} C
f g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.star.of
C : Type u
inst✝ : Category.{v, u} C
f g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.star.star
C : Type u
inst✝ : Category.{v, u} C
f g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.star.star
C : Type u
inst✝ : Category.{v, u} C
f g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
exact (h : PEmpty).elim
[GOAL]
case of.star.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : of a✝² ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
exact (g : PEmpty).elim
[GOAL]
case of.star.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
exact (h : PEmpty).elim
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : WithTerminal C
⊢ ∀ (a : X ⟶ star), a = default
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
x : C
⊢ (lift F M hM).map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ (liftStar F M hM).hom =
    NatTrans.app (inclLift F M hM).hom x ≫ M x
[PROOFSTEP]
erw [Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
x : C
⊢ (lift F M hM).map (Limits.IsTerminal.from starTerminal (incl.obj x)) = M x
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
⊢ ∀ {X Y : WithTerminal C} (f : X ⟶ Y),
    G.map f ≫
        ((fun X =>
              match X with
              | of x => h.app x
              | star => hG)
            Y).hom =
      ((fun X =>
              match X with
              | of x => h.app x
              | star => hG)
            X).hom ≫
        (lift F M hM).map f
[PROOFSTEP]
rintro (X | X) (Y | Y) f
[GOAL]
case of.of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
X Y : C
f : of X ⟶ of Y
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of Y)).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of X)).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
apply h.hom.naturality
[GOAL]
case of.star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
X : C
f : of X ⟶ star
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of X)).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
cases f
[GOAL]
case of.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
X : C
⊢ G.map PUnit.unit ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of X)).hom ≫
      (lift F M hM).map PUnit.unit
[PROOFSTEP]
exact hh _
[GOAL]
case star.of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
Y : C
f : star ⟶ of Y
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of Y)).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
cases f
[GOAL]
case star.star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
f : star ⟶ star
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
cases f
[GOAL]
case star.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
⊢ G.map PUnit.unit ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map PUnit.unit
[PROOFSTEP]
change G.map (𝟙 _) ≫ hG.hom = hG.hom ≫ 𝟙 _
[GOAL]
case star.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
⊢ G.map (𝟙 star) ≫ hG.hom = hG.hom ≫ 𝟙 Z
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a b c d : WithInitial C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases a
[GOAL]
case of
C : Type u
inst✝ : Category.{v, u} C
b c d : WithInitial C
g : b ⟶ c
h : c ⟶ d
a✝ : C
f : of a✝ ⟶ b
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases b
[GOAL]
case star
C : Type u
inst✝ : Category.{v, u} C
b c d : WithInitial C
g : b ⟶ c
h : c ⟶ d
f : star ⟶ b
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases b
[GOAL]
case of.of
C : Type u
inst✝ : Category.{v, u} C
c d : WithInitial C
h : c ⟶ d
a✝¹ a✝ : C
g : of a✝ ⟶ c
f : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case of.star
C : Type u
inst✝ : Category.{v, u} C
c d : WithInitial C
h : c ⟶ d
a✝ : C
g : star ⟶ c
f : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case star.of
C : Type u
inst✝ : Category.{v, u} C
c d : WithInitial C
h : c ⟶ d
a✝ : C
g : of a✝ ⟶ c
f : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case star.star
C : Type u
inst✝ : Category.{v, u} C
c d : WithInitial C
h : c ⟶ d
g : star ⟶ c
f : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case of.of.of
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝ ⟶ d
g : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.of.star
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
h : star ⟶ d
g : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.star.of
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
a✝¹ : C
f : of a✝¹ ⟶ star
a✝ : C
h : of a✝ ⟶ d
g : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.star.star
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
a✝ : C
f : of a✝ ⟶ star
h : star ⟶ d
g : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.of.of
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
a✝¹ : C
f : star ⟶ of a✝¹
a✝ : C
h : of a✝ ⟶ d
g : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.of.star
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
a✝ : C
f : star ⟶ of a✝
h : star ⟶ d
g : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.star.of
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
f : star ⟶ star
a✝ : C
h : of a✝ ⟶ d
g : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.star.star
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
f : star ⟶ star
h : star ⟶ d
g : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝³ a✝² : C
f : of a✝³ ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝³ a✝² : C
f : of a✝³ ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : of a✝² ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : of a✝² ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : of a✝ ⟶ star
g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : of a✝ ⟶ star
g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : star ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : star ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : star ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : star ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.of.of
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.of.of
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.of.star
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.of.star
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.star.of
C : Type u
inst✝ : Category.{v, u} C
f g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.star.of
C : Type u
inst✝ : Category.{v, u} C
f g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.star.star
C : Type u
inst✝ : Category.{v, u} C
f g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.star.star
C : Type u
inst✝ : Category.{v, u} C
f g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
exact (g : PEmpty).elim
[GOAL]
case of.star.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : of a✝² ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
exact (f : PEmpty).elim
[GOAL]
case of.star.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
exact (f : PEmpty).elim
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : WithInitial C
⊢ ∀ (a : star ⟶ X), a = default
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
x : C
⊢ (liftStar F M hM).hom ≫ (lift F M hM).map (Limits.IsInitial.to starInitial (incl.obj x)) =
    M x ≫ NatTrans.app (inclLift F M hM).hom x
[PROOFSTEP]
erw [Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
x : C
⊢ (lift F M hM).map (Limits.IsInitial.to starInitial (incl.obj x)) = M x
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
⊢ ∀ {X Y : WithInitial C} (f : X ⟶ Y),
    G.map f ≫
        ((fun X =>
              match X with
              | of x => h.app x
              | star => hG)
            Y).hom =
      ((fun X =>
              match X with
              | of x => h.app x
              | star => hG)
            X).hom ≫
        (lift F M hM).map f
[PROOFSTEP]
rintro (X | X) (Y | Y) f
[GOAL]
case of.of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
X Y : C
f : of X ⟶ of Y
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of Y)).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of X)).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
apply h.hom.naturality
[GOAL]
case of.star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
X : C
f : of X ⟶ star
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of X)).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
cases f
[GOAL]
case star.of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
Y : C
f : star ⟶ of Y
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of Y)).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
cases f
[GOAL]
case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
Y : C
⊢ G.map PUnit.unit ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of Y)).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map PUnit.unit
[PROOFSTEP]
change G.map _ ≫ h.hom.app _ = hG.hom ≫ _
[GOAL]
case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
Y : C
⊢ G.map PUnit.unit ≫ NatTrans.app h.hom Y = hG.hom ≫ (lift F M hM).map PUnit.unit
[PROOFSTEP]
symm
[GOAL]
case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
Y : C
⊢ hG.hom ≫ (lift F M hM).map PUnit.unit = G.map PUnit.unit ≫ NatTrans.app h.hom Y
[PROOFSTEP]
erw [← Iso.eq_inv_comp, ← Category.assoc, hh]
[GOAL]
case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
Y : C
⊢ (lift F M hM).map PUnit.unit = (M Y ≫ NatTrans.app h.symm.hom Y) ≫ NatTrans.app h.hom Y
[PROOFSTEP]
simp
[GOAL]
case star.star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
f : star ⟶ star
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
cases f
[GOAL]
case star.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
⊢ G.map PUnit.unit ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map PUnit.unit
[PROOFSTEP]
change G.map (𝟙 _) ≫ hG.hom = hG.hom ≫ 𝟙 _
[GOAL]
case star.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
⊢ G.map (𝟙 star) ≫ hG.hom = hG.hom ≫ 𝟙 Z
[PROOFSTEP]
simp


[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ IsReflexivePair (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
[PROOFSTEP]
apply IsReflexivePair.mk' _ _ _
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ (free T).obj X.A ⟶ (free T).obj (T.obj X.A)
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ ?m.2463 ≫ FreeCoequalizer.topMap X = 𝟙 ((free T).obj X.A)
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ ?m.2463 ≫ FreeCoequalizer.bottomMap X = 𝟙 ((free T).obj X.A)
[PROOFSTEP]
apply (free T).map (T.η.app X.A)
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ (free T).map (NatTrans.app (η T) X.A) ≫ FreeCoequalizer.topMap X = 𝟙 ((free T).obj X.A)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ ((free T).map (NatTrans.app (η T) X.A) ≫ FreeCoequalizer.topMap X).f = (𝟙 ((free T).obj X.A)).f
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ T.map (NatTrans.app (η T) X.A) ≫ T.map X.a = 𝟙 (T.obj X.A)
[PROOFSTEP]
rw [← Functor.map_comp, X.unit, Functor.map_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ (free T).map (NatTrans.app (η T) X.A) ≫ FreeCoequalizer.bottomMap X = 𝟙 ((free T).obj X.A)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
⊢ ((free T).map (NatTrans.app (η T) X.A) ≫ FreeCoequalizer.bottomMap X).f = (𝟙 ((free T).obj X.A)).f
[PROOFSTEP]
apply Monad.right_unit
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
⊢ { l //
    Cofork.π (beckAlgebraCofork X) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
have h₁ : (T : C ⥤ C).map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f := congr_arg Monad.Algebra.Hom.f s.condition
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ { l //
    Cofork.π (beckAlgebraCofork X) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
have h₂ : (T : C ⥤ C).map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f := s.π.h
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ { l //
    Cofork.π (beckAlgebraCofork X) ≫ l = Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s → m = l }
[PROOFSTEP]
refine' ⟨⟨T.η.app _ ≫ s.π.f, _⟩, _, _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ T.map (NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f) ≫ s.pt.a =
    (beckAlgebraCofork X).pt.a ≫ NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ T.map (NatTrans.app (η T) X.1 ≫ (Cofork.π s).f) ≫ s.pt.a = X.a ≫ NatTrans.app (η T) X.1 ≫ (Cofork.π s).f
[PROOFSTEP]
rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc, show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _,
  h₁, Monad.left_unit_assoc]
[GOAL]
case refine'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ Cofork.π (beckAlgebraCofork X) ≫ Algebra.Hom.mk (NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f) =
    Cofork.π s
[PROOFSTEP]
ext
[GOAL]
case refine'_2.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ (Cofork.π (beckAlgebraCofork X) ≫ Algebra.Hom.mk (NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f)).f =
    (Cofork.π s).f
[PROOFSTEP]
simpa [← T.η.naturality_assoc, T.left_unit_assoc] using T.η.app ((T : C ⥤ C).obj X.A) ≫= h₁
[GOAL]
case refine'_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
⊢ ∀
    {m :
      ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
        ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
    Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s →
      m = Algebra.Hom.mk (NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f)
[PROOFSTEP]
intro m hm
[GOAL]
case refine'_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
m :
  ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm : Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s
⊢ m = Algebra.Hom.mk (NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f)
[PROOFSTEP]
ext
[GOAL]
case refine'_3.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
m :
  ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm : Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s
⊢ m.f = (Algebra.Hom.mk (NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f)).f
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_3.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
m :
  ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm : Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s
⊢ m.f = NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π s).f
[PROOFSTEP]
rw [← hm]
[GOAL]
case refine'_3.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : Algebra T
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ (Cofork.π s).f = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
h₂ : T.map (Cofork.π s).f ≫ s.pt.a = NatTrans.app (μ T) X.A ≫ (Cofork.π s).f
m :
  ((Functor.const WalkingParallelPair).obj (beckAlgebraCofork X).pt).obj WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm : Cofork.π (beckAlgebraCofork X) ≫ m = Cofork.π s
⊢ m.f = NatTrans.app (η T) (beckAlgebraCofork X).pt.1 ≫ (Cofork.π (beckAlgebraCofork X) ≫ m).f
[PROOFSTEP]
apply (X.unit_assoc _).symm


[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]


[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_5, u_2} D
inst✝⁴ : Category.{?u.20851, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : HasShift E A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
X : C
⊢ NatTrans.app (isoAdd e₁ e₂).hom X =
    F.map (NatTrans.app (shiftFunctorAdd C a b).hom X) ≫
      NatTrans.app e₂.hom ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map (NatTrans.app e₁.hom X) ≫ NatTrans.app (shiftFunctorAdd D a b).inv (F.obj X)
[PROOFSTEP]
simp only [isoAdd, isoAdd'_hom_app, shiftFunctorAdd'_eq_shiftFunctorAdd]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_5, u_2} D
inst✝⁴ : Category.{?u.24197, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : HasShift E A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
X : C
⊢ NatTrans.app (isoAdd e₁ e₂).inv X =
    NatTrans.app (shiftFunctorAdd D a b).hom (F.obj X) ≫
      (shiftFunctor D b).map (NatTrans.app e₁.inv X) ≫
        NatTrans.app e₂.inv ((shiftFunctor C a).obj X) ≫ F.map (NatTrans.app (shiftFunctorAdd C a b).inv X)
[PROOFSTEP]
simp only [isoAdd, isoAdd'_inv_app, shiftFunctorAdd'_eq_shiftFunctorAdd]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁷ : Category.{u_6, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
inst✝⁵ : Category.{?u.38582, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : CommShift F A
a b c : A
h : a + b = c
⊢ commShiftIso F c = CommShift.isoAdd' h (commShiftIso F a) (commShiftIso F b)
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁷ : Category.{u_6, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
inst✝⁵ : Category.{?u.38582, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : CommShift F A
a b : A
⊢ commShiftIso F (a + b) = CommShift.isoAdd' (_ : a + b = a + b) (commShiftIso F a) (commShiftIso F b)
[PROOFSTEP]
simp only [commShiftIso_add, CommShift.isoAdd]


[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.4486, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
⊢ ∀ ⦃X Y : D⦄ (f : X ⟶ Y),
    ((𝟭 (D ⥤ C)).obj G).map f ≫ (fun X => NatTrans.app (ihom.coev (F.obj X)) (G.obj X)) Y =
      (fun X => NatTrans.app (ihom.coev (F.obj X)) (G.obj X)) X ≫ ((tensorLeft F ⋙ closedIhom F).obj G).map f
[PROOFSTEP]
intro X Y f
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.4486, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ ((𝟭 (D ⥤ C)).obj G).map f ≫ (fun X => NatTrans.app (ihom.coev (F.obj X)) (G.obj X)) Y =
    (fun X => NatTrans.app (ihom.coev (F.obj X)) (G.obj X)) X ≫ ((tensorLeft F ⋙ closedIhom F).obj G).map f
[PROOFSTEP]
dsimp
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.4486, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ NatTrans.app (ihom.coev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.coev (F.obj X)) (G.obj X) ≫ ((closedIhom F).obj (F ⊗ G)).map f
[PROOFSTEP]
simp only [ihom.coev_naturality, closedIhom_obj_map, Monoidal.tensorObj_map]
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.4486, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ (ihom (F.obj Y)).map (𝟙 (F.obj Y) ⊗ G.map f) =
    NatTrans.app (ihom.coev (F.obj X)) (G.obj X) ≫
      NatTrans.app (pre (CategoryTheory.inv (F.map f))) ((F ⊗ G).obj X) ≫ (ihom (F.obj Y)).map (F.map f ⊗ G.map f)
[PROOFSTEP]
dsimp
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.4486, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ (ihom (F.obj Y)).map (𝟙 (F.obj Y) ⊗ G.map f) =
    NatTrans.app (ihom.coev (F.obj X)) (G.obj X) ≫
      NatTrans.app (pre (CategoryTheory.inv (F.map f))) (F.obj X ⊗ G.obj X) ≫ (ihom (F.obj Y)).map (F.map f ⊗ G.map f)
[PROOFSTEP]
rw [coev_app_comp_pre_app_assoc, ← Functor.map_comp]
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.4486, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ (ihom (F.obj Y)).map (𝟙 (F.obj Y) ⊗ G.map f) =
    NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫
      (ihom (F.obj Y)).map ((CategoryTheory.inv (F.map f) ⊗ 𝟙 (G.obj X)) ≫ (F.map f ⊗ G.map f))
[PROOFSTEP]
simp
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.13597, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
⊢ ∀ ⦃X Y : D⦄ (f : X ⟶ Y),
    ((closedIhom F ⋙ tensorLeft F).obj G).map f ≫ (fun X => NatTrans.app (ihom.ev (F.obj X)) (G.obj X)) Y =
      (fun X => NatTrans.app (ihom.ev (F.obj X)) (G.obj X)) X ≫ ((𝟭 (D ⥤ C)).obj G).map f
[PROOFSTEP]
intro X Y f
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.13597, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ ((closedIhom F ⋙ tensorLeft F).obj G).map f ≫ (fun X => NatTrans.app (ihom.ev (F.obj X)) (G.obj X)) Y =
    (fun X => NatTrans.app (ihom.ev (F.obj X)) (G.obj X)) X ≫ ((𝟭 (D ⥤ C)).obj G).map f
[PROOFSTEP]
dsimp
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.13597, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (F.map f ⊗ ((closedIhom F).obj G).map f) ≫ NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f
[PROOFSTEP]
simp only [closedIhom_obj_map, pre_comm_ihom_map]
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.13597, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (F.map f ⊗ (ihom (F.obj X)).map (G.map f) ≫ NatTrans.app (pre (CategoryTheory.inv (F.map f))) (G.obj Y)) ≫
      NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f
[PROOFSTEP]
rw [← tensor_id_comp_id_tensor, id_tensor_comp]
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.13597, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ ((F.map f ⊗ 𝟙 ((ihom (F.obj X)).obj (G.obj X))) ≫
        (𝟙 (F.obj Y) ⊗ (ihom (F.obj X)).map (G.map f)) ≫
          (𝟙 (F.obj Y) ⊗ NatTrans.app (pre (CategoryTheory.inv (F.map f))) (G.obj Y))) ≫
      NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f
[PROOFSTEP]
simp
[GOAL]
D : Type u_1
C : Type u_2
inst✝³ : Groupoid D
inst✝² : Category.{?u.29801, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
⊢ (X : D ⥤ C) → Closed X
[PROOFSTEP]
infer_instance