∀ {A : Type u_5} {B : Type u_7} {C : Type u_1} {D : Type u_3} [inst : CategoryTheory.Category.{u_8, u_5} A]
  [inst_1 : CategoryTheory.Category.{u_6, u_7} B] [inst_2 : CategoryTheory.Category.{u_4, u_1} C]
  [inst_3 : CategoryTheory.Category.{u_2, u_3} D] (G : CategoryTheory.Functor B D) (L : CategoryTheory.Functor A C)
  [inst_4 : G.PreservesLeftKanExtensions L] [inst_5 : ∀ (F : CategoryTheory.Functor A B), L.HasLeftKanExtension F]
  [inst_6 : ∀ (F : CategoryTheory.Functor A D), L.HasLeftKanExtension F] {F F' : CategoryTheory.Functor A B}
  (η : F ⟶ F'),
  CategoryTheory.CategoryStruct.comp ((L.lan.comp ((CategoryTheory.Functor.whiskeringRight C B D).obj G)).map η)
      ((fun F => G.leftKanExtensionCompIsoOfPreserves F L) F').hom =
    CategoryTheory.CategoryStruct.comp ((fun F => G.leftKanExtensionCompIsoOfPreserves F L) F).hom
      ((((CategoryTheory.Functor.whiskeringRight A B D).obj G).comp L.lan).map η)