awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : MonadicRightAdjoint R
inst_4 : PreservesColimit (K ⋙ R) (monadicLeftAdjoint R ⋙ R)
inst_5 : PreservesColimit ((K ⋙ R) ⋙ monadicLeftAdjoint R ⋙ R) (monadicLeftAdjoint R ⋙ R)
A : D ⥤ (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).Algebra :=
  Monad.comparison (monadicAdjunction R)
B : (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).Algebra ⥤ C :=
  (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).forget
i : (K ⋙ Monad.comparison (monadicAdjunction R)) ⋙
    (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).forget ≅
  K ⋙ R :=
  K.associator (Monad.comparison (monadicAdjunction R))
      (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).forget ≪≫
    K.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction R))
this_1 : PreservesColimit ((K ⋙ A) ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).forget)
  (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).toFunctor :=
  ⋯
this_2 : PreservesColimit
  (((K ⋙ A) ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).forget) ⋙
    (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).toFunctor)
  (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).toFunctor :=
  ⋯
this_3 : CreatesColimit (K ⋙ A) B := Monad.forgetCreatesColimit (K ⋙ A)
this : CreatesColimit K (A ⋙ B) := compCreatesColimit A B
e : Monad.comparison (monadicAdjunction R) ⋙
    (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).forget ≅
  R :=
  Monad.comparisonForget (monadicAdjunction R)
⊢ CreatesColimit K R

Tactic:
apply createsColimitOfNatIso e

Premises used: CategoryTheory.createsColimitOfNatIso
-- 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
inst_3 : MonadicRightAdjoint R
inst_4 : PreservesColimitsOfShape.{v, u, v₂, v₁, u₂, u₁} J R
⊢ PreservesColimitsOfShape.{v, u, v₁, v₂, u₁, u₂} J (monadicLeftAdjoint R)

Tactic:
apply (Adjunction.leftAdjoint_preservesColimits (monadicAdjunction R)).1

Premises used: CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
-- 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
inst_3 : MonadicRightAdjoint R
inst_4 : PreservesColimitsOfShape.{v, u, v₂, v₁, u₂, u₁} J R
this : PreservesColimitsOfShape.{v, u, v₁, v₂, u₁, u₂} J (monadicLeftAdjoint R) := ⋯
⊢ PreservesColimitsOfShape.{v, u, v₁, v₁, u₁, u₁} J (monadicLeftAdjoint R ⋙ R)

Tactic:
apply CategoryTheory.Limits.comp_preservesColimitsOfShape _ _

Premises used: CategoryTheory.Limits.comp_preservesColimitsOfShape
-- 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 : HasLimit (F ⋙ R)
inst_4 : Reflective R
⊢ HasLimit F

Tactic:
haveI := monadicCreatesLimits.{v, u} R
  hasLimit_of_created F R

Premises used: CategoryTheory.hasLimit_of_created
-- 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
inst_3 : HasLimitsOfShape.{v, u, v₁, u₁} J C
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : Reflective R
⊢ HasLimitsOfShape.{v, u, v₂, u₂} J D

Tactic:
⟨fun F => hasLimit_of_reflective F R⟩

Premises used: CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.hasLimit_of_reflective
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : HasLimitsOfSize.{v, u, v₁, u₁} C
inst_3 : Reflective R
⊢ HasLimitsOfSize.{v, u, v₂, u₂} D

Tactic:
⟨fun _ => hasLimitsOfShape_of_reflective R⟩

Premises used: CategoryTheory.Limits.HasLimitsOfSize.mk, CategoryTheory.hasLimitsOfShape_of_reflective
-- 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
inst_3 : Reflective R
inst_4 : HasColimitsOfShape.{v, u, v₁, u₁} J C
F : Functor.{v, v₂, u, u₂} J D
c : Cocone ((F ⋙ R) ⋙ monadicLeftAdjoint R) := (monadicLeftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape.{v, u, v₁, v₂, u₁, u₂} J (monadicLeftAdjoint R) := ⋯
t : IsColimit c := isColimitOfPreserves (monadicLeftAdjoint R) (colimit.isColimit (F ⋙ R))
apply : (F ⋙ R) ⋙ monadicLeftAdjoint R ≅ F
⊢ HasColimit F

Tactic:
apply HasColimit.mk ⟨_, (IsColimit.precomposeInvEquiv _ _).symm t⟩

Premises used: CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeInvEquiv
-- 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
inst_3 : Reflective R
inst_4 : HasColimitsOfShape.{v, u, v₁, u₁} J C
F : Functor.{v, v₂, u, u₂} J D
c : Cocone ((F ⋙ R) ⋙ monadicLeftAdjoint R) := (monadicLeftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape.{v, u, v₁, v₂, u₁, u₂} J (monadicLeftAdjoint R) := ⋯
t : IsColimit c := isColimitOfPreserves (monadicLeftAdjoint R) (colimit.isColimit (F ⋙ R))
⊢ (F ⋙ R) ⋙ monadicLeftAdjoint R ≅ F

Tactic:
apply
        (isoWhiskerLeft F (asIso (monadicAdjunction R).counit) :) ≪≫ F.rightUnitor

Premises used: CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Adjunction.counit, CategoryTheory.monadicAdjunction, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
inst_3 : HasColimitsOfSize.{v, u, v₁, u₁} C
⊢ HasColimitsOfSize.{v, u, v₂, u₂} D

Tactic:
⟨fun _ => hasColimitsOfShape_of_reflective R⟩

Premises used: CategoryTheory.hasColimitsOfShape_of_reflective, CategoryTheory.Limits.HasColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
preserves : ∀ {c : Cone (F ⋙ R)} (hc : IsLimit c), Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))
⊢ PreservesLimit (F ⋙ R) (monadicLeftAdjoint R)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
⊢ HasLimit (F ⋙ R)

Tactic:
haveI : HasLimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
this : HasLimit (F ⋙ R)
⊢ HasLimit F

Tactic:
haveI : HasLimit F := hasLimit_of_reflective F R
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
this_1 : HasLimit (F ⋙ R)
this : HasLimit F
preserves : IsLimit ((monadicLeftAdjoint R).mapCone c)
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
this_1 : HasLimit (F ⋙ R)
this : HasLimit F
preserves : (limit.cone F).pt ≅ ((monadicLeftAdjoint R).mapCone c).pt
⊢ IsLimit ((monadicLeftAdjoint R).mapCone c)

Tactic:
apply isLimitChangeEmptyCone D (limit.isLimit F)

Premises used: CategoryTheory.Limits.isLimitChangeEmptyCone, CategoryTheory.Limits.limit.isLimit
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
this_1 : HasLimit (F ⋙ R)
this : HasLimit F
preserves : (R ⋙ monadicLeftAdjoint R).obj (limit.cone F).1 ≅ ((monadicLeftAdjoint R).mapCone c).pt
⊢ (limit.cone F).pt ≅ ((monadicLeftAdjoint R).mapCone c).pt

Tactic:
apply (asIso ((monadicAdjunction R).counit.app _)).symm.trans

Premises used: CategoryTheory.Adjunction.counit, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.monadicAdjunction, CategoryTheory.NatTrans.app, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
this_1 : HasLimit (F ⋙ R)
this : HasLimit F
preserves : R.obj (limit.cone F).1 ≅ c.pt
⊢ (R ⋙ monadicLeftAdjoint R).obj (limit.cone F).1 ≅ ((monadicLeftAdjoint R).mapCone c).pt

Tactic:
apply (monadicLeftAdjoint R).mapIso

Premises used: CategoryTheory.monadicLeftAdjoint, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
this_1 : HasLimit (F ⋙ R)
this_2 : HasLimit F
this : CreatesLimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := monadicCreatesLimits R
A : PreservesLimit F R := ⋯
⊢ R.obj (limit.cone F).1 ≅ c.pt

Tactic:
apply (isLimitOfPreserves _ (limit.isLimit F)).conePointUniqueUpToIso h

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : Reflective R
K : Functor.{v, v₁, v, u₁} (Discrete PEmpty.{v + 1}) C
F : Functor.{v, v₂, v, u₂} (Discrete PEmpty.{v + 1}) D := empty D
this : PreservesLimit (F ⋙ R) (monadicLeftAdjoint R) := ⋯
⊢ PreservesLimit K (monadicLeftAdjoint R)

Tactic:
apply preservesLimit_of_iso_diagram _ (Functor.emptyExt (F ⋙ R) _)

Premises used: CategoryTheory.Functor.emptyExt, CategoryTheory.Functor.comp, CategoryTheory.Limits.preservesLimit_of_iso_diagram
-- 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 : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
simp : (D.obj j).a ≫ T.ε.app (D.obj j).A ≫ c.ι.app j = c.ι.app j
⊢ c.ι.app j ≫
      CategoryStruct.comp (Y := T.obj c.pt) (t.desc (newCocone D c) : c.pt ⟶ (newCocone D c).pt) (T.ε.app c.pt) =
    c.ι.app j ≫ 𝟙 c.pt

Tactic:
simp only [Functor.comp_obj, forget_obj, Functor.id_obj, Functor.const_obj_obj,
      IsColimit.fac_assoc, newCocone_ι_app, assoc, NatTrans.naturality, Functor.id_map, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone_ι_app, CategoryTheory.Functor.id_map, CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.id_obj, CategoryTheory.Comonad.forget_obj, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Limits.IsColimit.fac_assoc
-- 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 : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
rw : ((D.obj j).a ≫ T.ε.app (D.obj j).A) ≫ c.ι.app j = c.ι.app j
rw₁ : 𝟙 (D.obj j).A ≫ c.ι.app j = c.ι.app j
rw₂ rw₃ : c.ι.app j = c.ι.app j
⊢ (D.obj j).a ≫ T.ε.app (D.obj j).A ≫ c.ι.app j = c.ι.app j

Tactic:
rw [← Category.assoc, (D.obj j).counit, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Comonad.Coalgebra.counit, CategoryTheory.Functor.obj, 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 : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
simp :
  (D.obj j).a ≫ T.δ.app (D.obj j).A ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (c.ι.app j) ≫ T.map (t.desc (newCocone D c))
⊢ Eq (α := (D ⋙ T.forget).obj j ⟶ (T.toFunctor ⋙ T.toFunctor).obj c.pt)
    (c.ι.app j ≫
      CategoryStruct.comp (Y := T.obj c.pt) (t.desc (newCocone D c) : c.pt ⟶ (newCocone D c).pt) (T.δ.app c.pt))
    (c.ι.app j ≫
      CategoryStruct.comp (Y := T.obj c.pt) (t.desc (newCocone D c) : c.pt ⟶ (newCocone D c).pt)
        (T.map (t.desc (newCocone D c))))

Tactic:
simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, IsColimit.fac_assoc,
      newCocone_ι_app, assoc, NatTrans.naturality, Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone_ι_app, CategoryTheory.NatTrans.naturality, CategoryTheory.Comonad.forget_obj, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Limits.IsColimit.fac_assoc, CategoryTheory.Functor.comp_map
-- 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 : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
rw :
  ((D.obj j).a ≫ T.δ.app (D.obj j).A) ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (c.ι.app j) ≫ T.map (t.desc (newCocone D c))
rw₁ :
  ((D.obj j).a ≫ T.map (D.obj j).a) ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (c.ι.app j) ≫ T.map (t.desc (newCocone D c))
rw₂ :
  ((D.obj j).a ≫ T.map (D.obj j).a) ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (c.ι.app j ≫ t.desc (newCocone D c))
rw₃ : ((D.obj j).a ≫ T.map (D.obj j).a) ≫ T.map (T.map (c.ι.app j)) = (D.obj j).a ≫ T.map ((newCocone D c).ι.app j)
rw₄ :
  ((D.obj j).a ≫ T.map (D.obj j).a) ≫ T.map (T.map (c.ι.app j)) = (D.obj j).a ≫ T.map ((D.obj j).a ≫ T.map (c.ι.app j))
rw₅ :
  ((D.obj j).a ≫ T.map (D.obj j).a) ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (D.obj j).a ≫ T.map (T.map (c.ι.app j))
rw₆ rw₇ :
  (D.obj j).a ≫ T.map (D.obj j).a ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (D.obj j).a ≫ T.map (T.map (c.ι.app j))
⊢ (D.obj j).a ≫ T.δ.app (D.obj j).A ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (c.ι.app j) ≫ T.map (t.desc (newCocone D c))

Tactic:
rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j,
      newCocone_ι_app, Functor.map_comp, assoc]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone_ι_app, CategoryTheory.Comonad.Coalgebra.coassoc, CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone, CategoryTheory.Functor.map_comp, 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 : Cocone (D ⋙ T.forget)
t : IsColimit c
X Y : J
f : X ⟶ Y
h :
  Eq (α := (D.obj X).A ⟶ (obj (obj (const J) (coconePoint D c t)) Y).A)
    (Coalgebra.Hom.f (D.map f ≫ { f := c.ι.app Y, h := ⋯ }))
    (Coalgebra.Hom.f ({ f := c.ι.app X, h := ⋯ } ≫ map (obj (const J) (coconePoint D c t)) f))
⊢ Eq (α := D.obj X ⟶ obj (obj (const J) (coconePoint D c t)) Y) (D.map f ≫ { f := c.ι.app Y, h := ⋯ })
    ({ f := c.ι.app X, h := ⋯ } ≫ map (obj (const J) (coconePoint D c t)) 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 : Cocone (D ⋙ T.forget)
t : IsColimit c
X Y : J
f : X ⟶ Y
⊢ Eq (α := (D.obj X).A ⟶ (obj (obj (const J) (coconePoint D c t)) Y).A)
    (Coalgebra.Hom.f (D.map f ≫ { f := c.ι.app Y, h := ⋯ }))
    (Coalgebra.Hom.f ({ f := c.ι.app X, h := ⋯ } ≫ map (obj (const J) (coconePoint D c t)) f))

Tactic:
simpa using (c.w f)

Premises used: CategoryTheory.Limits.Cocone.w
-- 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 : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
dsimp :
  Eq (α := (D.obj j).A ⟶ T.obj s.pt.A)
    (c.ι.app j ≫
      CategoryStruct.comp (Y := T.obj c.pt) (t.desc (newCocone D c) : c.pt ⟶ (newCocone D c).pt)
        (T.map (t.desc (T.forget.mapCocone s))))
    (c.ι.app j ≫ t.desc (T.forget.mapCocone s) ≫ s.pt.a)
⊢ Eq (α := (D ⋙ T.forget).obj j ⟶ T.obj s.pt.A)
    (c.ι.app j ≫ (liftedCocone D c t).pt.a ≫ T.map (t.desc (T.forget.mapCocone s)) :
      (D ⋙ T.forget).obj j ⟶ T.obj s.pt.A)
    (c.ι.app j ≫ t.desc (T.forget.mapCocone s) ≫ s.pt.a : (D ⋙ T.forget).obj j ⟶ T.obj s.pt.A)

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 : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
rw : (D.obj j).a ≫ T.map ((T.forget.mapCocone s).ι.app j) = T.forget.map (s.ι.app j) ≫ s.pt.a
⊢ Eq (α := (D.obj j).A ⟶ T.obj s.pt.A)
    (c.ι.app j ≫
      CategoryStruct.comp (Y := T.obj c.pt) (t.desc (newCocone D c) : c.pt ⟶ (newCocone D c).pt)
        (T.map (t.desc (T.forget.mapCocone s))))
    (c.ι.app j ≫ t.desc (T.forget.mapCocone s) ≫ s.pt.a)

Tactic:
rw [← Category.assoc, ← Category.assoc, t.fac, newCocone_ι_app, t.fac,
            Functor.mapCocone_ι_app, Category.assoc, ← Functor.map_comp, t.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, CategoryTheory.Functor.mapCocone_ι_app, CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone_ι_app, CategoryTheory.Functor.map_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 : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ (D.obj j).a ≫ T.map ((T.forget.mapCocone s).ι.app j) = T.forget.map (s.ι.app j) ≫ s.pt.a

Tactic:
apply (s.ι.app j).h

Premises used: CategoryTheory.Comonad.Coalgebra.Hom.h, CategoryTheory.Limits.Cocone.ι, 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 : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
m : (liftedCocone D c t).pt ⟶ s.pt
J : ∀ (j : J_1), (liftedCocone D c t).ι.app j ≫ m = s.ι.app j
h : m.f = Coalgebra.Hom.f { f := t.desc (T.forget.mapCocone s), h := ⋯ }
⊢ m = { f := t.desc (T.forget.mapCocone 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 : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
m : (liftedCocone D c t).pt ⟶ s.pt
J : ∀ (j : J_1), (liftedCocone D c t).ι.app j ≫ m = s.ι.app j
h : ∀ (j : J_1), c.ι.app j ≫ m.f = c.ι.app j ≫ Coalgebra.Hom.f { f := t.desc (T.forget.mapCocone s), h := ⋯ }
⊢ m.f = Coalgebra.Hom.f { f := t.desc (T.forget.mapCocone s), h := ⋯ }

Tactic:
apply t.hom_ext

Premises used: CategoryTheory.Limits.IsColimit.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 : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
m : (liftedCocone D c t).pt ⟶ s.pt
J : ∀ (j : J_1), (liftedCocone D c t).ι.app j ≫ m = s.ι.app j
j : J_1
⊢ c.ι.app j ≫ m.f = c.ι.app j ≫ Coalgebra.Hom.f { f := t.desc (T.forget.mapCocone s), h := ⋯ }

Tactic:
simpa [t.fac ((forget T).mapCocone s) j] using congr_arg Coalgebra.Hom.f (J j)

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.mapCocone, CategoryTheory.Comonad.forget, CategoryTheory.Comonad.Coalgebra.Hom.f, congr_arg
-- 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
D : J ⥤ T.Coalgebra
inst_2 : HasColimit (D ⋙ T.forget)
⊢ HasColimit D

Tactic:
hasColimit_of_created D (forget T)

Premises used: CategoryTheory.Comonad.forget, CategoryTheory.hasColimit_of_created
-- 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
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst_2 : PreservesLimit (D ⋙ T.forget) T.toFunctor
j : J
⊢ lambda c t ≫ T.map (c.π.app j) = c.π.app j ≫ (D.obj j).a

Tactic:
(isLimitOfPreserves _ t).fac (newCone c) j

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Comonad.ForgetCreatesLimits'.newCone, CategoryTheory.Limits.isLimitOfPreserves, 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
j : J
rw : c.π.app j ≫ (D.obj j).a ≫ T.ε.app (T.forget.obj (D.obj j)) = 𝟙 c.pt ≫ c.π.app j
⊢ (lambda c t ≫ T.ε.app c.pt) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j

Tactic:
rw [assoc, ← show _ = _ ≫ c.π.app j from T.ε.naturality _, ← assoc, commuting, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cone.π, CategoryTheory.Comonad.ε, CategoryTheory.NatTrans.naturality, CategoryTheory.Comonad.ForgetCreatesLimits'.commuting, CategoryTheory.NatTrans.app