∀ {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 L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L))
  (X_1 : D),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).unitIso.hom.app X).right.app X_1 =
    CategoryTheory.CategoryStruct.id (X.right.obj X_1)