awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
⊢ whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ
have h₁ : ∀ (a_1 : B), (whiskerLeft f θ ≫ whiskerRight η i).as.app a_1 = (whiskerRight η h ≫ whiskerLeft g θ).as.app a_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
⊢ F.map f ◁ η.app b ◁ Γ.as.app b ≫ (η ≫ ι).naturality f = (η ≫ θ).naturality f ≫ (η.app a ◁ Γ.as.app a) ▷ H.map f
have 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
Tactic: dsimp only [comp_app, comp_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
⊢ 𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
      ((F.map f ≫ η.app b) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫
        η.app a ◁ ι.naturality f ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) =
    𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map f ◁ Γ.as.app b ≫ ι.naturality f) ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f)
have rw : 𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
    (η.naturality f ▷ θ.app b ≫ (η.app a ≫ G.map f) ◁ Γ.as.app b) ⊗≫
      η.app a ◁ ι.naturality f ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) =
  𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
    η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map f ◁ Γ.as.app b ≫ ι.naturality f) ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f)
Tactic: rw [whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
⊢ 𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫
        η.app a ◁ (G.map f ◁ Γ.as.app b ≫ ι.naturality f) ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) =
    ((α_ (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
have rw : 𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
    η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (θ.naturality f ≫ Γ.as.app a ▷ H.map f) ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) =
  ((α_ (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
Tactic: rw [Γ.as.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
⊢ 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
have _ : 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) ⊗≫
    ((F.map f ≫ η.app b) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫
      η.app a ◁ ι.naturality f ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f)
Tactic: calc
        _ = 𝟙 _ ⊗≫ ((F.map f ≫ η.app b) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫
            η.app a ◁ ι.naturality f ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map f ◁ Γ.as.app b ≫
            ι.naturality f) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]
          bicategory
        _ = _ := by
          rw [Γ.as.naturality]
          bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
_ :
  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) ⊗≫
      ((F.map f ≫ η.app b) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫
        η.app a ◁ ι.naturality f ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f)
⊢ 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
have _₁ : 𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
    ((F.map f ≫ η.app b) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫
      η.app a ◁ ι.naturality f ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) =
  𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
    η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map f ◁ Γ.as.app b ≫ ι.naturality f) ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f)
Tactic: calc
        _ = 𝟙 _ ⊗≫ ((F.map f ≫ η.app b) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫
            η.app a ◁ ι.naturality f ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map f ◁ Γ.as.app b ≫
            ι.naturality f) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]
          bicategory
        _ = _ := by
          rw [Γ.as.naturality]
          bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
_ :
  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) ⊗≫
      ((F.map f ≫ η.app b) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫
        η.app a ◁ ι.naturality f ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f)
_₁ :
  𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
      ((F.map f ≫ η.app b) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫
        η.app a ◁ ι.naturality f ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) =
    𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map f ◁ Γ.as.app b ≫ ι.naturality f) ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f)
⊢ 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
have _₂ : 𝟙 (F.map f ≫ η.app b ≫ θ.app b) ⊗≫
    η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map f ◁ Γ.as.app b ≫ ι.naturality f) ⊗≫ 𝟙 ((η.app a ≫ ι.app a) ≫ H.map f) =
  ((α_ (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
Tactic: calc
        _ = 𝟙 _ ⊗≫ ((F.map f ≫ η.app b) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫
            η.app a ◁ ι.naturality f ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map f ◁ Γ.as.app b ≫
            ι.naturality f) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]
          bicategory
        _ = _ := by
          rw [Γ.as.naturality]
          bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫ (θ ≫ ι).naturality f = (η ≫ ι).naturality f ≫ Γ.as.app a ▷ ι.app a ▷ H.map f
have dsimp : F.map f ◁ Γ.as.app b ▷ ι.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) ≫
    Γ.as.app a ▷ ι.app a ▷ H.map f
Tactic: dsimp only [comp_app, comp_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
⊢ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
      (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫
        θ.app a ◁ ι.naturality f ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
    𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
      η.naturality f ▷ ι.app b ⊗≫
        (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f)
have rw : 𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
    (η.naturality f ≫ Γ.as.app a ▷ G.map f) ▷ ι.app b ⊗≫ θ.app a ◁ ι.naturality f ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
  𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
    η.naturality f ▷ ι.app b ⊗≫
      (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f)
Tactic: rw [Γ.as.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
⊢ 𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
      η.naturality f ▷ ι.app b ⊗≫
        (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
    ((α_ (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) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f
have rw : 𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
    η.naturality f ▷ ι.app b ⊗≫
      (η.app a ◁ ι.naturality f ≫ Γ.as.app a ▷ (ι.app a ≫ H.map f)) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
  ((α_ (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) ≫
    Γ.as.app a ▷ ι.app a ▷ H.map f
Tactic: rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
⊢ F.map f ◁ Γ.as.app b ▷ ι.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) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f
have _ : F.map f ◁ Γ.as.app b ▷ ι.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) ⊗≫
    (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫ θ.app a ◁ ι.naturality f ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f)
Tactic: calc
        _ = 𝟙 _ ⊗≫ (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫
              θ.app a ◁ ι.naturality f ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.naturality f ▷ ι.app b ⊗≫ (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫
              θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 _ := by
          rw [Γ.as.naturality]
          bicategory
        _ = _ := by
          rw [← whisker_exchange]
          bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
_ :
  F.map f ◁ Γ.as.app b ▷ ι.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) ⊗≫
      (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫ θ.app a ◁ ι.naturality f ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f)
⊢ F.map f ◁ Γ.as.app b ▷ ι.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) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f
have _₁ : 𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
    (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫ θ.app a ◁ ι.naturality f ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
  𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
    η.naturality f ▷ ι.app b ⊗≫
      (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f)
Tactic: calc
        _ = 𝟙 _ ⊗≫ (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫
              θ.app a ◁ ι.naturality f ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.naturality f ▷ ι.app b ⊗≫ (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫
              θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 _ := by
          rw [Γ.as.naturality]
          bicategory
        _ = _ := by
          rw [← whisker_exchange]
          bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
_ :
  F.map f ◁ Γ.as.app b ▷ ι.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) ⊗≫
      (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫ θ.app a ◁ ι.naturality f ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f)
_₁ :
  𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
      (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫
        θ.app a ◁ ι.naturality f ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
    𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
      η.naturality f ▷ ι.app b ⊗≫
        (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f)
⊢ F.map f ◁ Γ.as.app b ▷ ι.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) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f
have _₂ : 𝟙 (F.map f ≫ η.app b ≫ ι.app b) ⊗≫
    η.naturality f ▷ ι.app b ⊗≫
      (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 ((θ.app a ≫ ι.app a) ≫ H.map f) =
  ((α_ (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) ≫
    Γ.as.app a ▷ ι.app a ▷ H.map f
Tactic: calc
        _ = 𝟙 _ ⊗≫ (F.map f ◁ Γ.as.app b ≫ θ.naturality f) ▷ ι.app b ⊗≫
              θ.app a ◁ ι.naturality f ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.naturality f ▷ ι.app b ⊗≫ (Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫
              θ.app a ◁ ι.naturality f) ⊗≫ 𝟙 _ := by
          rw [Γ.as.naturality]
          bicategory
        _ = _ := by
          rw [← whisker_exchange]
          bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax (goal)
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
⊢ F.map f ◁ Iso.hom ((fun (a : B) ↦ α_ (η.app a) (θ.app a) (ι.app a)) b) ≫ (η ≫ θ ≫ ι).naturality f =
    ((η ≫ θ) ≫ ι).naturality f ≫ Iso.hom ((fun (a : B) ↦ α_ (η.app a) (θ.app a) (ι.app a)) a) ▷ I.map f
have dsimp : F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom ≫
    (α_ (F.map f) (η.app b) (θ.app b ≫ ι.app b)).inv ≫
      η.naturality f ▷ (θ.app b ≫ ι.app b) ≫
        (α_ (η.app a) (G.map f) (θ.app b ≫ ι.app b)).hom ≫
          η.app a ◁
              ((α_ (G.map f) (θ.app b) (ι.app b)).inv ≫
                θ.naturality f ▷ ι.app b ≫
                  (α_ (θ.app a) (H.map f) (ι.app b)).hom ≫
                    θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (I.map f)).inv) ≫
            (α_ (η.app a) (θ.app a ≫ ι.app a) (I.map f)).inv =
  ((α_ (F.map f) (η.app b ≫ θ.app b) (ι.app b)).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 b ≫
        (α_ (η.app a ≫ θ.app a) (H.map f) (ι.app b)).hom ≫
          (η.app a ≫ θ.app a) ◁ ι.naturality f ≫ (α_ (η.app a ≫ θ.app a) (ι.app a) (I.map f)).inv) ≫
    (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f
Tactic: dsimp only [comp_app, comp_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : OplaxFunctor.{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 ≫ (η ≫ ι).naturality f = (η ≫ θ).naturality f ≫ F.map f ◁ η.app b ◁ Γ.as.app b
have 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
Tactic: dsimp only [comp_app, comp_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : OplaxFunctor.{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 ◁ (Γ.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)
have 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)
Tactic: rw [Γ.as.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H I : OplaxFunctor.{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 ⊗≫
        ((η.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
have 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
Tactic: rw [whisker_exchange]