∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [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]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  {G : CategoryTheory.Functor D D'} [G.IsEquivalence] (e : L.comp G ≅ L') (F : CategoryTheory.Functor C H),
  L'.HasLeftKanExtension F ↔ L.HasLeftKanExtension F