∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D] {L : C ≌ D}
  {F₀ : CategoryTheory.Functor C H} {F₁ : CategoryTheory.Functor D H} (α : F₀ ≅ L.functor.comp F₁),
  F₁.IsLeftKanExtension α.hom