awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x y : B
f g : x ⟶ y
η : f ⟶ g
⊢ F.toStrictlyUnitaryLaxFunctor.map₂ η = F.map₂ η

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x y z : B
f : x ⟶ y
g : y ⟶ z
⊢ F.toStrictlyUnitaryLaxFunctor.mapComp f g = (F.mapComp f g).inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x : B
⊢ F.toStrictlyUnitaryLaxFunctor.mapId x = (F.mapId x).inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 F : StrictlyUnitaryPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryPseudofunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
x : B
⊢ (F.comp G.toPseudofunctor).map (𝟙 x) = 𝟙 ((F.comp G.toPseudofunctor).obj x)

Tactic:
simp [StrictlyUnitaryPseudofunctor.map_id]

Premises used: CategoryTheory.StrictlyUnitaryPseudofunctor.map_id
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 F : StrictlyUnitaryPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryPseudofunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
x : B
w : ((F.comp G.toPseudofunctor).mapId x).hom = Iso.hom (eqToIso ⋯)
⊢ (F.comp G.toPseudofunctor).mapId x = eqToIso ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 F : StrictlyUnitaryPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryPseudofunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
x : B
⊢ ((F.comp G.toPseudofunctor).mapId x).hom = Iso.hom (eqToIso ⋯)

Tactic:
simp [StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso,
      PrelaxFunctor.map₂_eqToHom]

Premises used: CategoryTheory.PrelaxFunctor.map₂_eqToHom, CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
dsimp :
  (η.app a ◁ Γ.as.app a) ▷ H.map f ≫
      (α_ (η.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 =
    ((α_ (η.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
⊢ (η.app a ◁ Γ.as.app a) ▷ H.map f ≫ (η ≫ ι).naturality f = (η ≫ θ).naturality f ≫ F.map f ◁ η.app b ◁ Γ.as.app b

Tactic:
dsimp only [comp_app, comp_naturality]

Premises used: CategoryTheory.Lax.LaxTrans.comp_naturality, CategoryTheory.Lax.LaxTrans.comp_app
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (η.app a ◁ Γ.as.app a) ▷ H.map f ≫
      (α_ (η.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 =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (Γ.as.app a ▷ H.map f ≫ ι.naturality f) ⊗≫ η.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
rw :
  𝟙 ((η.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)
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (Γ.as.app a ▷ H.map f ≫ ι.naturality f) ⊗≫ η.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:
rw [Γ.as.naturality]

Premises used: CategoryTheory.Lax.LaxTrans.Hom.as, CategoryTheory.Lax.LaxTrans.Modification.naturality
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} 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:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
rw :
  𝟙 ((η.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
⊢ 𝟙 ((η.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) =
    ((α_ (η.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:
rw [whisker_exchange]

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} 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:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
_ :
  (η.app a ◁ Γ.as.app a) ▷ H.map f ≫
      (α_ (η.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 =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (Γ.as.app a ▷ H.map f ≫ ι.naturality f) ⊗≫ η.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ η.app b ≫ ι.app b)
_₁ :
  𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (Γ.as.app a ▷ H.map f ≫ ι.naturality f) ⊗≫ η.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)
_₂ :
  𝟙 ((η.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) =
    ((α_ (η.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
⊢ (η.app a ◁ Γ.as.app a) ▷ H.map f ≫
      (α_ (η.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 =
    ((α_ (η.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:
calc
        _ = 𝟙 _ ⊗≫ η.app a ◁ ((Γ.as.app a ▷ H.map f ≫ ι.naturality f)) ⊗≫
              η.naturality f ▷ (ι.app b) ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality f ⊗≫
              ((η.app a ≫ G.map f) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫ 𝟙 _ := by
          rw [Γ.as.naturality]
          bicategory
        _ = _ := by
          rw [whisker_exchange]
          bicategory

Premises used: CategoryTheory.Lax.LaxTrans.Modification.app, CategoryTheory.Lax.LaxTrans.Hom.as, CategoryTheory.Lax.LaxTrans.naturality, CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct, CategoryTheory.Lax.LaxTrans.app, CategoryTheory.LaxFunctor.toPrelaxFunctor, Prefunctor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.PrelaxFunctorStruct.toPrefunctor, CategoryTheory.Bicategory.whiskerLeft
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
dsimp :
  Γ.as.app a ▷ ι.app a ▷ H.map f ≫
      (α_ (θ.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 =
    ((α_ (η.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 ◁ Γ.as.app b ▷ ι.app b
⊢ Γ.as.app a ▷ ι.app a ▷ H.map f ≫ (θ ≫ ι).naturality f = (η ≫ ι).naturality f ≫ F.map f ◁ Γ.as.app b ▷ ι.app b

Tactic:
dsimp only [comp_app, comp_naturality]

Premises used: CategoryTheory.Lax.LaxTrans.comp_naturality, CategoryTheory.Lax.LaxTrans.comp_app
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ Γ.as.app a ▷ ι.app a ▷ H.map f ≫
      (α_ (θ.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 =
    𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
        θ.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
rw :
  𝟙 ((η.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)
⊢ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
        θ.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:
rw [← whisker_exchange]

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} 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:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
rw :
  𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (η.app a ◁ ι.naturality f ⊗≫ (η.naturality f ≫ F.map f ◁ Γ.as.app b) ▷ ι.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 ◁ Γ.as.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) =
    ((α_ (η.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 ◁ Γ.as.app b ▷ ι.app b

Tactic:
rw [Γ.as.naturality]

Premises used: CategoryTheory.Lax.LaxTrans.Hom.as, CategoryTheory.Lax.LaxTrans.Modification.naturality
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} 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 ≫ F.map f ◁ Γ.as.app b) ▷ ι.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 ◁ Γ.as.app b ▷ ι.app b

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
_ :
  Γ.as.app a ▷ ι.app a ▷ H.map f ≫
      (α_ (θ.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 =
    𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
        θ.naturality f ▷ ι.app b ⊗≫ 𝟙 (F.map f ≫ θ.app b ≫ ι.app b)
_₁ :
  𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) ⊗≫
      (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
        θ.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)
_₂ :
  𝟙 ((η.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) =
    ((α_ (η.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 ◁ Γ.as.app b ▷ ι.app b
⊢ Γ.as.app a ▷ ι.app a ▷ H.map f ≫
      (α_ (θ.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 =
    ((α_ (η.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 ◁ Γ.as.app b ▷ ι.app b

Tactic:
calc
        _ = 𝟙 _ ⊗≫ (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
              θ.naturality f ▷ ι.app b ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ (η.app a ◁ ι.naturality f ⊗≫ (Γ.as.app a ▷ G.map f ≫
              θ.naturality f) ▷ ι.app b) ⊗≫ 𝟙 _ := by
          rw [← whisker_exchange]
          bicategory
        _ = _ := by
          rw [Γ.as.naturality]
          bicategory

Premises used: CategoryTheory.Lax.LaxTrans.Modification.app, CategoryTheory.Lax.LaxTrans.Hom.as, CategoryTheory.Lax.LaxTrans.naturality, CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct, CategoryTheory.Lax.LaxTrans.app, CategoryTheory.LaxFunctor.toPrelaxFunctor, Prefunctor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.PrelaxFunctorStruct.toPrefunctor, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.bicategoricalComp
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
f : a ⟶ b
dsimp :
  (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫
      (α_ (η.app a) (θ.app a ≫ ι.app a) (I.map f)).hom ≫
        η.app a ◁
            ((α_ (θ.app a) (ι.app a) (I.map f)).hom ≫
              θ.app a ◁ ι.naturality f ≫
                (α_ (θ.app a) (H.map f) (ι.app b)).inv ≫
                  θ.naturality f ▷ ι.app b ≫ (α_ (G.map f) (θ.app b) (ι.app b)).hom) ≫
          (α_ (η.app a) (G.map f) (θ.app b ≫ ι.app b)).inv ≫
            η.naturality f ▷ (θ.app b ≫ ι.app b) ≫ (α_ (F.map f) (η.app b) (θ.app b ≫ ι.app b)).hom =
    ((α_ (η.app a ≫ θ.app a) (ι.app a) (I.map f)).hom ≫
        (η.app a ≫ θ.app a) ◁ ι.naturality f ≫
          (α_ (η.app a ≫ θ.app a) (H.map f) (ι.app b)).inv ≫
            ((α_ (η.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) ▷
                ι.app b ≫
              (α_ (F.map f) (η.app b ≫ θ.app b) (ι.app b)).hom) ≫
      F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom
⊢ Iso.hom ((fun (a : B) ↦ α_ (η.app a) (θ.app a) (ι.app a)) a) ▷ I.map f ≫ (η ≫ θ ≫ ι).naturality f =
    ((η ≫ θ) ≫ ι).naturality f ≫ F.map f ◁ Iso.hom ((fun (a : B) ↦ α_ (η.app a) (θ.app a) (ι.app a)) b)

Tactic:
dsimp only [comp_app, comp_naturality]

Premises used: CategoryTheory.Lax.LaxTrans.comp_naturality, CategoryTheory.Lax.LaxTrans.comp_app
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
f : a ⟶ b
⊢ (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫
      (α_ (η.app a) (θ.app a ≫ ι.app a) (I.map f)).hom ≫
        η.app a ◁
            ((α_ (θ.app a) (ι.app a) (I.map f)).hom ≫
              θ.app a ◁ ι.naturality f ≫
                (α_ (θ.app a) (H.map f) (ι.app b)).inv ≫
                  θ.naturality f ▷ ι.app b ≫ (α_ (G.map f) (θ.app b) (ι.app b)).hom) ≫
          (α_ (η.app a) (G.map f) (θ.app b ≫ ι.app b)).inv ≫
            η.naturality f ▷ (θ.app b ≫ ι.app b) ≫ (α_ (F.map f) (η.app b) (θ.app b ≫ ι.app b)).hom =
    ((α_ (η.app a ≫ θ.app a) (ι.app a) (I.map f)).hom ≫
        (η.app a ≫ θ.app a) ◁ ι.naturality f ≫
          (α_ (η.app a ≫ θ.app a) (H.map f) (ι.app b)).inv ≫
            ((α_ (η.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) ▷
                ι.app b ≫
              (α_ (F.map f) (η.app b ≫ θ.app b) (ι.app b)).hom) ≫
      F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I a b c : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
h₁ : ∀ (a_1 : B), (whiskerLeft f θ ≫ whiskerRight η i).as.app a_1 = (whiskerRight η h ≫ whiskerLeft g θ).as.app a_1
⊢ whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I a b c : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
a_1 : B
⊢ (whiskerLeft f θ ≫ whiskerRight η i).as.app a_1 = (whiskerRight η h ≫ whiskerLeft g θ).as.app a_1

Tactic:
whisker_exchange _ _

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I a b c : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
f g : a ⟶ b
h i : b ⟶ c
η : f ⟶ g
θ : h ⟶ i
a_1 : B
⊢ (whiskerLeft f θ ≫ whiskerRight η i).as.app a_1 = (whiskerRight η h ≫ whiskerLeft g θ).as.app a_1

Tactic:
exact whisker_exchange _ _

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
dsimp :
  F.map f ◁ η.app b ◁ Γ.as.app b ≫
      (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        η.naturality f ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫ η.app a ◁ θ.naturality f ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f
⊢ F.map f ◁ η.app b ◁ Γ.as.app b ≫ (η ≫ ι).naturality f = (η ≫ θ).naturality f ≫ (η.app a ◁ Γ.as.app a) ▷ H.map f

Tactic:
dsimp only [comp_app, comp_naturality]

Premises used: CategoryTheory.Lax.OplaxTrans.comp_app, CategoryTheory.Lax.OplaxTrans.comp_naturality