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 ⟶ b
g : (↑G.toPrelaxFunctor).obj b ⟶ a'
⊢ (↑F.toPrelaxFunctor).map f ◁ app Γ b ▷ g ≫
      (α_ ((↑F.toPrelaxFunctor).map f) (OplaxNatTrans.app θ b) g).inv ≫ OplaxNatTrans.naturality θ f ▷ g =
    (α_ ((↑F.toPrelaxFunctor).map f) (OplaxNatTrans.app η b) g).inv ≫
      OplaxNatTrans.naturality η f ▷ g ≫ app Γ a ▷ (↑G.toPrelaxFunctor).map f ▷ g
simp_rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight, naturality]