[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (↑F.toPrelaxFunctor).map f ◁ (fun a => η.app a ◁ Γ.app a) b ≫ naturality (η ≫ ι) f =
    naturality (η ≫ θ) f ≫ (fun a => η.app a ◁ Γ.app a) a ▷ (↑H.toPrelaxFunctor).map f
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (↑F.toPrelaxFunctor).map f ◁ η.app b ◁ Γ.app b ≫
      (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) (ι.app b)).inv ≫
        naturality η f ▷ ι.app b ≫
          (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (ι.app b)).hom ≫
            η.app a ◁ naturality ι f ≫ (α_ (η.app a) (ι.app a) ((↑H.toPrelaxFunctor).map f)).inv =
    ((α_ ((↑F.toPrelaxFunctor).map f) (η.app b) (θ.app b)).inv ≫
        naturality η f ▷ θ.app b ≫
          (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (θ.app b)).hom ≫
            η.app a ◁ naturality θ f ≫ (α_ (η.app a) (θ.app a) ((↑H.toPrelaxFunctor).map f)).inv) ≫
      (η.app a ◁ Γ.app a) ▷ (↑H.toPrelaxFunctor).map f
[PROOFSTEP]
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc]
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) (θ.app b)).inv ≫
      naturality η f ▷ θ.app b ≫
        (η.app a ≫ (↑G.toPrelaxFunctor).map f) ◁ Γ.app b ≫
          (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (ι.app b)).hom ≫
            η.app a ◁ naturality ι f ≫ (α_ (η.app a) (ι.app a) ((↑H.toPrelaxFunctor).map f)).inv =
    ((α_ ((↑F.toPrelaxFunctor).map f) (η.app b) (θ.app b)).inv ≫
        naturality η f ▷ θ.app b ≫
          (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (θ.app b)).hom ≫
            η.app a ◁ naturality θ f ≫ (α_ (η.app a) (θ.app a) ((↑H.toPrelaxFunctor).map f)).inv) ≫
      (η.app a ◁ Γ.app a) ▷ (↑H.toPrelaxFunctor).map f
[PROOFSTEP]
simp
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ (↑F.toPrelaxFunctor).map f ◁ (fun a => Γ.app a ▷ ι.app a) b ≫ naturality (θ ≫ ι) f =
    naturality (η ≫ ι) f ≫ (fun a => Γ.app a ▷ ι.app a) a ▷ (↑H.toPrelaxFunctor).map f
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ (↑F.toPrelaxFunctor).map f ◁ Γ.app b ▷ ι.app b ≫
      (α_ ((↑F.toPrelaxFunctor).map f) (θ.app b) (ι.app b)).inv ≫
        naturality θ f ▷ ι.app b ≫
          (α_ (θ.app a) ((↑G.toPrelaxFunctor).map f) (ι.app b)).hom ≫
            θ.app a ◁ naturality ι f ≫ (α_ (θ.app a) (ι.app a) ((↑H.toPrelaxFunctor).map f)).inv =
    ((α_ ((↑F.toPrelaxFunctor).map f) (η.app b) (ι.app b)).inv ≫
        naturality η f ▷ ι.app b ≫
          (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (ι.app b)).hom ≫
            η.app a ◁ naturality ι f ≫ (α_ (η.app a) (ι.app a) ((↑H.toPrelaxFunctor).map f)).inv) ≫
      Γ.app a ▷ ι.app a ▷ (↑H.toPrelaxFunctor).map f
[PROOFSTEP]
simp_rw [assoc, ← associator_inv_naturality_left, whisker_exchange_assoc]
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ (↑F.toPrelaxFunctor).map f ◁ Γ.app b ▷ ι.app b ≫
      (α_ ((↑F.toPrelaxFunctor).map f) (θ.app b) (ι.app b)).inv ≫
        naturality θ f ▷ ι.app b ≫
          (α_ (θ.app a) ((↑G.toPrelaxFunctor).map f) (ι.app b)).hom ≫
            θ.app a ◁ naturality ι f ≫ (α_ (θ.app a) (ι.app a) ((↑H.toPrelaxFunctor).map f)).inv =
    (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) (ι.app b)).inv ≫
      naturality η f ▷ ι.app b ≫
        (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (ι.app b)).hom ≫
          Γ.app a ▷ ((↑G.toPrelaxFunctor).map f ≫ ι.app b) ≫
            θ.app a ◁ naturality ι f ≫ (α_ (θ.app a) (ι.app a) ((↑H.toPrelaxFunctor).map f)).inv
[PROOFSTEP]
simp
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
⊢ ∀ {a b : B} (f : a ⟶ b),
    (↑F.toPrelaxFunctor).map f ◁ ((fun a => α_ (η.app a) (θ.app a) (ι.app a)) b).hom ≫ naturality (η ≫ θ ≫ ι) f =
      naturality ((η ≫ θ) ≫ ι) f ≫ ((fun a => α_ (η.app a) (θ.app a) (ι.app a)) a).hom ▷ (↑I.toPrelaxFunctor).map f
[PROOFSTEP]
aesop_cat
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η : F ⟶ G
⊢ ∀ {a b : B} (f : a ⟶ b),
    (↑F.toPrelaxFunctor).map f ◁ ((fun a => λ_ (η.app a)) b).hom ≫ naturality η f =
      naturality (𝟙 F ≫ η) f ≫ ((fun a => λ_ (η.app a)) a).hom ▷ (↑G.toPrelaxFunctor).map f
[PROOFSTEP]
aesop_cat
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : OplaxFunctor B C
η : F ⟶ G
⊢ ∀ {a b : B} (f : a ⟶ b),
    (↑F.toPrelaxFunctor).map f ◁ ((fun a => ρ_ (η.app a)) b).hom ≫ naturality η f =
      naturality (η ≫ 𝟙 G) f ≫ ((fun a => ρ_ (η.app a)) a).hom ▷ (↑G.toPrelaxFunctor).map f
[PROOFSTEP]
aesop_cat
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : OplaxFunctor B C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
⊢ (fun {F G H} η x x_1 Γ => OplaxNatTrans.whiskerLeft η Γ) f h i θ ≫
      (fun {F G H} x x_1 Γ η => OplaxNatTrans.whiskerRight Γ η) f g η i =
    (fun {F G H} x x_1 Γ η => OplaxNatTrans.whiskerRight Γ η) f g η h ≫
      (fun {F G H} η x x_1 Γ => OplaxNatTrans.whiskerLeft η Γ) g h i θ
[PROOFSTEP]
ext
[GOAL]
case w
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I a b c : OplaxFunctor B C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
b✝ : B
⊢ ((fun {F G H} η x x_1 Γ => OplaxNatTrans.whiskerLeft η Γ) f h i θ ≫
          (fun {F G H} x x_1 Γ η => OplaxNatTrans.whiskerRight Γ η) f g η i).app
      b✝ =
    ((fun {F G H} x x_1 Γ η => OplaxNatTrans.whiskerRight Γ η) f g η h ≫
          (fun {F G H} η x x_1 Γ => OplaxNatTrans.whiskerLeft η Γ) g h i θ).app
      b✝
[PROOFSTEP]
exact whisker_exchange _ _
