awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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 ≫ 𝟙 c.pt
have h : (D.map f).f ≫ c.ι.app B = c.ι.app A
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ 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)
have rw : T.map ((T.forget.mapCocone s).ι.app j) ≫ s.pt.a = (D.obj j).a ≫ (T.forget.mapCocone s).ι.app j
Tactic: rw [← Functor.map_comp_assoc, ← Category.assoc, t.fac, commuting, Category.assoc, t.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ m = { f := t.desc (T.forget.mapCocone s), h := ⋯ }
have h : m.f = Algebra.Hom.f { f := t.desc (T.forget.mapCocone s), h := sorry }
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ m.f = Algebra.Hom.f { f := t.desc (T.forget.mapCocone s), h := ⋯ }
have h : ∀ (j : J_1), c.ι.app j ≫ m.f = c.ι.app j ≫ Algebra.Hom.f { f := t.desc (T.forget.mapCocone s), h := sorry }
Tactic: apply t.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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 ⟶ 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)
have 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 := sorry }))
  (Algebra.Hom.f ({ f := c.ι.app A, h := sorry } ≫ map (obj (const J) (coconePoint c t)) f))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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))
⊢ HasColimit F
have apply : (F ⋙ R) ⋙ monadicLeftAdjoint R ≅ F
Tactic: apply HasColimit.mk ⟨_, (IsColimit.precomposeInvEquiv _ _).symm t⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ PreservesLimit (F ⋙ R) (monadicLeftAdjoint R)
have preserves : ∀ {c : Cone (F ⋙ R)} (hc : IsLimit c), Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (hypothesis)
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
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))
have this : HasLimit (F ⋙ R)
Tactic: haveI : HasLimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (hypothesis)
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)
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))
have this₁ : HasLimit F
Tactic: haveI : HasLimit F := hasLimit_of_reflective F R
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))
have preserves : IsLimit ((monadicLeftAdjoint R).mapCone c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ IsLimit ((monadicLeftAdjoint R).mapCone c)
have preserves : (limit.cone F).pt ≅ ((monadicLeftAdjoint R).mapCone c).pt
Tactic: apply isLimitChangeEmptyCone D (limit.isLimit F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ (limit.cone F).pt ≅ ((monadicLeftAdjoint R).mapCone c).pt
have preserves : (R ⋙ monadicLeftAdjoint R).obj (limit.cone F).1 ≅ ((monadicLeftAdjoint R).mapCone c).pt
Tactic: apply (asIso ((monadicAdjunction R).counit.app _)).symm.trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ (R ⋙ monadicLeftAdjoint R).obj (limit.cone F).1 ≅ ((monadicLeftAdjoint R).mapCone c).pt
have preserves : R.obj (limit.cone F).1 ≅ c.pt
Tactic: apply (monadicLeftAdjoint R).mapIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ 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
have simp : (D.obj j).a ≫ T.ε.app (D.obj j).A ≫ c.ι.app j = c.ι.app j
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ (D.obj j).a ≫ T.ε.app (D.obj j).A ≫ c.ι.app j = c.ι.app j
have rw : ((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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ (D.obj j).a ≫ T.ε.app (D.obj j).A ≫ c.ι.app j = c.ι.app j
have rw₁ : 𝟙 (D.obj j).A ≫ c.ι.app j = c.ι.app j
Tactic: rw [← Category.assoc, (D.obj j).counit, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ (D.obj j).a ≫ T.ε.app (D.obj j).A ≫ c.ι.app j = c.ι.app j
have rw₂ : c.ι.app j = c.ι.app j
Tactic: rw [← Category.assoc, (D.obj j).counit, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ 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))))
have 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))
Tactic: simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, IsColimit.fac_assoc,
      newCocone_ι_app, assoc, NatTrans.naturality, Functor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ (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))
have 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))
Tactic: rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j,
      newCocone_ι_app, Functor.map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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))
⊢ (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))
have 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))
Tactic: rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j,
      newCocone_ι_app, Functor.map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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))
⊢ (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))
have 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))
Tactic: rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j,
      newCocone_ι_app, Functor.map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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))
⊢ (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))
have 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)
Tactic: rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j,
      newCocone_ι_app, Functor.map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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)
⊢ (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))
have 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))
Tactic: rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j,
      newCocone_ι_app, Functor.map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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))
⊢ (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))
have 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))
Tactic: rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j,
      newCocone_ι_app, Functor.map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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))
⊢ (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))
have 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))
Tactic: rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j,
      newCocone_ι_app, Functor.map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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 ⟶ 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)
have 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 := sorry }))
  (Coalgebra.Hom.f ({ f := c.ι.app X, h := sorry } ≫ map (obj (const J) (coconePoint D c t)) f))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ 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)
have rw : (D.obj j).a ≫ T.map ((T.forget.mapCocone s).ι.app j) = T.forget.map (s.ι.app j) ≫ 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ m = { f := t.desc (T.forget.mapCocone s), h := ⋯ }
have h : m.f = Coalgebra.Hom.f { f := t.desc (T.forget.mapCocone s), h := sorry }
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ m.f = Coalgebra.Hom.f { f := t.desc (T.forget.mapCocone s), h := ⋯ }
have h : ∀ (j : J_1), c.ι.app j ≫ m.f = c.ι.app j ≫ Coalgebra.Hom.f { f := t.desc (T.forget.mapCocone s), h := sorry }
Tactic: apply t.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monad.Limits (goal)
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
⊢ (lambda c t ≫ T.ε.app c.pt) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j
have rw : c.π.app j ≫ (D.obj j).a ≫ T.ε.app (T.forget.obj (D.obj j)) = 𝟙 c.pt ≫ c.π.app j
Tactic: rw [assoc, ← show _ = _ ≫ c.π.app j from T.ε.naturality _, ← assoc, commuting, assoc]