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 : a' ⟶ (↑G.toPrelaxFunctor).obj a
g h : a ⟶ b
β : g ⟶ h
⊢ f ◁ PrelaxFunctor.map₂ G.toPrelaxFunctor β ▷ app θ b ≫ f ◁ naturality θ h =
    f ◁ naturality θ g ≫ f ◁ app θ a ◁ PrelaxFunctor.map₂ H.toPrelaxFunctor β
simp_rw [← whiskerLeft_comp, naturality_naturality]