Lean4
/-- (Impl)
Construct the colimiting algebra from the map `λ : TL ⟶ L` given by `lambda`. We are required to
show it satisfies the two algebra laws, which follow from the algebra laws for the image of `D` and
our `commuting` lemma.
-/
@[simps]
noncomputable def coconePoint : Algebra T where
A := c.pt
a := lambda c t
unit := by
apply t.hom_ext
intro j
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)]
simp
assoc := by
refine (isColimitOfPreserves _ (isColimitOfPreserves _ t)).hom_ext fun j => ?_
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]
apply (D.obj j).assoc_assoc _
