Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: case obj
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
x✝ : B
⊢ ((F.comp G).comp H).obj x✝ = (F.comp (G.comp H)).obj x✝

pp: case map
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @Prefunctor.map B inst✝³.toQuiver E inst✝.toQuiver ((F.comp G).comp H).toPrefunctor ≍
    @Prefunctor.map B inst✝³.toQuiver E inst✝.toQuiver (F.comp (G.comp H)).toPrefunctor

pp: case map₂
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @PrelaxFunctorStruct.map₂ B inst✝³.toQuiver (fun a b ↦ (homCategory a b).toQuiver) E inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) ((F.comp G).comp H).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝³.toQuiver (fun a b ↦ (homCategory a b).toQuiver) E inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) (F.comp (G.comp H)).toPrelaxFunctorStruct

pp: case mapId
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ ((F.comp G).comp H).mapId ≍ (F.comp (G.comp H)).mapId

pp: case mapComp
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @LaxFunctor.mapComp B inst✝³ E inst✝ ((F.comp G).comp H).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝³ E inst✝ (F.comp (G.comp H)).toLaxFunctor

Tactic:
· simp

Goal state after:
case map
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @Prefunctor.map B inst✝³.toQuiver E inst✝.toQuiver ((F.comp G).comp H).toPrefunctor ≍
    @Prefunctor.map B inst✝³.toQuiver E inst✝.toQuiver (F.comp (G.comp H)).toPrefunctor

case map₂
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @PrelaxFunctorStruct.map₂ B inst✝³.toQuiver (fun a b ↦ (homCategory a b).toQuiver) E inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) ((F.comp G).comp H).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst✝³.toQuiver (fun a b ↦ (homCategory a b).toQuiver) E inst✝.toQuiver
      (fun a b ↦ (homCategory a b).toQuiver) (F.comp (G.comp H)).toPrelaxFunctorStruct

case mapId
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ ((F.comp G).comp H).mapId ≍ (F.comp (G.comp H)).mapId

case mapComp
B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ @LaxFunctor.mapComp B inst✝³ E inst✝ ((F.comp G).comp H).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst✝³ E inst✝ (F.comp (G.comp H)).toLaxFunctor