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
⊢ f ◁ naturality θ (𝟙 a) ≫ f ◁ app θ a ◁ OplaxFunctor.mapId H a =
    f ◁ OplaxFunctor.mapId G a ▷ app θ a ≫ f ◁ (λ_ (app θ a)).hom ≫ f ◁ (ρ_ (app θ a)).inv
simp_rw [← whiskerLeft_comp, naturality_id]