∀ {C : Type u_1} {H : Type u_3} {D : Type u_5} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_2, u_3} H] [inst_2 : CategoryTheory.Category.{u_6, u_5} D]
  {L : CategoryTheory.Functor C D} {F₁ F₂ : CategoryTheory.Functor C H} (α₁ : L.RightExtension F₁)
  (α₂ : L.RightExtension F₂) (e : F₁ ≅ F₂) (e' : α₁.left ≅ α₂.left),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft e'.hom) α₂.hom = CategoryTheory.CategoryStruct.comp α₁.hom e.hom →
    CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.whiskeringLeft C D H).obj L).map e'.hom) α₂.hom =
      ((L.rightExtensionEquivalenceOfIso₂ e).functor.obj α₁).hom