Lean4
/-- `F ⋙ uliftYoneda` is naturally isomorphic to `uliftYoneda ⋙ F.op.lan`. -/
noncomputable def compULiftYonedaIsoULiftYonedaCompLan :
F ⋙ uliftYoneda.{max w v₁} ≅ uliftYoneda.{max w v₂} ⋙ F.op.lan :=
NatIso.ofComponents
(fun X =>
Functor.leftKanExtensionUnique _ (uliftYonedaMap.{w} F X) (F.op.lan.obj _) (F.op.lanUnit.app (uliftYoneda.obj X)))
(fun {X Y} f => by
apply uliftYonedaEquiv.injective
have eq₁ :=
congr_fun
((uliftYoneda.{max w v₁}.obj (F.obj Y)).descOfIsLeftKanExtension_fac_app (uliftYonedaMap F Y)
(F.op.lan.obj (uliftYoneda.obj Y)) (F.op.lanUnit.app (uliftYoneda.obj Y)) _)
⟨f⟩
have eq₂ :=
congr_fun
(((uliftYoneda.{max w v₁}.obj (F.obj X)).descOfIsLeftKanExtension_fac_app (uliftYonedaMap F X)
(F.op.lan.obj (uliftYoneda.obj X)) (F.op.lanUnit.app (uliftYoneda.obj X)))
_)
⟨𝟙 _⟩
have eq₃ := congr_fun (congr_app (F.op.lanUnit.naturality (uliftYoneda.{max w v₂}.map f)) _) ⟨𝟙 _⟩
dsimp [uliftYoneda, uliftYonedaMap, uliftYonedaEquiv, Functor.leftKanExtensionUnique] at eq₁ eq₂ eq₃ ⊢
simp only [Functor.map_id] at eq₂
simp only [id_comp] at eq₃
simp [eq₁, eq₂, eq₃])
