mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case right_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F ((Hom₂.right_unitor_inv f✝).vcomp (Hom₂.right_unitor f✝)) = liftHom₂ F (Hom₂.id f✝)

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case pentagon
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ e✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
i✝ : Hom d✝ e✝
⊢ liftHom₂ F
      ((Hom₂.whisker_right i✝ (Hom₂.associator f✝ g✝ h✝)).vcomp
        ((Hom₂.associator f✝ (g✝.comp h✝) i✝).vcomp (Hom₂.whisker_left f✝ (Hom₂.associator g✝ h✝ i✝)))) =
    liftHom₂ F ((Hom₂.associator (f✝.comp g✝) h✝ i✝).vcomp (Hom₂.associator f✝ g✝ (h✝.comp i✝)))

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case triangle
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ liftHom₂ F ((Hom₂.associator f✝ (Hom.id b✝) g✝).vcomp (Hom₂.whisker_left f✝ (Hom₂.left_unitor g✝))) =
    liftHom₂ F (Hom₂.whisker_right g✝ (Hom₂.right_unitor f✝))

Tactic:
(dsimp [liftHom₂]; cat_disch)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.inv ▷ α.app b ≫ (α.naturality f).hom ≫ α.app a ◁ G.map₂ η.hom =
    (F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η).hom

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.inv ▷ α.app b ≫ (α.naturality f).hom ≫ α.app a ◁ G.map₂ η.hom =
    (F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η).hom
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫ (η.app a ◁ G.map₂ β ≫ η.naturality g) ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.naturality f ≫ G.map₂ β ▷ θ.app b) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b)

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫ (η.app a ◁ G.map₂ β ≫ η.naturality g) ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.naturality f ≫ G.map₂ β ▷ θ.app b) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.app a ◁ H.map₂ β ≫ θ.naturality g) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
    η.vCompApp θ a ◁ H.map₂ β ≫ η.vCompNaturality θ g

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.app a ◁ H.map₂ β ≫ θ.naturality g) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
    η.vCompApp θ a ◁ H.map₂ β ≫ η.vCompNaturality θ g
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫ (η.app a ◁ G.map₂ β ≫ η.naturality g) ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.naturality f ≫ G.map₂ β ▷ θ.app b) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b)

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫ (η.app a ◁ G.map₂ β ≫ η.naturality g) ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.naturality f ≫ G.map₂ β ▷ θ.app b) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      η.app a ◁ ((ρ_ (θ.app a)).hom ≫ (λ_ (θ.app a)).inv ≫ G.mapId a ▷ θ.app a) ⊗≫
        η.naturality (𝟙 a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a)

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      η.app a ◁ ((ρ_ (θ.app a)).hom ≫ (λ_ (θ.app a)).inv ≫ G.mapId a ▷ θ.app a) ⊗≫
        η.naturality (𝟙 a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.app a ◁ H.map₂ β ≫ θ.naturality g) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
    η.vCompApp θ a ◁ H.map₂ β ≫ η.vCompNaturality θ g

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.app a ◁ H.map₂ β ≫ θ.naturality g) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
    η.vCompApp θ a ◁ H.map₂ β ≫ η.vCompNaturality θ g
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      ((ρ_ (η.app a)).hom ≫ (λ_ (η.app a)).inv ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv ≫ F.mapId a ▷ η.vCompApp θ a

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      ((ρ_ (η.app a)).hom ≫ (λ_ (η.app a)).inv ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv ≫ F.mapId a ▷ η.vCompApp θ a
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ θ.naturality (𝟙 a) ⊗≫
        (η.app a ◁ G.mapId a ≫ (ρ_ (η.app a)).hom ≫ (λ_ (η.app a)).inv) ▷ θ.app a ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ (θ.naturality (𝟙 a) ≫ G.mapId a ▷ θ.app a) ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a)

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ θ.naturality (𝟙 a) ⊗≫
        (η.app a ◁ G.mapId a ≫ (ρ_ (η.app a)).hom ≫ (λ_ (η.app a)).inv) ▷ θ.app a ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ (θ.naturality (𝟙 a) ≫ G.mapId a ▷ θ.app a) ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁
          ((α_ (θ.app a) (H.map f) (H.map g)).inv ≫
            θ.naturality f ▷ H.map g ≫
              (α_ (G.map f) (θ.app b) (H.map g)).hom ≫
                G.map f ◁ θ.naturality g ≫ (α_ (G.map f) (G.map g) (θ.app c)).inv ≫ G.mapComp f g ▷ θ.app c) ⊗≫
        η.naturality (f ≫ g) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁
          ((α_ (θ.app a) (H.map f) (H.map g)).inv ≫
            θ.naturality f ▷ H.map g ≫
              (α_ (G.map f) (θ.app b) (H.map g)).hom ≫
                G.map f ◁ θ.naturality g ≫ (α_ (G.map f) (G.map g) (θ.app c)).inv ≫ G.mapComp f g ▷ θ.app c) ⊗≫
        η.naturality (f ≫ g) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapId a ≫ (ρ_ (θ.app a)).hom ≫ (λ_ (θ.app a)).inv) ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) =
    η.vCompApp θ a ◁ H.mapId a ≫ (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapId a ≫ (ρ_ (θ.app a)).hom ≫ (λ_ (θ.app a)).inv) ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) =
    η.vCompApp θ a ◁ H.mapId a ≫ (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ θ.naturality (f ≫ g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫
              (α_ (η.app a) (G.map f) (G.map g)).inv ≫
                η.naturality f ▷ G.map g ≫
                  (α_ (F.map f) (η.app b) (G.map g)).hom ≫
                    F.map f ◁ η.naturality g ≫ (α_ (F.map f) (F.map g) (η.app c)).inv) ▷
            θ.app c ⊗≫
          𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ (θ.naturality (f ≫ g) ≫ G.mapComp f g ▷ θ.app c) ⊗≫
        (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c)

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ θ.naturality (f ≫ g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫
              (α_ (η.app a) (G.map f) (G.map g)).inv ≫
                η.naturality f ▷ G.map g ≫
                  (α_ (F.map f) (η.app b) (G.map g)).hom ≫
                    F.map f ◁ η.naturality g ≫ (α_ (F.map f) (F.map g) (η.app c)).inv) ▷
            θ.app c ⊗≫
          𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ (θ.naturality (f ≫ g) ≫ G.mapComp f g ▷ θ.app c) ⊗≫
        (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        ((α_ (η.app a) (G.map f) (G.map g)).inv ≫
              η.naturality f ▷ G.map g ≫
                (α_ (F.map f) (η.app b) (G.map g)).hom ≫
                  F.map f ◁ η.naturality g ≫ (α_ (F.map f) (F.map g) (η.app c)).inv ≫ F.mapComp f g ▷ η.app c) ▷
            θ.app c ⊗≫
          𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ θ.naturality f ▷ H.map g ⊗≫
        ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
            F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        ((α_ (η.app a) (G.map f) (G.map g)).inv ≫
              η.naturality f ▷ G.map g ≫
                (α_ (F.map f) (η.app b) (G.map g)).hom ≫
                  F.map f ◁ η.naturality g ≫ (α_ (F.map f) (F.map g) (η.app c)).inv ≫ F.mapComp f g ▷ η.app c) ▷
            θ.app c ⊗≫
          𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ θ.naturality f ▷ H.map g ⊗≫
        ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
            F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.naturality f ≫ G.map f ◁ Γ.as.app b) ⊗≫ η.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫
        ((η.app a ≫ G.map f) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b)

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.naturality f ≫ G.map f ◁ Γ.as.app b) ⊗≫ η.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫
        ((η.app a ≫ G.map f) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b)
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫
        (η.naturality f ▷ θ.app b ≫ (F.map f ≫ η.app b) ◁ Γ.as.app b) ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) =
    ((α_ (η.app a) (θ.app a) (H.map f)).hom ≫
        η.app a ◁ θ.naturality f ≫
          (α_ (η.app a) (G.map f) (θ.app b)).inv ≫ η.naturality f ▷ θ.app b ≫ (α_ (F.map f) (η.app b) (θ.app b)).hom) ≫
      F.map f ◁ η.app b ◁ Γ.as.app b

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫
        (η.naturality f ▷ θ.app b ≫ (F.map f ≫ η.app b) ◁ Γ.as.app b) ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) =
    ((α_ (η.app a) (θ.app a) (H.map f)).hom ≫
        η.app a ◁ θ.naturality f ≫
          (α_ (η.app a) (G.map f) (θ.app b)).inv ≫ η.naturality f ▷ θ.app b ≫ (α_ (F.map f) (η.app b) (θ.app b)).hom) ≫
      F.map f ◁ η.app b ◁ Γ.as.app b
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ θ.naturality f ▷ H.map g ⊗≫
        (η.naturality f ▷ (θ.app b ≫ H.map g) ≫ (F.map f ≫ η.app b) ◁ θ.naturality g) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
            F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
      η.vCompNaturality θ f ▷ H.map g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
          F.map f ◁ η.vCompNaturality θ g ≫
            (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv ≫ F.mapComp f g ▷ η.vCompApp θ c

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ θ.naturality f ▷ H.map g ⊗≫
        (η.naturality f ▷ (θ.app b ≫ H.map g) ≫ (F.map f ≫ η.app b) ◁ θ.naturality g) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
            F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
      η.vCompNaturality θ f ▷ H.map g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
          F.map f ◁ η.vCompNaturality θ g ≫
            (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv ≫ F.mapComp f g ▷ η.vCompApp θ c
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁
          (θ.app a ◁ H.mapComp f g ≫
            (α_ (θ.app a) (H.map f) (H.map g)).inv ≫
              θ.naturality f ▷ H.map g ≫
                (α_ (G.map f) (θ.app b) (H.map g)).hom ≫
                  G.map f ◁ θ.naturality g ≫ (α_ (G.map f) (G.map g) (θ.app c)).inv) ⊗≫
        (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapComp f g ⊗≫ θ.naturality f ▷ H.map g) ⊗≫
        ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c)

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁
          (θ.app a ◁ H.mapComp f g ≫
            (α_ (θ.app a) (H.map f) (H.map g)).inv ≫
              θ.naturality f ▷ H.map g ≫
                (α_ (G.map f) (θ.app b) (H.map g)).hom ≫
                  G.map f ◁ θ.naturality g ≫ (α_ (G.map f) (G.map g) (θ.app c)).inv) ⊗≫
        (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapComp f g ⊗≫ θ.naturality f ▷ H.map g) ⊗≫
        ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c)
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapComp f g ⊗≫ θ.naturality f ▷ H.map g) ⊗≫
        (η.naturality f ▷ (θ.app b ≫ H.map g) ≫ (F.map f ≫ η.app b) ◁ θ.naturality g) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) =
    η.vCompApp θ a ◁ H.mapComp f g ≫
      (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫
          (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
            F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapComp f g ⊗≫ θ.naturality f ▷ H.map g) ⊗≫
        (η.naturality f ▷ (θ.app b ≫ H.map g) ≫ (F.map f ≫ η.app b) ◁ θ.naturality g) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) =
    η.vCompApp θ a ◁ H.mapComp f g ≫
      (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫
          (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
            F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (η.app a ◁ ι.naturality f ≫ Γ.as.app a ▷ (G.map f ≫ ι.app b)) ⊗≫
        θ.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b) =
    𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (η.app a ◁ ι.naturality f ⊗≫ (Γ.as.app a ▷ G.map f ≫ θ.naturality f) ▷ ι.app b) ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b)

Tactic:
]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (η.app a ◁ ι.naturality f ≫ Γ.as.app a ▷ (G.map f ≫ ι.app b)) ⊗≫
        θ.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b) =
    𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (η.app a ◁ ι.naturality f ⊗≫ (Γ.as.app a ▷ G.map f ≫ θ.naturality f) ▷ ι.app b) ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b)