no goals
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η θ ι : F ⟶ G
Γ : Modification η θ
a b c : B
a' : C
f : a' ⟶ (↑F.toPrelaxFunctor).obj b
g : b ⟶ c
⊢ f ◁ (↑F.toPrelaxFunctor).map g ◁ app Γ c ≫ f ◁ OplaxNatTrans.naturality θ g =
    f ◁ OplaxNatTrans.naturality η g ≫ f ◁ app Γ b ▷ (↑G.toPrelaxFunctor).map g
simp_rw [← whiskerLeft_comp, naturality]