awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ c.π.app j ≫ (D.obj j).a ≫ T.ε.app (T.forget.obj (D.obj j)) = 𝟙 c.pt ≫ c.π.app j

Tactic:
simp [Coalgebra.counit (D.obj j)]

Premises used: CategoryTheory.Comonad.Coalgebra.counit, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
⊢ lambda c t ≫ T.δ.app c.pt = lambda c t ≫ T.map (lambda c t)

Tactic:
(isLimitOfPreserves _ (isLimitOfPreserves _ t)).hom_ext fun j => ?_

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
refine :
  ∀ (j : J),
    (lambda c t ≫ T.δ.app c.pt) ≫ (T.mapCone (T.mapCone c)).π.app j =
      (lambda c t ≫ T.map (lambda c t)) ≫ (T.mapCone (T.mapCone c)).π.app j
⊢ lambda c t ≫ T.δ.app c.pt = lambda c t ≫ T.map (lambda c t)

Tactic:
refine (isLimitOfPreserves _ (isLimitOfPreserves _ t)).hom_ext fun j => ?_

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
rw : (c.π.app j ≫ (D.obj j).a) ≫ T.δ.app ((D ⋙ T.forget).obj j) = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
⊢ (lambda c t ≫ T.δ.app c.pt) ≫ (T.mapCone (T.mapCone c)).π.app j =
    (lambda c t ≫ T.map (lambda c t)) ≫ (T.mapCone (T.mapCone c)).π.app j

Tactic:
rw [Functor.mapCone_π_app, Functor.mapCone_π_app, assoc,
      ← show _ = _ ≫ T.map (T.map _) from T.δ.naturality _, assoc, ← Functor.map_comp, commuting,
      Functor.map_comp, ← assoc, commuting]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Comonad.δ, CategoryTheory.Functor.mapCone_π_app, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Comonad.ForgetCreatesLimits'.commuting
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
simp : c.π.app j ≫ (D.obj j).a ≫ T.δ.app (D.obj j).A = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
⊢ (c.π.app j ≫ (D.obj j).a) ≫ T.δ.app ((D ⋙ T.forget).obj j) = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a

Tactic:
simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Comonad.forget_obj, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
rw : c.π.app j ≫ (D.obj j).a ≫ T.map (D.obj j).a = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
rw₁ : (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
rw₂ : (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a = (lambda c t ≫ T.map (c.π.app j)) ≫ T.map (D.obj j).a
rw₃ rw₄ : (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a = (c.π.app j ≫ (D.obj j).a) ≫ T.map (D.obj j).a
⊢ c.π.app j ≫ (D.obj j).a ≫ T.δ.app (D.obj j).A = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a

Tactic:
rw [(D.obj j).coassoc, ← assoc, ← assoc, commuting]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Comonad.Coalgebra.coassoc, CategoryTheory.Comonad.ForgetCreatesLimits'.commuting, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
h :
  Eq (α := (obj (obj (const J) (conePoint c t)) A).A ⟶ (D.obj B).A)
    (Coalgebra.Hom.f (map (obj (const J) (conePoint c t)) f ≫ { f := c.π.app B, h := ⋯ }))
    (Coalgebra.Hom.f ({ f := c.π.app A, h := ⋯ } ≫ D.map f))
⊢ Eq (α := obj (obj (const J) (conePoint c t)) A ⟶ D.obj B)
    (map (obj (const J) (conePoint c t)) f ≫ { f := c.π.app B, h := ⋯ }) ({ f := c.π.app A, h := ⋯ } ≫ D.map f)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
h : 𝟙 c.pt ≫ c.π.app B = c.π.app A ≫ (D.map f).f
⊢ Eq (α := (obj (obj (const J) (conePoint c t)) A).A ⟶ (D.obj B).A)
    (Coalgebra.Hom.f (map (obj (const J) (conePoint c t)) f ≫ { f := c.π.app B, h := ⋯ }))
    (Coalgebra.Hom.f ({ f := c.π.app A, h := ⋯ } ≫ D.map f))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
h : c.π.app A ≫ (D ⋙ T.forget).map f = c.π.app A ≫ (D.map f).f
h₁ : A ⟶ B
rw : J
⊢ 𝟙 c.pt ≫ c.π.app B = c.π.app A ≫ (D.map f).f

Tactic:
rw [id_comp, ← c.w]

Premises used: CategoryTheory.Limits.Cone.w, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
dsimp :
  (s.pt.a ≫ T.map (t.lift (T.forget.mapCone s))) ≫ T.map (c.π.app j) =
    (t.lift (T.forget.mapCone s) ≫ lambda c t) ≫ T.map (c.π.app j)
⊢ (s.pt.a ≫ T.map (t.lift (T.forget.mapCone s))) ≫ (T.mapCone c).π.app j =
    (t.lift (T.forget.mapCone s) ≫ (liftedCone c t).pt.a) ≫ (T.mapCone c).π.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
rw : s.pt.a ≫ T.map ((T.forget.mapCone s).π.app j) = (T.forget.mapCone s).π.app j ≫ (D.obj j).a
⊢ (s.pt.a ≫ T.map (t.lift (T.forget.mapCone s))) ≫ T.map (c.π.app j) =
    (t.lift (T.forget.mapCone s) ≫ lambda c t) ≫ T.map (c.π.app j)

Tactic:
rw [Category.assoc, ← t.fac, Category.assoc, t.fac, commuting, ← assoc, ← assoc, t.fac,
            assoc, ← Functor.map_comp, t.fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Comonad.ForgetCreatesLimits'.commuting, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ s.pt.a ≫ T.map ((T.forget.mapCone s).π.app j) = (T.forget.mapCone s).π.app j ≫ (D.obj j).a

Tactic:
(s.π.app j).h

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Comonad.Coalgebra.Hom.h, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ s.pt.a ≫ T.map ((T.forget.mapCone s).π.app j) = (T.forget.mapCone s).π.app j ≫ (D.obj j).a

Tactic:
exact (s.π.app j).h

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Comonad.Coalgebra.Hom.h, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J_1 : Type u
inst_2 : Category.{v, u} J_1
T : Comonad.{v₁, u₁} C
D : J_1 ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
m : s.pt ⟶ (liftedCone c t).pt
J : ∀ (j : J_1), m ≫ (liftedCone c t).π.app j = s.π.app j
h : m.f = Coalgebra.Hom.f { f := t.lift (T.forget.mapCone s), h := ⋯ }
⊢ m = { f := t.lift (T.forget.mapCone s), h := ⋯ }

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J_1 : Type u
inst_2 : Category.{v, u} J_1
T : Comonad.{v₁, u₁} C
D : J_1 ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
m : s.pt ⟶ (liftedCone c t).pt
J : ∀ (j : J_1), m ≫ (liftedCone c t).π.app j = s.π.app j
h : ∀ (j : J_1), m.f ≫ c.π.app j = Coalgebra.Hom.f { f := t.lift (T.forget.mapCone s), h := ⋯ } ≫ c.π.app j
⊢ m.f = Coalgebra.Hom.f { f := t.lift (T.forget.mapCone s), h := ⋯ }

Tactic:
apply t.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J_1 : Type u
inst_2 : Category.{v, u} J_1
T : Comonad.{v₁, u₁} C
D : J_1 ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst_5 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
m : s.pt ⟶ (liftedCone c t).pt
J : ∀ (j : J_1), m ≫ (liftedCone c t).π.app j = s.π.app j
j : J_1
⊢ m.f ≫ c.π.app j = Coalgebra.Hom.f { f := t.lift (T.forget.mapCone s), h := ⋯ } ≫ c.π.app j

Tactic:
simpa using congr_arg Coalgebra.Hom.f (J j)

Premises used: CategoryTheory.Comonad.Coalgebra.Hom.f, congr_arg
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
c : Cone (D ⋙ T.forget)
t : IsLimit c
A B : J
f : A ⟶ B
h :
  Eq (α := (obj (obj (const J) (conePoint c t)) A).A ⟶ (D.obj B).A)
    (Coalgebra.Hom.f (map (obj (const J) (conePoint c t)) f ≫ { f := c.π.app B, h := ⋯ }))
    (Coalgebra.Hom.f ({ f := c.π.app A, h := ⋯ } ≫ D.map f))
⊢ Eq (α := obj (obj (const J) (conePoint c t)) A ⟶ D.obj B)
    (map (obj (const J) (conePoint c t)) f ≫ { f := c.π.app B, h := ⋯ }) ({ f := c.π.app A, h := ⋯ } ≫ D.map f)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
D : J ⥤ T.Coalgebra
inst_3 : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst_4 : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
c : Cone (D ⋙ T.forget)
t : IsLimit c
A B : J
f : A ⟶ B
⊢ Eq (α := (obj (obj (const J) (conePoint c t)) A).A ⟶ (D.obj B).A)
    (Coalgebra.Hom.f (map (obj (const J) (conePoint c t)) f ≫ { f := c.π.app B, h := ⋯ }))
    (Coalgebra.Hom.f ({ f := c.π.app A, h := ⋯ } ≫ D.map f))

Tactic:
simpa using (c.w f).symm

Premises used: CategoryTheory.Limits.Cone.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape.{v, u, v₁, v₁, u₁, u₁} J T.toFunctor
⊢ {K : J ⥤ T.Coalgebra} → CreatesLimit K T.forget

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
inst_3 : PreservesLimitsOfSize.{v, u, v₁, v₁, u₁, u₁} T.toFunctor
⊢ {J : Type u} → [inst_4 : Category.{v, u} J] → CreatesLimitsOfShape J T.forget

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
T : Comonad.{v₁, u₁} C
inst_2 : PreservesLimitsOfShape.{v, u, v₁, v₁, u₁, u₁} J T.toFunctor
D : J ⥤ T.Coalgebra
inst_3 : HasLimit (D ⋙ T.forget)
⊢ HasLimit D

Tactic:
hasLimit_of_created D (forget T)

Premises used: CategoryTheory.hasLimit_of_created, CategoryTheory.Comonad.forget
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
F : Functor.{v, v₂, u, u₂} J D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : ComonadicLeftAdjoint R
inst_4 : HasColimit (F ⋙ R)
⊢ HasColimit
    ((F ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙
      (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget)

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
F : Functor.{v, v₂, u, u₂} J D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : ComonadicLeftAdjoint R
inst_4 : HasColimit (F ⋙ R)
⊢ HasColimit (C := (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).Coalgebra)
    (F ⋙ Comonad.comparison (comonadicAdjunction R))

Tactic:
Comonad.hasColimit_of_comp_forget_hasColimit (F ⋙ Comonad.comparison (comonadicAdjunction R))

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Comonad.comparison, CategoryTheory.comonadicAdjunction, CategoryTheory.Comonad.hasColimit_of_comp_forget_hasColimit
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
R : Functor.{v₂, v₁, u₂, u₁} D C
K : Functor.{v, v₂, u, u₂} J D
inst_3 : ComonadicLeftAdjoint R
inst_4 : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst_5 : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).Coalgebra :=
  Comonad.comparison (comonadicAdjunction R)
B : (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).Coalgebra ⥤ C :=
  (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget
i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙
    (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget ≅
  K ⋙ R :=
  K.associator (Comonad.comparison (comonadicAdjunction R))
      (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget ≪≫
    K.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction R))
⊢ PreservesLimit ((K ⋙ A) ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget)
    (comonadicRightAdjoint R ⋙ R)

Tactic:
preservesLimit_of_iso_diagram _ i.symm

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
R : Functor.{v₂, v₁, u₂, u₁} D C
K : Functor.{v, v₂, u, u₂} J D
inst_3 : ComonadicLeftAdjoint R
inst_4 : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst_5 : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).Coalgebra :=
  Comonad.comparison (comonadicAdjunction R)
B : (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).Coalgebra ⥤ C :=
  (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget
i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙
    (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget ≅
  K ⋙ R :=
  K.associator (Comonad.comparison (comonadicAdjunction R))
      (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget ≪≫
    K.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction R))
⊢ PreservesLimit ((K ⋙ A) ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget)
    (comonadicRightAdjoint R ⋙ R)

Tactic:
exact preservesLimit_of_iso_diagram _ i.symm

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
R : Functor.{v₂, v₁, u₂, u₁} D C
K : Functor.{v, v₂, u, u₂} J D
inst_3 : ComonadicLeftAdjoint R
inst_4 : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst_5 : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).Coalgebra :=
  Comonad.comparison (comonadicAdjunction R)
B : (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).Coalgebra ⥤ C :=
  (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget
i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙
    (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget ≅
  K ⋙ R :=
  K.associator (Comonad.comparison (comonadicAdjunction R))
      (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget ≪≫
    K.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction R))
this : PreservesLimit ((K ⋙ A) ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget)
  (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).toFunctor :=
  ⋯
⊢ PreservesLimit
    (((K ⋙ A) ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget) ⋙
      comonadicRightAdjoint R ⋙ R)
    (comonadicRightAdjoint R ⋙ R)

Tactic:
preservesLimit_of_iso_diagram _ (isoWhiskerRight i (comonadicRightAdjoint R ⋙ R)).symm

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Iso.symm, CategoryTheory.comonadicRightAdjoint, CategoryTheory.Functor.isoWhiskerRight
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u
inst_2 : Category.{v, u} J
R : Functor.{v₂, v₁, u₂, u₁} D C
K : Functor.{v, v₂, u, u₂} J D
inst_3 : ComonadicLeftAdjoint R
inst_4 : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst_5 : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).Coalgebra :=
  Comonad.comparison (comonadicAdjunction R)
B : (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).Coalgebra ⥤ C :=
  (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget
i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙
    (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget ≅
  K ⋙ R :=
  K.associator (Comonad.comparison (comonadicAdjunction R))
      (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget ≪≫
    K.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction R))
this : PreservesLimit ((K ⋙ A) ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget)
  (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).toFunctor :=
  ⋯
⊢ PreservesLimit
    (((K ⋙ A) ⋙ (Adjunction.toComonad (R := comonadicRightAdjoint R) (comonadicAdjunction R)).forget) ⋙
      comonadicRightAdjoint R ⋙ R)
    (comonadicRightAdjoint R ⋙ R)

Tactic:
exact preservesLimit_of_iso_diagram _ (isoWhiskerRight i (comonadicRightAdjoint R ⋙ R)).symm

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Iso.symm, CategoryTheory.comonadicRightAdjoint, CategoryTheory.Functor.isoWhiskerRight