no goals
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
a' : C
f g : a ⟶ b
β : f ⟶ g
h : (↑G.toPrelaxFunctor).obj b ⟶ a'
⊢ PrelaxFunctor.map₂ F.toPrelaxFunctor β ▷ app η b ▷ h ≫ naturality η g ▷ h =
    naturality η f ▷ h ≫
      (α_ (app η a) ((↑G.toPrelaxFunctor).map f) h).hom ≫
        app η a ◁ PrelaxFunctor.map₂ G.toPrelaxFunctor β ▷ h ≫ (α_ (app η a) ((↑G.toPrelaxFunctor).map g) h).inv
rw [← comp_whiskerRight, naturality_naturality, comp_whiskerRight, whisker_assoc]