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 : a ⟶ b
h : b ⟶ c
⊢ f ◁ naturality θ (g ≫ h) ≫ f ◁ app θ a ◁ OplaxFunctor.mapComp H g h =
    f ◁ OplaxFunctor.mapComp G g h ▷ app θ c ≫
      f ◁ (α_ ((↑G.toPrelaxFunctor).map g) ((↑G.toPrelaxFunctor).map h) (app θ c)).hom ≫
        f ◁ (↑G.toPrelaxFunctor).map g ◁ naturality θ h ≫
          f ◁ (α_ ((↑G.toPrelaxFunctor).map g) (app θ b) ((↑H.toPrelaxFunctor).map h)).inv ≫
            f ◁ naturality θ g ▷ (↑H.toPrelaxFunctor).map h ≫
              f ◁ (α_ (app θ a) ((↑H.toPrelaxFunctor).map g) ((↑H.toPrelaxFunctor).map h)).hom
simp_rw [← whiskerLeft_comp, naturality_comp]