awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ T.map (T.forget.map (s.π.app j)) ≫ (D.obj j).a = s.pt.a ≫ T.forget.map (s.π.app j)

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

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Monad.Algebra.Hom.h, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J_1 : Type u
inst_1 : Category.{v, u} J_1
D : J_1 ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
m : s.pt ⟶ (liftedCone D c t).pt
J : ∀ (j : J_1), m ≫ (liftedCone D c t).π.app j = s.π.app j
h : m.f = Algebra.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
T : Monad.{v₁, u₁} C
J_1 : Type u
inst_1 : Category.{v, u} J_1
D : J_1 ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
m : s.pt ⟶ (liftedCone D c t).pt
J : ∀ (j : J_1), m ≫ (liftedCone D c t).π.app j = s.π.app j
h : ∀ (j : J_1), m.f ≫ c.π.app j = Algebra.Hom.f { f := t.lift (T.forget.mapCone s), h := ⋯ } ≫ c.π.app j
⊢ m.f = Algebra.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
T : Monad.{v₁, u₁} C
J_1 : Type u
inst_1 : Category.{v, u} J_1
D : J_1 ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
m : s.pt ⟶ (liftedCone D c t).pt
J : ∀ (j : J_1), m ≫ (liftedCone D c t).π.app j = s.π.app j
j : J_1
⊢ m.f ≫ c.π.app j = Algebra.Hom.f { f := t.lift (T.forget.mapCone s), h := ⋯ } ≫ c.π.app j

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

Premises used: CategoryTheory.Monad.forget, congr_arg, CategoryTheory.Monad.Algebra.Hom.f, CategoryTheory.Functor.mapCone, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
inst_2 : HasLimit (D ⋙ T.forget)
⊢ HasLimit D

Tactic:
hasLimit_of_created D (forget T)

Premises used: CategoryTheory.hasLimit_of_created, CategoryTheory.Monad.forget
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
j : J
⊢ T.map (c.ι.app j) ≫ lambda c t = (D.obj j).a ≫ c.ι.app j

Tactic:
(isColimitOfPreserves _ t).fac (newCocone c) j

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Monad.ForgetCreatesColimits.newCocone, CategoryTheory.Functor.comp, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
apply : ∀ (j : J), c.ι.app j ≫ T.η.app c.pt ≫ lambda c t = c.ι.app j ≫ 𝟙 c.pt
⊢ T.η.app c.pt ≫ lambda c t = 𝟙 c.pt

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
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
rw : c.ι.app j = c.ι.app j ≫ 𝟙 c.pt
⊢ c.ι.app j ≫ T.η.app c.pt ≫ lambda c t = c.ι.app j ≫ 𝟙 c.pt

Tactic:
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)]

Premises used: CategoryTheory.Monad.ForgetCreatesColimits.commuting, CategoryTheory.Monad.Algebra.unit_assoc, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Monad.η, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ c.ι.app j = c.ι.app j ≫ 𝟙 c.pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
⊢ T.μ.app c.pt ≫ lambda c t = T.map (lambda c t) ≫ lambda c t

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

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
rw : T.μ.app ((D ⋙ T.forget).obj j) ≫ (D.obj j).a ≫ c.ι.app j = T.map (D.obj j).a ≫ (D.obj j).a ≫ c.ι.app j
⊢ (T.mapCocone (T.mapCocone c)).ι.app j ≫ T.μ.app c.pt ≫ lambda c t =
    (T.mapCocone (T.mapCocone c)).ι.app j ≫ T.map (lambda c t) ≫ lambda c t

Tactic:
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]

Premises used: CategoryTheory.Monad.ForgetCreatesColimits.commuting, CategoryTheory.Category.assoc, CategoryTheory.Functor.mapCocone_ι_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Monad.μ, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.μ.app ((D ⋙ T.forget).obj j) ≫ (D.obj j).a ≫ c.ι.app j = T.map (D.obj j).a ≫ (D.obj j).a ≫ c.ι.app j

Tactic:
apply (D.obj j).assoc_assoc _

Premises used: CategoryTheory.Monad.Algebra.assoc_assoc, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
h :
  Eq (α := (D.obj A).A ⟶ (obj (obj (const J) (coconePoint c t)) B).A)
    (Algebra.Hom.f (D.map f ≫ { f := c.ι.app B, h := ⋯ }))
    (Algebra.Hom.f ({ f := c.ι.app A, h := ⋯ } ≫ map (obj (const J) (coconePoint c t)) f))
⊢ Eq (α := D.obj A ⟶ obj (obj (const J) (coconePoint c t)) B) (D.map f ≫ { f := c.ι.app B, h := ⋯ })
    ({ f := c.ι.app A, h := ⋯ } ≫ map (obj (const J) (coconePoint c t)) f)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
h : (D.map f).f ≫ c.ι.app B = c.ι.app A ≫ 𝟙 c.pt
⊢ Eq (α := (D.obj A).A ⟶ (obj (obj (const J) (coconePoint c t)) B).A)
    (Algebra.Hom.f (D.map f ≫ { f := c.ι.app B, h := ⋯ }))
    (Algebra.Hom.f ({ f := c.ι.app A, h := ⋯ } ≫ map (obj (const J) (coconePoint c t)) f))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
h : (D.map f).f ≫ c.ι.app B = c.ι.app A
⊢ (D.map f).f ≫ c.ι.app B = c.ι.app A ≫ 𝟙 c.pt

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ (D.map f).f ≫ c.ι.app B = c.ι.app A

Tactic:
apply c.w

Premises used: CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
dsimp :
  Eq (α := T.obj (D.obj j).A ⟶ s.pt.A)
    (T.map (c.ι.app j) ≫ T.map (t.desc (T.forget.mapCocone s)) ≫ s.pt.a : T.obj (D.obj j).A ⟶ s.pt.A)
    (T.map (c.ι.app j) ≫ lambda c t ≫ t.desc (T.forget.mapCocone s) : T.obj (D.obj j).A ⟶ s.pt.A)
⊢ Eq (α := ((D ⋙ T.forget) ⋙ T.toFunctor).obj j ⟶ s.pt.A)
    ((T.mapCocone c).ι.app j ≫ T.map (t.desc (T.forget.mapCocone s)) ≫ s.pt.a :
      ((D ⋙ T.forget) ⋙ T.toFunctor).obj j ⟶ s.pt.A)
    ((T.mapCocone c).ι.app j ≫ (liftedCocone c t).pt.a ≫ t.desc (T.forget.mapCocone s) :
      ((D ⋙ T.forget) ⋙ T.toFunctor).obj j ⟶ s.pt.A)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
rw : T.map ((T.forget.mapCocone s).ι.app j) ≫ s.pt.a = (D.obj j).a ≫ (T.forget.mapCocone s).ι.app j
⊢ Eq (α := T.obj (D.obj j).A ⟶ s.pt.A)
    (T.map (c.ι.app j) ≫ T.map (t.desc (T.forget.mapCocone s)) ≫ s.pt.a : T.obj (D.obj j).A ⟶ s.pt.A)
    (T.map (c.ι.app j) ≫ lambda c t ≫ t.desc (T.forget.mapCocone s) : T.obj (D.obj j).A ⟶ s.pt.A)

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

Premises used: CategoryTheory.Monad.ForgetCreatesColimits.commuting, CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map ((T.forget.mapCocone s).ι.app j) ≫ s.pt.a = (D.obj j).a ≫ (T.forget.mapCocone s).ι.app j

Tactic:
apply Algebra.Hom.h

Premises used: CategoryTheory.Monad.Algebra.Hom.h
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J_1 : Type u
inst_1 : Category.{v, u} J_1
D : J_1 ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
m : (liftedCocone c t).pt ⟶ s.pt
J : ∀ (j : J_1), (liftedCocone c t).ι.app j ≫ m = s.ι.app j
h : m.f = Algebra.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
T : Monad.{v₁, u₁} C
J_1 : Type u
inst_1 : Category.{v, u} J_1
D : J_1 ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
m : (liftedCocone c t).pt ⟶ s.pt
J : ∀ (j : J_1), (liftedCocone c t).ι.app j ≫ m = s.ι.app j
h : ∀ (j : J_1), c.ι.app j ≫ m.f = c.ι.app j ≫ Algebra.Hom.f { f := t.desc (T.forget.mapCocone s), h := ⋯ }
⊢ m.f = Algebra.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
T : Monad.{v₁, u₁} C
J_1 : Type u
inst_1 : Category.{v, u} J_1
D : J_1 ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
m : (liftedCocone c t).pt ⟶ s.pt
J : ∀ (j : J_1), (liftedCocone c t).ι.app j ≫ m = s.ι.app j
j : J_1
⊢ c.ι.app j ≫ m.f = c.ι.app j ≫ Algebra.Hom.f { f := t.desc (T.forget.mapCocone s), h := ⋯ }

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

Premises used: congr_arg, CategoryTheory.Monad.Algebra.Hom.f
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
c : Cocone (D ⋙ T.forget)
t : IsColimit c
A B : J
f : A ⟶ B
h :
  Eq (α := (D.obj A).A ⟶ (obj (obj (const J) (coconePoint c t)) B).A)
    (Algebra.Hom.f (D.map f ≫ { f := c.ι.app B, h := ⋯ }))
    (Algebra.Hom.f ({ f := c.ι.app A, h := ⋯ } ≫ map (obj (const J) (coconePoint c t)) f))
⊢ Eq (α := D.obj A ⟶ obj (obj (const J) (coconePoint c t)) B) (D.map f ≫ { f := c.ι.app B, h := ⋯ })
    ({ f := c.ι.app A, h := ⋯ } ≫ map (obj (const J) (coconePoint c t)) f)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Monad.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
D : J ⥤ T.Algebra
inst_2 : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst_3 : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
c : Cocone (D ⋙ T.forget)
t : IsColimit c
A B : J
f : A ⟶ B
⊢ Eq (α := (D.obj A).A ⟶ (obj (obj (const J) (coconePoint c t)) B).A)
    (Algebra.Hom.f (D.map f ≫ { f := c.ι.app B, h := ⋯ }))
    (Algebra.Hom.f ({ f := c.ι.app A, h := ⋯ } ≫ map (obj (const J) (coconePoint 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
T : Monad.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
inst_2 : PreservesColimitsOfShape.{v, u, v₁, v₁, u₁, u₁} J T.toFunctor
⊢ {K : J ⥤ T.Algebra} → CreatesColimit K T.forget

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

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

Tactic:
hasColimit_of_created D (forget T)

Premises used: CategoryTheory.Monad.forget, CategoryTheory.hasColimit_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
F : Functor.{v, v₂, u, u₂} J D
R : Functor.{v₂, v₁, u₂, u₁} D C
inst_3 : MonadicRightAdjoint R
inst_4 : HasLimit (F ⋙ R)
⊢ HasLimit
    ((F ⋙ Monad.comparison (monadicAdjunction R)) ⋙
      (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction 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 : MonadicRightAdjoint R
inst_4 : HasLimit (F ⋙ R)
⊢ HasLimit (C := (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).Algebra)
    (F ⋙ Monad.comparison (monadicAdjunction R))

Tactic:
Monad.hasLimit_of_comp_forget_hasLimit (F ⋙ Monad.comparison (monadicAdjunction R))

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Monad.comparison, CategoryTheory.Monad.hasLimit_of_comp_forget_hasLimit, CategoryTheory.monadicAdjunction
-- 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))
⊢ PreservesColimit ((K ⋙ A) ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).forget)
    (monadicLeftAdjoint R ⋙ R)

Tactic:
preservesColimit_of_iso_diagram _ i.symm

Premises used: CategoryTheory.Limits.preservesColimit_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 : 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))
⊢ PreservesColimit ((K ⋙ A) ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).forget)
    (monadicLeftAdjoint R ⋙ R)

Tactic:
exact preservesColimit_of_iso_diagram _ i.symm

Premises used: CategoryTheory.Limits.preservesColimit_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 : 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 : PreservesColimit ((K ⋙ A) ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).forget)
  (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).toFunctor :=
  ⋯
⊢ PreservesColimit
    (((K ⋙ A) ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).forget) ⋙
      monadicLeftAdjoint R ⋙ R)
    (monadicLeftAdjoint R ⋙ R)

Tactic:
preservesColimit_of_iso_diagram _ (isoWhiskerRight i (monadicLeftAdjoint R ⋙ R)).symm

Premises used: CategoryTheory.monadicLeftAdjoint, CategoryTheory.Functor.comp, CategoryTheory.Limits.preservesColimit_of_iso_diagram, CategoryTheory.Iso.symm, 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 : 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 : PreservesColimit ((K ⋙ A) ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).forget)
  (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).toFunctor :=
  ⋯
⊢ PreservesColimit
    (((K ⋙ A) ⋙ (Adjunction.toMonad (L := monadicLeftAdjoint R) (monadicAdjunction R)).forget) ⋙
      monadicLeftAdjoint R ⋙ R)
    (monadicLeftAdjoint R ⋙ R)

Tactic:
exact preservesColimit_of_iso_diagram _ (isoWhiskerRight i (monadicLeftAdjoint R ⋙ R)).symm

Premises used: CategoryTheory.monadicLeftAdjoint, CategoryTheory.Functor.comp, CategoryTheory.Limits.preservesColimit_of_iso_diagram, CategoryTheory.Iso.symm, CategoryTheory.Functor.isoWhiskerRight