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 : (↑G.toPrelaxFunctor).obj a ⟶ a'
⊢ (OplaxFunctor.mapId F a ▷ app η a ≫ (λ_ (app η a)).hom ≫ (ρ_ (app η a)).inv) ▷ f ≫
      (α_ (app η a) (𝟙 ((↑G.toPrelaxFunctor).obj a)) f).hom =
    OplaxFunctor.mapId F a ▷ app η a ▷ f ≫
      (λ_ (app η a)).hom ▷ f ≫ (ρ_ (app η a)).inv ▷ f ≫ (α_ (app η a) (𝟙 ((↑G.toPrelaxFunctor).obj a)) f).hom
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 : (↑G.toPrelaxFunctor).obj a ⟶ a'
⊢ naturality η (𝟙 a) ▷ f ≫
      (α_ (app η a) ((↑G.toPrelaxFunctor).map (𝟙 a)) f).hom ≫ app η a ◁ OplaxFunctor.mapId G a ▷ f =
    OplaxFunctor.mapId F a ▷ app η a ▷ f ≫
      (λ_ (app η a)).hom ▷ f ≫ (ρ_ (app η a)).inv ▷ f ≫ (α_ (app η a) (𝟙 ((↑G.toPrelaxFunctor).obj a)) f).hom
rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, naturality_id]
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 : (↑G.toPrelaxFunctor).obj a ⟶ a'
⊢ (OplaxFunctor.mapId F a ▷ app η a ≫ (λ_ (app η a)).hom ≫ (ρ_ (app η a)).inv) ▷ f ≫
      (α_ (app η a) (𝟙 ((↑G.toPrelaxFunctor).obj a)) f).hom =
    OplaxFunctor.mapId F a ▷ app η a ▷ f ≫
      (λ_ (app η a)).hom ▷ f ≫ (ρ_ (app η a)).inv ▷ f ≫ (α_ (app η a) (𝟙 ((↑G.toPrelaxFunctor).obj a)) f).hom
simp