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 ⟶ b
g : b ⟶ c
h : (↑G.toPrelaxFunctor).obj c ⟶ a'
⊢ (OplaxFunctor.mapComp F f g ▷ app η c ≫
          (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (app η c)).hom ≫
            (↑F.toPrelaxFunctor).map f ◁ naturality η g ≫
              (α_ ((↑F.toPrelaxFunctor).map f) (app η b) ((↑G.toPrelaxFunctor).map g)).inv ≫
                naturality η f ▷ (↑G.toPrelaxFunctor).map g ≫
                  (α_ (app η a) ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)).hom) ▷
        h ≫
      (α_ (app η a) ((↑G.toPrelaxFunctor).map f ≫ (↑G.toPrelaxFunctor).map g) h).hom =
    OplaxFunctor.mapComp F f g ▷ app η c ▷ h ≫
      (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (app η c)).hom ▷ h ≫
        (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ app η c) h).hom ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ h ≫
            (α_ ((↑F.toPrelaxFunctor).map f) (app η b ≫ (↑G.toPrelaxFunctor).map g) h).inv ≫
              (α_ ((↑F.toPrelaxFunctor).map f) (app η b) ((↑G.toPrelaxFunctor).map g)).inv ▷ h ≫
                naturality η f ▷ (↑G.toPrelaxFunctor).map g ▷ h ≫
                  (α_ (app η a) ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)).hom ▷ h ≫
                    (α_ (app η a) ((↑G.toPrelaxFunctor).map f ≫ (↑G.toPrelaxFunctor).map g) h).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 : a ⟶ b
g : b ⟶ c
h : (↑G.toPrelaxFunctor).obj c ⟶ a'
⊢ naturality η (f ≫ g) ▷ h ≫
      (α_ (app η a) ((↑G.toPrelaxFunctor).map (f ≫ g)) h).hom ≫ app η a ◁ OplaxFunctor.mapComp G f g ▷ h =
    OplaxFunctor.mapComp F f g ▷ app η c ▷ h ≫
      (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (app η c)).hom ▷ h ≫
        (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ app η c) h).hom ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ h ≫
            (α_ ((↑F.toPrelaxFunctor).map f) (app η b ≫ (↑G.toPrelaxFunctor).map g) h).inv ≫
              (α_ ((↑F.toPrelaxFunctor).map f) (app η b) ((↑G.toPrelaxFunctor).map g)).inv ▷ h ≫
                naturality η f ▷ (↑G.toPrelaxFunctor).map g ▷ h ≫
                  (α_ (app η a) ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)).hom ▷ h ≫
                    (α_ (app η a) ((↑G.toPrelaxFunctor).map f ≫ (↑G.toPrelaxFunctor).map g) h).hom
rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, naturality_comp]
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 ⟶ b
g : b ⟶ c
h : (↑G.toPrelaxFunctor).obj c ⟶ a'
⊢ (OplaxFunctor.mapComp F f g ▷ app η c ≫
          (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (app η c)).hom ≫
            (↑F.toPrelaxFunctor).map f ◁ naturality η g ≫
              (α_ ((↑F.toPrelaxFunctor).map f) (app η b) ((↑G.toPrelaxFunctor).map g)).inv ≫
                naturality η f ▷ (↑G.toPrelaxFunctor).map g ≫
                  (α_ (app η a) ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)).hom) ▷
        h ≫
      (α_ (app η a) ((↑G.toPrelaxFunctor).map f ≫ (↑G.toPrelaxFunctor).map g) h).hom =
    OplaxFunctor.mapComp F f g ▷ app η c ▷ h ≫
      (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (app η c)).hom ▷ h ≫
        (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ app η c) h).hom ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ h ≫
            (α_ ((↑F.toPrelaxFunctor).map f) (app η b ≫ (↑G.toPrelaxFunctor).map g) h).inv ≫
              (α_ ((↑F.toPrelaxFunctor).map f) (app η b) ((↑G.toPrelaxFunctor).map g)).inv ▷ h ≫
                naturality η f ▷ (↑G.toPrelaxFunctor).map g ▷ h ≫
                  (α_ (app η a) ((↑G.toPrelaxFunctor).map f) ((↑G.toPrelaxFunctor).map g)).hom ▷ h ≫
                    (α_ (app η a) ((↑G.toPrelaxFunctor).map f ≫ (↑G.toPrelaxFunctor).map g) h).hom
simp