∀ {𝒮 : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} 𝒮] {a b c d : CategoryTheory.BasedCategory 𝒮}
  (f : CategoryTheory.BasedFunctor a b) {g g' : CategoryTheory.BasedFunctor b c} (η : g ⟶ g')
  (h : CategoryTheory.BasedFunctor c d),
  CategoryTheory.BasedCategory.whiskerRight (CategoryTheory.BasedCategory.whiskerLeft f η) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.BasedNatIso.id ((f.comp g).comp h)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.BasedCategory.whiskerLeft f (CategoryTheory.BasedCategory.whiskerRight η h))
        (CategoryTheory.BasedNatIso.id ((f.comp g').comp h)).inv)