[GOAL]
B : Type u₁
inst✝⁵ : Quiver B
inst✝⁴ : (a b : B) → Quiver (a ⟶ b)
C : Type u₂
inst✝³ : Quiver C
inst✝² : (a b : C) → Quiver (a ⟶ b)
D : Type u₃
inst✝¹ : Quiver D
inst✝ : (a b : D) → Quiver (a ⟶ b)
F✝ F : PrelaxFunctor B C
G : PrelaxFunctor C D
src✝ : B ⥤q D := ↑F ⋙q ↑G
a✝ b✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
⊢ { obj := src✝.obj, map := fun {X Y} => src✝.map }.map f✝ ⟶ { obj := src✝.obj, map := fun {X Y} => src✝.map }.map g✝
[PROOFSTEP]
exact G.map₂ (F.map₂ η)
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a : B
⊢ (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map (𝟙 a) ⟶
    𝟙 ((↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).obj a)
[PROOFSTEP]
exact (G.mapFunctor _ _).map (F.mapId a) ≫ G.mapId (F.obj a)
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
⊢ (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map (f ≫ g) ⟶
    (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f ≫
      (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map g
[PROOFSTEP]
exact (G.mapFunctor _ _).map (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } (η ▷ g) ≫
      (fun {a b c} f g =>
          (mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj c)).map (mapComp F f g) ≫
            mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g))
        f'✝ g =
    (fun {a b c} f g =>
          (mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj c)).map (mapComp F f g) ≫
            mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g))
        f✝ g ≫
      PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } η ▷
        (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map g
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ PrelaxFunctor.map₂ G.toPrelaxFunctor (PrelaxFunctor.map₂ F.toPrelaxFunctor (η ▷ g)) ≫
      PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F f'✝ g) ≫
        mapComp G ((↑F.toPrelaxFunctor).map f'✝) ((↑F.toPrelaxFunctor).map g) =
    (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F f✝ g) ≫
        mapComp G ((↑F.toPrelaxFunctor).map f✝) ((↑F.toPrelaxFunctor).map g)) ≫
      PrelaxFunctor.map₂ G.toPrelaxFunctor (PrelaxFunctor.map₂ F.toPrelaxFunctor η) ▷
        (↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map g)
[PROOFSTEP]
rw [← map₂_comp_assoc, mapComp_naturality_left, map₂_comp_assoc, mapComp_naturality_left, assoc]
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
⊢ ∀ {g g' : b✝ ⟶ c✝} (η_1 : g ⟶ g'),
    PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } (η ◁ η_1) ≫
        (fun {a b c} f g =>
            (mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj c)).map (mapComp F f g) ≫
              mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g))
          η g' =
      (fun {a b c} f g =>
            (mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj c)).map (mapComp F f g) ≫
              mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g))
          η g ≫
        (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map η ◁
          PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } η_1
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
⊢ ∀ {g g' : b✝ ⟶ c✝} (η_1 : g ⟶ g'),
    PrelaxFunctor.map₂ G.toPrelaxFunctor (PrelaxFunctor.map₂ F.toPrelaxFunctor (η ◁ η_1)) ≫
        PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F η g') ≫
          mapComp G ((↑F.toPrelaxFunctor).map η) ((↑F.toPrelaxFunctor).map g') =
      (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F η g) ≫
          mapComp G ((↑F.toPrelaxFunctor).map η) ((↑F.toPrelaxFunctor).map g)) ≫
        (↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map η) ◁
          PrelaxFunctor.map₂ G.toPrelaxFunctor (PrelaxFunctor.map₂ F.toPrelaxFunctor η_1)
[PROOFSTEP]
intros
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ c✝ : B
η : a✝ ⟶ b✝
g✝ g'✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ g'✝
⊢ PrelaxFunctor.map₂ G.toPrelaxFunctor (PrelaxFunctor.map₂ F.toPrelaxFunctor (η ◁ η✝)) ≫
      PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F η g'✝) ≫
        mapComp G ((↑F.toPrelaxFunctor).map η) ((↑F.toPrelaxFunctor).map g'✝) =
    (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F η g✝) ≫
        mapComp G ((↑F.toPrelaxFunctor).map η) ((↑F.toPrelaxFunctor).map g✝)) ≫
      (↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map η) ◁
        PrelaxFunctor.map₂ G.toPrelaxFunctor (PrelaxFunctor.map₂ F.toPrelaxFunctor η✝)
[PROOFSTEP]
rw [← map₂_comp_assoc, mapComp_naturality_right, map₂_comp_assoc, mapComp_naturality_right, assoc]
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } (α_ f g h).hom ≫
      (fun {a b c} f g =>
            (mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj c)).map (mapComp F f g) ≫
              mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g))
          f (g ≫ h) ≫
        (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f ◁
          (fun {a b c} f g =>
              (mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj c)).map (mapComp F f g) ≫
                mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g))
            g h =
    (fun {a b c} f g =>
          (mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj c)).map (mapComp F f g) ≫
            mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g))
        (f ≫ g) h ≫
      (fun {a b c} f g =>
              (mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj c)).map (mapComp F f g) ≫
                mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g))
            f g ▷
          (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map h ≫
        (α_ ((↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f)
            ((↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map g)
            ((↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map h)).hom
[PROOFSTEP]
dsimp
  -- porting note: if you use the `map₂_associator_aux` hack in the definition of
        -- `map₂_associator` then the `simp only` call below does not seem to apply `map₂_associator`
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ PrelaxFunctor.map₂ G.toPrelaxFunctor (PrelaxFunctor.map₂ F.toPrelaxFunctor (α_ f g h).hom) ≫
      (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F f (g ≫ h)) ≫
          mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map (g ≫ h))) ≫
        (↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map f) ◁
          (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F g h) ≫
            mapComp G ((↑F.toPrelaxFunctor).map g) ((↑F.toPrelaxFunctor).map h)) =
    (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F (f ≫ g) h) ≫
        mapComp G ((↑F.toPrelaxFunctor).map (f ≫ g)) ((↑F.toPrelaxFunctor).map h)) ≫
      (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F f g) ≫
            mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g)) ▷
          (↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map h) ≫
        (α_ ((↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map f))
            ((↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map g))
            ((↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map h))).hom
[PROOFSTEP]
simp only [map₂_associator, ← map₂_comp_assoc, ← mapComp_naturality_right_assoc, whiskerLeft_comp, assoc]
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ PrelaxFunctor.map₂ G.toPrelaxFunctor
        (mapComp F (f ≫ g) h ≫
          mapComp F f g ▷ (↑F.toPrelaxFunctor).map h ≫
            (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) ((↑F.toPrelaxFunctor).map h)).hom) ≫
      mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ (↑F.toPrelaxFunctor).map h) ≫
        (↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map f) ◁
          mapComp G ((↑F.toPrelaxFunctor).map g) ((↑F.toPrelaxFunctor).map h) =
    PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F (f ≫ g) h) ≫
      mapComp G ((↑F.toPrelaxFunctor).map (f ≫ g)) ((↑F.toPrelaxFunctor).map h) ≫
        (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F f g) ≫
              mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g)) ▷
            (↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map h) ≫
          (α_ ((↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map f))
              ((↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map g))
              ((↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map h))).hom
[PROOFSTEP]
simp only [map₂_associator, map₂_comp, mapComp_naturality_left_assoc, comp_whiskerRight, assoc]
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } (λ_ f).hom =
    (fun {a b c} f g =>
          (mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj c)).map (mapComp F f g) ≫
            mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g))
        (𝟙 a✝) f ≫
      (fun a =>
              (mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj a)).map (mapId F a) ≫
                mapId G ((↑F.toPrelaxFunctor).obj a))
            a✝ ▷
          (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f ≫
        (λ_ ((↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f)).hom
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ PrelaxFunctor.map₂ G.toPrelaxFunctor (PrelaxFunctor.map₂ F.toPrelaxFunctor (λ_ f).hom) =
    (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F (𝟙 a✝) f) ≫
        mapComp G ((↑F.toPrelaxFunctor).map (𝟙 a✝)) ((↑F.toPrelaxFunctor).map f)) ≫
      (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapId F a✝) ≫ mapId G ((↑F.toPrelaxFunctor).obj a✝)) ▷
          (↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map f) ≫
        (λ_ ((↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map f))).hom
[PROOFSTEP]
simp only [map₂_leftUnitor, map₂_comp, mapComp_naturality_left_assoc, comp_whiskerRight, assoc]
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } (ρ_ f).hom =
    (fun {a b c} f g =>
          (mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj c)).map (mapComp F f g) ≫
            mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g))
        f (𝟙 b✝) ≫
      (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f ◁
          (fun a =>
              (mapFunctor G ((↑F.toPrelaxFunctor).obj a) ((↑F.toPrelaxFunctor).obj a)).map (mapId F a) ≫
                mapId G ((↑F.toPrelaxFunctor).obj a))
            b✝ ≫
        (ρ_ ((↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f)).hom
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : OplaxFunctor B C
G : OplaxFunctor C D
src✝ : PrelaxFunctor B D := PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ PrelaxFunctor.map₂ G.toPrelaxFunctor (PrelaxFunctor.map₂ F.toPrelaxFunctor (ρ_ f).hom) =
    (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F f (𝟙 b✝)) ≫
        mapComp G ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map (𝟙 b✝))) ≫
      (↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map f) ◁
          (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapId F b✝) ≫ mapId G ((↑F.toPrelaxFunctor).obj b✝)) ≫
        (ρ_ ((↑G.toPrelaxFunctor).map ((↑F.toPrelaxFunctor).map f))).hom
[PROOFSTEP]
simp only [map₂_rightUnitor, map₂_comp, mapComp_naturality_right_assoc, whiskerLeft_comp, assoc]
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
F' : OplaxFunctor.PseudoCore F
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } (f ◁ η) =
    ((fun {a b c} => OplaxFunctor.PseudoCore.mapCompIso F') f g).hom ≫
      (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f ◁
          PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } η ≫
        ((fun {a b c} => OplaxFunctor.PseudoCore.mapCompIso F') f h).inv
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
F' : OplaxFunctor.PseudoCore F
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ PrelaxFunctor.map₂ F.toPrelaxFunctor (f ◁ η) =
    (OplaxFunctor.PseudoCore.mapCompIso F' f g).hom ≫
      (↑F.toPrelaxFunctor).map f ◁ PrelaxFunctor.map₂ F.toPrelaxFunctor η ≫
        (OplaxFunctor.PseudoCore.mapCompIso F' f h).inv
[PROOFSTEP]
rw [F'.mapCompIso_hom f g, ← F.mapComp_naturality_right_assoc, ← F'.mapCompIso_hom f h, hom_inv_id, comp_id]
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
F' : OplaxFunctor.PseudoCore F
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } (η ▷ h) =
    ((fun {a b c} => OplaxFunctor.PseudoCore.mapCompIso F') f✝ h).hom ≫
      PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } η ▷
          (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map h ≫
        ((fun {a b c} => OplaxFunctor.PseudoCore.mapCompIso F') g✝ h).inv
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
F' : OplaxFunctor.PseudoCore F
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ PrelaxFunctor.map₂ F.toPrelaxFunctor (η ▷ h) =
    (OplaxFunctor.PseudoCore.mapCompIso F' f✝ h).hom ≫
      PrelaxFunctor.map₂ F.toPrelaxFunctor η ▷ (↑F.toPrelaxFunctor).map h ≫
        (OplaxFunctor.PseudoCore.mapCompIso F' g✝ h).inv
[PROOFSTEP]
rw [F'.mapCompIso_hom _ h, ← F.mapComp_naturality_left_assoc, ← F'.mapCompIso_hom _ h, hom_inv_id, comp_id]
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
F' : OplaxFunctor.PseudoCore F
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } (α_ f g h).hom =
    ((fun {a b c} => OplaxFunctor.PseudoCore.mapCompIso F') (f ≫ g) h).hom ≫
      ((fun {a b c} => OplaxFunctor.PseudoCore.mapCompIso F') f g).hom ▷
          (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map h ≫
        (α_ ((↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f)
              ((↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map g)
              ((↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map h)).hom ≫
          (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f ◁
              ((fun {a b c} => OplaxFunctor.PseudoCore.mapCompIso F') g h).inv ≫
            ((fun {a b c} => OplaxFunctor.PseudoCore.mapCompIso F') f (g ≫ h)).inv
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
F' : OplaxFunctor.PseudoCore F
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ PrelaxFunctor.map₂ F.toPrelaxFunctor (α_ f g h).hom =
    (OplaxFunctor.PseudoCore.mapCompIso F' (f ≫ g) h).hom ≫
      (OplaxFunctor.PseudoCore.mapCompIso F' f g).hom ▷ (↑F.toPrelaxFunctor).map h ≫
        (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) ((↑F.toPrelaxFunctor).map h)).hom ≫
          (↑F.toPrelaxFunctor).map f ◁ (OplaxFunctor.PseudoCore.mapCompIso F' g h).inv ≫
            (OplaxFunctor.PseudoCore.mapCompIso F' f (g ≫ h)).inv
[PROOFSTEP]
rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ← F'.mapCompIso_hom f (g ≫ h), ←
  F'.mapCompIso_hom g h, hom_inv_whiskerLeft_assoc, hom_inv_id, comp_id]
[GOAL]
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
inst✝¹ : ∀ (a : B), IsIso (OplaxFunctor.mapId F a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (OplaxFunctor.mapComp F f g)
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } (f ◁ η) =
    ((fun {a b c} f g => asIso (OplaxFunctor.mapComp F f g)) f g).hom ≫
      (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f ◁
          PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } η ≫
        ((fun {a b c} f g => asIso (OplaxFunctor.mapComp F f g)) f h).inv
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
inst✝¹ : ∀ (a : B), IsIso (OplaxFunctor.mapId F a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (OplaxFunctor.mapComp F f g)
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ PrelaxFunctor.map₂ F.toPrelaxFunctor (f ◁ η) =
    OplaxFunctor.mapComp F f g ≫
      (↑F.toPrelaxFunctor).map f ◁ PrelaxFunctor.map₂ F.toPrelaxFunctor η ≫ inv (OplaxFunctor.mapComp F f h)
[PROOFSTEP]
rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_right]
[GOAL]
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
inst✝¹ : ∀ (a : B), IsIso (OplaxFunctor.mapId F a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (OplaxFunctor.mapComp F f g)
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } (η ▷ h) =
    ((fun {a b c} f g => asIso (OplaxFunctor.mapComp F f g)) f✝ h).hom ≫
      PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } η ▷
          (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map h ≫
        ((fun {a b c} f g => asIso (OplaxFunctor.mapComp F f g)) g✝ h).inv
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
inst✝¹ : ∀ (a : B), IsIso (OplaxFunctor.mapId F a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (OplaxFunctor.mapComp F f g)
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ PrelaxFunctor.map₂ F.toPrelaxFunctor (η ▷ h) =
    OplaxFunctor.mapComp F f✝ h ≫
      PrelaxFunctor.map₂ F.toPrelaxFunctor η ▷ (↑F.toPrelaxFunctor).map h ≫ inv (OplaxFunctor.mapComp F g✝ h)
[PROOFSTEP]
rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_left]
[GOAL]
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
inst✝¹ : ∀ (a : B), IsIso (OplaxFunctor.mapId F a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (OplaxFunctor.mapComp F f g)
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ PrelaxFunctor.map₂ { toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ } (α_ f g h).hom =
    ((fun {a b c} f g => asIso (OplaxFunctor.mapComp F f g)) (f ≫ g) h).hom ≫
      ((fun {a b c} f g => asIso (OplaxFunctor.mapComp F f g)) f g).hom ▷
          (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map h ≫
        (α_ ((↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f)
              ((↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map g)
              ((↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map h)).hom ≫
          (↑{ toPrefunctor := ↑src✝, map₂ := fun {a b} {f g} => PrelaxFunctor.map₂ src✝ }).map f ◁
              ((fun {a b c} f g => asIso (OplaxFunctor.mapComp F f g)) g h).inv ≫
            ((fun {a b c} f g => asIso (OplaxFunctor.mapComp F f g)) f (g ≫ h)).inv
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
inst✝¹ : ∀ (a : B), IsIso (OplaxFunctor.mapId F a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (OplaxFunctor.mapComp F f g)
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ PrelaxFunctor.map₂ F.toPrelaxFunctor (α_ f g h).hom =
    OplaxFunctor.mapComp F (f ≫ g) h ≫
      OplaxFunctor.mapComp F f g ▷ (↑F.toPrelaxFunctor).map h ≫
        (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) ((↑F.toPrelaxFunctor).map h)).hom ≫
          (↑F.toPrelaxFunctor).map f ◁ inv (OplaxFunctor.mapComp F g h) ≫ inv (OplaxFunctor.mapComp F f (g ≫ h))
[PROOFSTEP]
simp only [← assoc]
[GOAL]
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
inst✝¹ : ∀ (a : B), IsIso (OplaxFunctor.mapId F a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (OplaxFunctor.mapComp F f g)
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ PrelaxFunctor.map₂ F.toPrelaxFunctor (α_ f g h).hom =
    (((OplaxFunctor.mapComp F (f ≫ g) h ≫ OplaxFunctor.mapComp F f g ▷ (↑F.toPrelaxFunctor).map h) ≫
          (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) ((↑F.toPrelaxFunctor).map h)).hom) ≫
        (↑F.toPrelaxFunctor).map f ◁ inv (OplaxFunctor.mapComp F g h)) ≫
      inv (OplaxFunctor.mapComp F f (g ≫ h))
[PROOFSTEP]
rw [IsIso.eq_comp_inv, ← inv_whiskerLeft, IsIso.eq_comp_inv]
[GOAL]
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : Pseudofunctor B C
F : OplaxFunctor B C
inst✝¹ : ∀ (a : B), IsIso (OplaxFunctor.mapId F a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (OplaxFunctor.mapComp F f g)
src✝ : PrelaxFunctor B C := F.toPrelaxFunctor
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ (PrelaxFunctor.map₂ F.toPrelaxFunctor (α_ f g h).hom ≫ OplaxFunctor.mapComp F f (g ≫ h)) ≫
      (↑F.toPrelaxFunctor).map f ◁ OplaxFunctor.mapComp F g h =
    (OplaxFunctor.mapComp F (f ≫ g) h ≫ OplaxFunctor.mapComp F f g ▷ (↑F.toPrelaxFunctor).map h) ≫
      (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) ((↑F.toPrelaxFunctor).map h)).hom
[PROOFSTEP]
simp only [assoc, F.map₂_associator]


[GOAL]
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 h : a ⟶ b
β : g ⟶ h
⊢ f ◁ PrelaxFunctor.map₂ G.toPrelaxFunctor β ▷ θ.app b ≫ f ◁ naturality θ h =
    f ◁ naturality θ g ≫ f ◁ θ.app a ◁ PrelaxFunctor.map₂ H.toPrelaxFunctor β
[PROOFSTEP]
simp_rw [← whiskerLeft_comp, naturality_naturality]
[GOAL]
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 : a ⟶ b
β : f ⟶ g
h : (↑G.toPrelaxFunctor).obj b ⟶ a'
⊢ PrelaxFunctor.map₂ F.toPrelaxFunctor β ▷ η.app b ▷ h ≫ naturality η g ▷ h =
    naturality η f ▷ h ≫
      (α_ (η.app a) ((↑G.toPrelaxFunctor).map f) h).hom ≫
        η.app a ◁ PrelaxFunctor.map₂ G.toPrelaxFunctor β ▷ h ≫ (α_ (η.app a) ((↑G.toPrelaxFunctor).map g) h).inv
[PROOFSTEP]
rw [← comp_whiskerRight, naturality_naturality, comp_whiskerRight, whisker_assoc]
[GOAL]
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
[PROOFSTEP]
simp_rw [← whiskerLeft_comp, naturality_comp]
[GOAL]
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
[PROOFSTEP]
rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, naturality_comp]
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
simp_rw [← whiskerLeft_comp, naturality_id]
[GOAL]
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
[PROOFSTEP]
rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, naturality_id]
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
x✝⁴ x✝³ : B
x✝² x✝¹ : x✝⁴ ⟶ x✝³
x✝ : x✝² ⟶ x✝¹
⊢ PrelaxFunctor.map₂ F.toPrelaxFunctor x✝ ▷ (fun a => η.app a ≫ θ.app a) x✝³ ≫
      (fun {a b} f =>
          (α_ ((↑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)
        x✝¹ =
    (fun {a b} f =>
          (α_ ((↑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)
        x✝² ≫
      (fun a => η.app a ≫ θ.app a) x✝⁴ ◁ PrelaxFunctor.map₂ H.toPrelaxFunctor x✝
[PROOFSTEP]
simp only [whiskerRight_comp, assoc, Iso.hom_inv_id_assoc, whiskerRight_naturality_naturality_assoc,
  Iso.inv_hom_id_assoc, whiskerLeft_naturality_naturality_assoc, comp_whiskerLeft]
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
x✝ : B
⊢ (fun {a b} f =>
          (α_ ((↑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)
        (𝟙 x✝) ≫
      (fun a => η.app a ≫ θ.app a) x✝ ◁ OplaxFunctor.mapId H x✝ =
    OplaxFunctor.mapId F x✝ ▷ (fun a => η.app a ≫ θ.app a) x✝ ≫
      (λ_ ((fun a => η.app a ≫ θ.app a) x✝)).hom ≫ (ρ_ ((fun a => η.app a ≫ θ.app a) x✝)).inv
[PROOFSTEP]
simp only [comp_whiskerLeft, assoc, Iso.inv_hom_id_assoc, whiskerLeft_naturality_id_assoc, whiskerLeft_rightUnitor_inv,
  Iso.hom_inv_id, comp_id, whiskerRight_naturality_id_assoc, leftUnitor_whiskerRight, triangle_assoc,
  inv_hom_whiskerRight_assoc, whiskerRight_comp]
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (fun {a b} f =>
          (α_ ((↑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 ≫ g) ≫
      (fun a => η.app a ≫ θ.app a) a ◁ OplaxFunctor.mapComp H f g =
    OplaxFunctor.mapComp F f g ▷ (fun a => η.app a ≫ θ.app a) c ≫
      (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) ((fun a => η.app a ≫ θ.app a) c)).hom ≫
        (↑F.toPrelaxFunctor).map f ◁
            (fun {a b} f =>
                (α_ ((↑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)
              g ≫
          (α_ ((↑F.toPrelaxFunctor).map f) ((fun a => η.app a ≫ θ.app a) b) ((↑H.toPrelaxFunctor).map g)).inv ≫
            (fun {a b} f =>
                    (α_ ((↑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 ▷
                (↑H.toPrelaxFunctor).map g ≫
              (α_ ((fun a => η.app a ≫ θ.app a) a) ((↑H.toPrelaxFunctor).map f) ((↑H.toPrelaxFunctor).map g)).hom
[PROOFSTEP]
calc
  _ =
      ?_ ≫
        F.mapComp f g ▷ η.app c ▷ θ.app c ≫
          ?_ ≫
            F.map f ◁ η.naturality g ▷ θ.app c ≫
              ?_ ≫
                (F.map f ≫ η.app b) ◁ θ.naturality g ≫
                  η.naturality f ▷ (θ.app b ≫ H.map g) ≫ ?_ ≫ η.app a ◁ θ.naturality f ▷ H.map g ≫ ?_ :=
    ?_
  _ = _ := ?_
[GOAL]
case calc_1
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (↑F.toPrelaxFunctor).map (f ≫ g) ≫ (fun a => η.app a ≫ θ.app a) c ⟶
    ((↑F.toPrelaxFunctor).map (f ≫ g) ≫ η.app c) ≫ θ.app c
case calc_2
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (((↑F.toPrelaxFunctor).map f ≫ (↑F.toPrelaxFunctor).map g) ≫ η.app c) ≫ θ.app c ⟶
    (↑F.toPrelaxFunctor).map f ≫ ((↑F.toPrelaxFunctor).map g ≫ η.app c) ≫ θ.app c
case calc_3
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (↑F.toPrelaxFunctor).map f ≫ (η.app b ≫ (↑G.toPrelaxFunctor).map g) ≫ θ.app c ⟶
    ((↑F.toPrelaxFunctor).map f ≫ η.app b) ≫ (↑G.toPrelaxFunctor).map g ≫ θ.app c
case calc_4
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (η.app a ≫ (↑G.toPrelaxFunctor).map f) ≫ θ.app b ≫ (↑H.toPrelaxFunctor).map g ⟶
    η.app a ≫ ((↑G.toPrelaxFunctor).map f ≫ θ.app b) ≫ (↑H.toPrelaxFunctor).map g
case calc_5
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ η.app a ≫ (θ.app a ≫ (↑H.toPrelaxFunctor).map f) ≫ (↑H.toPrelaxFunctor).map g ⟶
    (fun a => η.app a ≫ θ.app a) a ≫ (↑H.toPrelaxFunctor).map f ≫ (↑H.toPrelaxFunctor).map g
case calc_6
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (fun {a b} f =>
          (α_ ((↑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 ≫ g) ≫
      (fun a => η.app a ≫ θ.app a) a ◁ OplaxFunctor.mapComp H f g =
    ?calc_1 ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ?calc_2 ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ?calc_3 ≫
              ((↑F.toPrelaxFunctor).map f ≫ η.app b) ◁ naturality θ g ≫
                naturality η f ▷ (θ.app b ≫ (↑H.toPrelaxFunctor).map g) ≫
                  ?calc_4 ≫ η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫ ?calc_5
case calc_7
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ ?calc_1 ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ?calc_2 ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ?calc_3 ≫
              ((↑F.toPrelaxFunctor).map f ≫ η.app b) ◁ naturality θ g ≫
                naturality η f ▷ (θ.app b ≫ (↑H.toPrelaxFunctor).map g) ≫
                  ?calc_4 ≫ η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫ ?calc_5 =
    OplaxFunctor.mapComp F f g ▷ (fun a => η.app a ≫ θ.app a) c ≫
      (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) ((fun a => η.app a ≫ θ.app a) c)).hom ≫
        (↑F.toPrelaxFunctor).map f ◁
            (fun {a b} f =>
                (α_ ((↑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)
              g ≫
          (α_ ((↑F.toPrelaxFunctor).map f) ((fun a => η.app a ≫ θ.app a) b) ((↑H.toPrelaxFunctor).map g)).inv ≫
            (fun {a b} f =>
                    (α_ ((↑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 ▷
                (↑H.toPrelaxFunctor).map g ≫
              (α_ ((fun a => η.app a ≫ θ.app a) a) ((↑H.toPrelaxFunctor).map f) ((↑H.toPrelaxFunctor).map g)).hom
[PROOFSTEP]
exact (α_ _ _ _).inv
[GOAL]
case calc_2
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (((↑F.toPrelaxFunctor).map f ≫ (↑F.toPrelaxFunctor).map g) ≫ η.app c) ≫ θ.app c ⟶
    (↑F.toPrelaxFunctor).map f ≫ ((↑F.toPrelaxFunctor).map g ≫ η.app c) ≫ θ.app c
case calc_3
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (↑F.toPrelaxFunctor).map f ≫ (η.app b ≫ (↑G.toPrelaxFunctor).map g) ≫ θ.app c ⟶
    ((↑F.toPrelaxFunctor).map f ≫ η.app b) ≫ (↑G.toPrelaxFunctor).map g ≫ θ.app c
case calc_4
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (η.app a ≫ (↑G.toPrelaxFunctor).map f) ≫ θ.app b ≫ (↑H.toPrelaxFunctor).map g ⟶
    η.app a ≫ ((↑G.toPrelaxFunctor).map f ≫ θ.app b) ≫ (↑H.toPrelaxFunctor).map g
case calc_5
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ η.app a ≫ (θ.app a ≫ (↑H.toPrelaxFunctor).map f) ≫ (↑H.toPrelaxFunctor).map g ⟶
    (fun a => η.app a ≫ θ.app a) a ≫ (↑H.toPrelaxFunctor).map f ≫ (↑H.toPrelaxFunctor).map g
case calc_6
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (fun {a b} f =>
          (α_ ((↑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 ≫ g) ≫
      (fun a => η.app a ≫ θ.app a) a ◁ OplaxFunctor.mapComp H f g =
    (α_ ((↑F.toPrelaxFunctor).map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ?calc_2 ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ?calc_3 ≫
              ((↑F.toPrelaxFunctor).map f ≫ η.app b) ◁ naturality θ g ≫
                naturality η f ▷ (θ.app b ≫ (↑H.toPrelaxFunctor).map g) ≫
                  ?calc_4 ≫ η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫ ?calc_5
case calc_7
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ ((↑F.toPrelaxFunctor).map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ?calc_2 ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ?calc_3 ≫
              ((↑F.toPrelaxFunctor).map f ≫ η.app b) ◁ naturality θ g ≫
                naturality η f ▷ (θ.app b ≫ (↑H.toPrelaxFunctor).map g) ≫
                  ?calc_4 ≫ η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫ ?calc_5 =
    OplaxFunctor.mapComp F f g ▷ (fun a => η.app a ≫ θ.app a) c ≫
      (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) ((fun a => η.app a ≫ θ.app a) c)).hom ≫
        (↑F.toPrelaxFunctor).map f ◁
            (fun {a b} f =>
                (α_ ((↑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)
              g ≫
          (α_ ((↑F.toPrelaxFunctor).map f) ((fun a => η.app a ≫ θ.app a) b) ((↑H.toPrelaxFunctor).map g)).inv ≫
            (fun {a b} f =>
                    (α_ ((↑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 ▷
                (↑H.toPrelaxFunctor).map g ≫
              (α_ ((fun a => η.app a ≫ θ.app a) a) ((↑H.toPrelaxFunctor).map f) ((↑H.toPrelaxFunctor).map g)).hom
[PROOFSTEP]
exact (α_ _ _ _).hom ▷ _ ≫ (α_ _ _ _).hom
[GOAL]
case calc_3
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (↑F.toPrelaxFunctor).map f ≫ (η.app b ≫ (↑G.toPrelaxFunctor).map g) ≫ θ.app c ⟶
    ((↑F.toPrelaxFunctor).map f ≫ η.app b) ≫ (↑G.toPrelaxFunctor).map g ≫ θ.app c
case calc_4
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (η.app a ≫ (↑G.toPrelaxFunctor).map f) ≫ θ.app b ≫ (↑H.toPrelaxFunctor).map g ⟶
    η.app a ≫ ((↑G.toPrelaxFunctor).map f ≫ θ.app b) ≫ (↑H.toPrelaxFunctor).map g
case calc_5
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ η.app a ≫ (θ.app a ≫ (↑H.toPrelaxFunctor).map f) ≫ (↑H.toPrelaxFunctor).map g ⟶
    (fun a => η.app a ≫ θ.app a) a ≫ (↑H.toPrelaxFunctor).map f ≫ (↑H.toPrelaxFunctor).map g
case calc_6
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (fun {a b} f =>
          (α_ ((↑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 ≫ g) ≫
      (fun a => η.app a ≫ θ.app a) a ◁ OplaxFunctor.mapComp H f g =
    (α_ ((↑F.toPrelaxFunctor).map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ((α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (η.app c)).hom ▷ θ.app c ≫
            (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ η.app c) (θ.app c)).hom) ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ?calc_3 ≫
              ((↑F.toPrelaxFunctor).map f ≫ η.app b) ◁ naturality θ g ≫
                naturality η f ▷ (θ.app b ≫ (↑H.toPrelaxFunctor).map g) ≫
                  ?calc_4 ≫ η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫ ?calc_5
case calc_7
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ ((↑F.toPrelaxFunctor).map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ((α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (η.app c)).hom ▷ θ.app c ≫
            (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ η.app c) (θ.app c)).hom) ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ?calc_3 ≫
              ((↑F.toPrelaxFunctor).map f ≫ η.app b) ◁ naturality θ g ≫
                naturality η f ▷ (θ.app b ≫ (↑H.toPrelaxFunctor).map g) ≫
                  ?calc_4 ≫ η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫ ?calc_5 =
    OplaxFunctor.mapComp F f g ▷ (fun a => η.app a ≫ θ.app a) c ≫
      (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) ((fun a => η.app a ≫ θ.app a) c)).hom ≫
        (↑F.toPrelaxFunctor).map f ◁
            (fun {a b} f =>
                (α_ ((↑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)
              g ≫
          (α_ ((↑F.toPrelaxFunctor).map f) ((fun a => η.app a ≫ θ.app a) b) ((↑H.toPrelaxFunctor).map g)).inv ≫
            (fun {a b} f =>
                    (α_ ((↑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 ▷
                (↑H.toPrelaxFunctor).map g ≫
              (α_ ((fun a => η.app a ≫ θ.app a) a) ((↑H.toPrelaxFunctor).map f) ((↑H.toPrelaxFunctor).map g)).hom
[PROOFSTEP]
exact _ ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv
[GOAL]
case calc_4
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (η.app a ≫ (↑G.toPrelaxFunctor).map f) ≫ θ.app b ≫ (↑H.toPrelaxFunctor).map g ⟶
    η.app a ≫ ((↑G.toPrelaxFunctor).map f ≫ θ.app b) ≫ (↑H.toPrelaxFunctor).map g
case calc_5
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ η.app a ≫ (θ.app a ≫ (↑H.toPrelaxFunctor).map f) ≫ (↑H.toPrelaxFunctor).map g ⟶
    (fun a => η.app a ≫ θ.app a) a ≫ (↑H.toPrelaxFunctor).map f ≫ (↑H.toPrelaxFunctor).map g
case calc_6
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (fun {a b} f =>
          (α_ ((↑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 ≫ g) ≫
      (fun a => η.app a ≫ θ.app a) a ◁ OplaxFunctor.mapComp H f g =
    (α_ ((↑F.toPrelaxFunctor).map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ((α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (η.app c)).hom ▷ θ.app c ≫
            (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ η.app c) (θ.app c)).hom) ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ((↑F.toPrelaxFunctor).map f ◁ (α_ (η.app b) ((↑G.toPrelaxFunctor).map g) (θ.app c)).hom ≫
                (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) ((↑G.toPrelaxFunctor).map g ≫ θ.app c)).inv) ≫
              ((↑F.toPrelaxFunctor).map f ≫ η.app b) ◁ naturality θ g ≫
                naturality η f ▷ (θ.app b ≫ (↑H.toPrelaxFunctor).map g) ≫
                  ?calc_4 ≫ η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫ ?calc_5
case calc_7
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ ((↑F.toPrelaxFunctor).map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ((α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (η.app c)).hom ▷ θ.app c ≫
            (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ η.app c) (θ.app c)).hom) ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ((↑F.toPrelaxFunctor).map f ◁ (α_ (η.app b) ((↑G.toPrelaxFunctor).map g) (θ.app c)).hom ≫
                (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) ((↑G.toPrelaxFunctor).map g ≫ θ.app c)).inv) ≫
              ((↑F.toPrelaxFunctor).map f ≫ η.app b) ◁ naturality θ g ≫
                naturality η f ▷ (θ.app b ≫ (↑H.toPrelaxFunctor).map g) ≫
                  ?calc_4 ≫ η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫ ?calc_5 =
    OplaxFunctor.mapComp F f g ▷ (fun a => η.app a ≫ θ.app a) c ≫
      (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) ((fun a => η.app a ≫ θ.app a) c)).hom ≫
        (↑F.toPrelaxFunctor).map f ◁
            (fun {a b} f =>
                (α_ ((↑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)
              g ≫
          (α_ ((↑F.toPrelaxFunctor).map f) ((fun a => η.app a ≫ θ.app a) b) ((↑H.toPrelaxFunctor).map g)).inv ≫
            (fun {a b} f =>
                    (α_ ((↑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 ▷
                (↑H.toPrelaxFunctor).map g ≫
              (α_ ((fun a => η.app a ≫ θ.app a) a) ((↑H.toPrelaxFunctor).map f) ((↑H.toPrelaxFunctor).map g)).hom
[PROOFSTEP]
exact (α_ _ _ _).hom ≫ _ ◁ (α_ _ _ _).inv
[GOAL]
case calc_5
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ η.app a ≫ (θ.app a ≫ (↑H.toPrelaxFunctor).map f) ≫ (↑H.toPrelaxFunctor).map g ⟶
    (fun a => η.app a ≫ θ.app a) a ≫ (↑H.toPrelaxFunctor).map f ≫ (↑H.toPrelaxFunctor).map g
case calc_6
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (fun {a b} f =>
          (α_ ((↑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 ≫ g) ≫
      (fun a => η.app a ≫ θ.app a) a ◁ OplaxFunctor.mapComp H f g =
    (α_ ((↑F.toPrelaxFunctor).map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ((α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (η.app c)).hom ▷ θ.app c ≫
            (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ η.app c) (θ.app c)).hom) ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ((↑F.toPrelaxFunctor).map f ◁ (α_ (η.app b) ((↑G.toPrelaxFunctor).map g) (θ.app c)).hom ≫
                (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) ((↑G.toPrelaxFunctor).map g ≫ θ.app c)).inv) ≫
              ((↑F.toPrelaxFunctor).map f ≫ η.app b) ◁ naturality θ g ≫
                naturality η f ▷ (θ.app b ≫ (↑H.toPrelaxFunctor).map g) ≫
                  ((α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (θ.app b ≫ (↑H.toPrelaxFunctor).map g)).hom ≫
                      η.app a ◁ (α_ ((↑G.toPrelaxFunctor).map f) (θ.app b) ((↑H.toPrelaxFunctor).map g)).inv) ≫
                    η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫ ?calc_5
case calc_7
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ ((↑F.toPrelaxFunctor).map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ((α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (η.app c)).hom ▷ θ.app c ≫
            (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ η.app c) (θ.app c)).hom) ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ((↑F.toPrelaxFunctor).map f ◁ (α_ (η.app b) ((↑G.toPrelaxFunctor).map g) (θ.app c)).hom ≫
                (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) ((↑G.toPrelaxFunctor).map g ≫ θ.app c)).inv) ≫
              ((↑F.toPrelaxFunctor).map f ≫ η.app b) ◁ naturality θ g ≫
                naturality η f ▷ (θ.app b ≫ (↑H.toPrelaxFunctor).map g) ≫
                  ((α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (θ.app b ≫ (↑H.toPrelaxFunctor).map g)).hom ≫
                      η.app a ◁ (α_ ((↑G.toPrelaxFunctor).map f) (θ.app b) ((↑H.toPrelaxFunctor).map g)).inv) ≫
                    η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫ ?calc_5 =
    OplaxFunctor.mapComp F f g ▷ (fun a => η.app a ≫ θ.app a) c ≫
      (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) ((fun a => η.app a ≫ θ.app a) c)).hom ≫
        (↑F.toPrelaxFunctor).map f ◁
            (fun {a b} f =>
                (α_ ((↑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)
              g ≫
          (α_ ((↑F.toPrelaxFunctor).map f) ((fun a => η.app a ≫ θ.app a) b) ((↑H.toPrelaxFunctor).map g)).inv ≫
            (fun {a b} f =>
                    (α_ ((↑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 ▷
                (↑H.toPrelaxFunctor).map g ≫
              (α_ ((fun a => η.app a ≫ θ.app a) a) ((↑H.toPrelaxFunctor).map f) ((↑H.toPrelaxFunctor).map g)).hom
[PROOFSTEP]
exact _ ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv
[GOAL]
case calc_6
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (fun {a b} f =>
          (α_ ((↑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 ≫ g) ≫
      (fun a => η.app a ≫ θ.app a) a ◁ OplaxFunctor.mapComp H f g =
    (α_ ((↑F.toPrelaxFunctor).map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ((α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (η.app c)).hom ▷ θ.app c ≫
            (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ η.app c) (θ.app c)).hom) ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ((↑F.toPrelaxFunctor).map f ◁ (α_ (η.app b) ((↑G.toPrelaxFunctor).map g) (θ.app c)).hom ≫
                (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) ((↑G.toPrelaxFunctor).map g ≫ θ.app c)).inv) ≫
              ((↑F.toPrelaxFunctor).map f ≫ η.app b) ◁ naturality θ g ≫
                naturality η f ▷ (θ.app b ≫ (↑H.toPrelaxFunctor).map g) ≫
                  ((α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (θ.app b ≫ (↑H.toPrelaxFunctor).map g)).hom ≫
                      η.app a ◁ (α_ ((↑G.toPrelaxFunctor).map f) (θ.app b) ((↑H.toPrelaxFunctor).map g)).inv) ≫
                    η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫
                      η.app a ◁ (α_ (θ.app a) ((↑H.toPrelaxFunctor).map f) ((↑H.toPrelaxFunctor).map g)).hom ≫
                        (α_ (η.app a) (θ.app a) ((↑H.toPrelaxFunctor).map f ≫ (↑H.toPrelaxFunctor).map g)).inv
[PROOFSTEP]
rw [whisker_exchange_assoc]
  -- Porting note: this used to be just `simp`
[GOAL]
case calc_6
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (fun {a b} f =>
          (α_ ((↑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 ≫ g) ≫
      (fun a => η.app a ≫ θ.app a) a ◁ OplaxFunctor.mapComp H f g =
    (α_ ((↑F.toPrelaxFunctor).map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ((α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (η.app c)).hom ▷ θ.app c ≫
            (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ η.app c) (θ.app c)).hom) ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ((↑F.toPrelaxFunctor).map f ◁ (α_ (η.app b) ((↑G.toPrelaxFunctor).map g) (θ.app c)).hom ≫
                (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) ((↑G.toPrelaxFunctor).map g ≫ θ.app c)).inv) ≫
              naturality η f ▷ ((↑G.toPrelaxFunctor).map g ≫ θ.app c) ≫
                (η.app a ≫ (↑G.toPrelaxFunctor).map f) ◁ naturality θ g ≫
                  ((α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (θ.app b ≫ (↑H.toPrelaxFunctor).map g)).hom ≫
                      η.app a ◁ (α_ ((↑G.toPrelaxFunctor).map f) (θ.app b) ((↑H.toPrelaxFunctor).map g)).inv) ≫
                    η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫
                      η.app a ◁ (α_ (θ.app a) ((↑H.toPrelaxFunctor).map f) ((↑H.toPrelaxFunctor).map g)).hom ≫
                        (α_ (η.app a) (θ.app a) ((↑H.toPrelaxFunctor).map f ≫ (↑H.toPrelaxFunctor).map g)).inv
[PROOFSTEP]
simp only [comp_whiskerLeft, assoc, Iso.inv_hom_id_assoc, whiskerLeft_naturality_comp_assoc,
  whiskerRight_naturality_comp_assoc, pentagon_assoc, whiskerRight_comp, pentagon_hom_inv_inv_inv_inv_assoc]
[GOAL]
case calc_7
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : OplaxFunctor B C
η✝ : OplaxNatTrans F G
θ✝ : OplaxNatTrans G H
η : OplaxNatTrans F G
θ : OplaxNatTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ ((↑F.toPrelaxFunctor).map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      OplaxFunctor.mapComp F f g ▷ η.app c ▷ θ.app c ≫
        ((α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) (η.app c)).hom ▷ θ.app c ≫
            (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g ≫ η.app c) (θ.app c)).hom) ≫
          (↑F.toPrelaxFunctor).map f ◁ naturality η g ▷ θ.app c ≫
            ((↑F.toPrelaxFunctor).map f ◁ (α_ (η.app b) ((↑G.toPrelaxFunctor).map g) (θ.app c)).hom ≫
                (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) ((↑G.toPrelaxFunctor).map g ≫ θ.app c)).inv) ≫
              ((↑F.toPrelaxFunctor).map f ≫ η.app b) ◁ naturality θ g ≫
                naturality η f ▷ (θ.app b ≫ (↑H.toPrelaxFunctor).map g) ≫
                  ((α_ (η.app a) ((↑G.toPrelaxFunctor).map f) (θ.app b ≫ (↑H.toPrelaxFunctor).map g)).hom ≫
                      η.app a ◁ (α_ ((↑G.toPrelaxFunctor).map f) (θ.app b) ((↑H.toPrelaxFunctor).map g)).inv) ≫
                    η.app a ◁ naturality θ f ▷ (↑H.toPrelaxFunctor).map g ≫
                      η.app a ◁ (α_ (θ.app a) ((↑H.toPrelaxFunctor).map f) ((↑H.toPrelaxFunctor).map g)).hom ≫
                        (α_ (η.app a) (θ.app a) ((↑H.toPrelaxFunctor).map f ≫ (↑H.toPrelaxFunctor).map g)).inv =
    OplaxFunctor.mapComp F f g ▷ (fun a => η.app a ≫ θ.app a) c ≫
      (α_ ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g) ((fun a => η.app a ≫ θ.app a) c)).hom ≫
        (↑F.toPrelaxFunctor).map f ◁
            (fun {a b} f =>
                (α_ ((↑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)
              g ≫
          (α_ ((↑F.toPrelaxFunctor).map f) ((fun a => η.app a ≫ θ.app a) b) ((↑H.toPrelaxFunctor).map g)).inv ≫
            (fun {a b} f =>
                    (α_ ((↑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 ▷
                (↑H.toPrelaxFunctor).map g ≫
              (α_ ((fun a => η.app a ≫ θ.app a) a) ((↑H.toPrelaxFunctor).map f) ((↑H.toPrelaxFunctor).map g)).hom
[PROOFSTEP]
simp
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η θ ι : F ⟶ G
Γ : Modification η θ
a b c : B
a' : C
f : a' ⟶ (↑F.toPrelaxFunctor).obj b
g : b ⟶ c
⊢ f ◁ (↑F.toPrelaxFunctor).map g ◁ Γ.app c ≫ f ◁ OplaxNatTrans.naturality θ g =
    f ◁ OplaxNatTrans.naturality η g ≫ f ◁ Γ.app b ▷ (↑G.toPrelaxFunctor).map g
[PROOFSTEP]
simp_rw [← whiskerLeft_comp, naturality]
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η θ ι : F ⟶ G
Γ : Modification η θ
a b c : B
a' : C
f : a ⟶ b
g : (↑G.toPrelaxFunctor).obj b ⟶ a'
⊢ (↑F.toPrelaxFunctor).map f ◁ Γ.app b ▷ g ≫
      (α_ ((↑F.toPrelaxFunctor).map f) (θ.app b) g).inv ≫ OplaxNatTrans.naturality θ f ▷ g =
    (α_ ((↑F.toPrelaxFunctor).map f) (η.app b) g).inv ≫
      OplaxNatTrans.naturality η f ▷ g ≫ Γ.app a ▷ (↑G.toPrelaxFunctor).map f ▷ g
[PROOFSTEP]
simp_rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight, naturality]
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η θ ι : F ⟶ G
Γ : Modification η θ
Δ : Modification θ ι
⊢ ∀ {a b : B} (f : a ⟶ b),
    (↑F.toPrelaxFunctor).map f ◁ (fun a => Γ.app a ≫ Δ.app a) b ≫ OplaxNatTrans.naturality ι f =
      OplaxNatTrans.naturality η f ≫ (fun a => Γ.app a ≫ Δ.app a) a ▷ (↑G.toPrelaxFunctor).map f
[PROOFSTEP]
intros
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η θ ι : F ⟶ G
Γ : Modification η θ
Δ : Modification θ ι
a✝ b✝ : B
f✝ : a✝ ⟶ b✝
⊢ (↑F.toPrelaxFunctor).map f✝ ◁ (fun a => Γ.app a ≫ Δ.app a) b✝ ≫ OplaxNatTrans.naturality ι f✝ =
    OplaxNatTrans.naturality η f✝ ≫ (fun a => Γ.app a ≫ Δ.app a) a✝ ▷ (↑G.toPrelaxFunctor).map f✝
[PROOFSTEP]
simp only [whiskerLeft_comp, assoc, naturality, naturality_assoc, comp_whiskerRight]
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F✝ G✝ : OplaxFunctor B C
η θ ι : F✝ ⟶ G✝
F G : OplaxFunctor B C
α β : F ⟶ G
m n : α ⟶ β
w : ∀ (b : B), m.app b = n.app b
⊢ m = n
[PROOFSTEP]
apply Modification.ext
[GOAL]
case app
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F✝ G✝ : OplaxFunctor B C
η θ ι : F✝ ⟶ G✝
F G : OplaxFunctor B C
α β : F ⟶ G
m n : α ⟶ β
w : ∀ (b : B), m.app b = n.app b
⊢ m.app = n.app
[PROOFSTEP]
ext
[GOAL]
case app.h
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F✝ G✝ : OplaxFunctor B C
η θ ι : F✝ ⟶ G✝
F G : OplaxFunctor B C
α β : F ⟶ G
m n : α ⟶ β
w : ∀ (b : B), m.app b = n.app b
x✝ : B
⊢ m.app x✝ = n.app x✝
[PROOFSTEP]
apply w
[GOAL]
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η θ ι : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality :
  ∀ {a b : B} (f : a ⟶ b),
    (↑F.toPrelaxFunctor).map f ◁ (app b).hom ≫ CategoryTheory.OplaxNatTrans.naturality θ f =
      CategoryTheory.OplaxNatTrans.naturality η f ≫ (app a).hom ▷ (↑G.toPrelaxFunctor).map f
a b : B
f : a ⟶ b
⊢ (↑F.toPrelaxFunctor).map f ◁ (fun a => (app a).inv) b ≫ CategoryTheory.OplaxNatTrans.naturality η f =
    CategoryTheory.OplaxNatTrans.naturality θ f ≫ (fun a => (app a).inv) a ▷ (↑G.toPrelaxFunctor).map f
[PROOFSTEP]
simpa using congr_arg (fun f => _ ◁ (app b).inv ≫ f ≫ (app a).inv ▷ _) (naturality f).symm