Lean4
/-- If the right extension defined by `α : F₀ ⟶ L ⋙ F₁` is universal,
then for every `L' : D ⥤ D'`, `F₁ : D ⥤ H`, if an extension
`b : L'.LeftExtension F₁` is universal, so is the "pasted" extension
`(LeftExtension.precomp₂ L' α).obj b`. -/
def isUniversalPrecomp₂ (hα : (LeftExtension.mk F₁ α).IsUniversal) {b : L'.LeftExtension F₁} (hb : b.IsUniversal) :
((LeftExtension.precomp₂ L' α).obj b).IsUniversal :=
by
letI (y : (L ⋙ L').LeftExtension F₀) : Unique ((precomp₂ L' α).obj b ⟶ y) :=
by
let u : L'.LeftExtension F₁ := mk y.right <| hα.desc <| LeftExtension.mk _ <| y.hom ≫ (L.associator L' y.right).hom
refine
⟨⟨StructuredArrow.homMk (hb.desc u) <| by
ext x
haveI hb_fac_app := congr_app (hb.fac u) (L.obj x)
haveI hα_fac_app := congr_app (hα.fac <| LeftExtension.mk _ <| y.hom ≫ (L.associator L' y.right).hom) x
dsimp at hα_fac_app hb_fac_app
simp [hb_fac_app, u, hα_fac_app]⟩,
fun a => ?_⟩
dsimp
ext1
apply hb.hom_ext
apply hα.hom_ext
ext t
dsimp
have a_w_t := congr_app a.w t
have hb_fac_app := congr_app (hb.fac u) (L.obj t)
have hα_fac_app := congr_app (hα.fac <| LeftExtension.mk _ <| y.hom ≫ (L.associator L' y.right).hom) t
dsimp at hb_fac_app hα_fac_app
simp only [precomp₂_obj_left, const_obj_obj, whiskeringLeft_obj_obj, comp_obj, StructuredArrow.left_eq_id,
const_obj_map, id_comp, precomp₂_obj_right, whiskeringLeft_obj_map, NatTrans.comp_app, precomp₂_obj_hom_app,
whiskerLeft_app, assoc] at a_w_t
simp [← a_w_t, hb_fac_app, u, hα_fac_app]
apply IsInitial.ofUnique
