awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ≫
      (α_ (η.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
have _ : (η.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: 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
-- 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 ≫
      (α_ (η.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 ◁ Γ.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
have _₁ : 𝟙 ((η.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: 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
-- 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 ≫
      (α_ (η.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 ◁ Γ.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
have _₂ : 𝟙 ((η.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: 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
-- 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
⊢ Γ.as.app a ▷ ι.app a ▷ H.map f ≫ (θ ≫ ι).naturality f = (η ≫ ι).naturality f ≫ F.map f ◁ Γ.as.app b ▷ ι.app b
have 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
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) ⊗≫
      (Γ.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)
have 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)
Tactic: rw [← whisker_exchange]
-- 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 ⊗≫ (Γ.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
have 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
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
⊢ Γ.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
have _ : Γ.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: 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
-- 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
_ :
  Γ.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)
⊢ Γ.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
have _₁ : 𝟙 ((η.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: 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
-- 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
_ :
  Γ.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)
⊢ Γ.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
have _₂ : 𝟙 ((η.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: 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
-- 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
ι : H ⟶ I
a b : B
f : a ⟶ b
⊢ 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)
have 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
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 a b c : OplaxFunctor.{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.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
⊢ 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
-- 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
⊢ 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 rw : (α_ (F.map f) (η.app b) (θ.app b)).inv ≫
    η.naturality f ▷ θ.app b ≫
      (η.app a ≫ G.map f) ◁ Γ.as.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: rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc]
-- 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
⊢ 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
-- 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
⊢ 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 simp_rw : 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 ≫
        Γ.as.app a ▷ (G.map f ≫ ι.app b) ≫ θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv
Tactic: simp_rw [assoc, ← associator_inv_naturality_left, whisker_exchange_assoc]
-- 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 a b c : OplaxFunctor.{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 w : ∀ (b_1 : B), (whiskerLeft f θ ≫ whiskerRight η i).as.app b_1 = (whiskerRight η h ≫ whiskerLeft g θ).as.app b_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo (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 : Pseudofunctor.{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).hom =
    ((η ≫ θ).naturality f).hom ≫ (η.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).hom ▷ ι.app b ≫
        (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
          η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
  ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
      (η.naturality f).hom ▷ θ.app b ≫
        (α_ (η.app a) (G.map f) (θ.app b)).hom ≫
          η.app a ◁ (θ.naturality f).hom ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
    (η.app a ◁ Γ.as.app a) ▷ H.map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo (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 : Pseudofunctor.{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).hom ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
            η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        (η.naturality f).hom ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫
            η.app a ◁ (θ.naturality f).hom ≫ (α_ (η.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)).inv ≫
    (η.naturality f).hom ▷ θ.app b ≫
      (η.app a ≫ G.map f) ◁ Γ.as.app b ≫
        (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
          η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
  ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
      (η.naturality f).hom ▷ θ.app b ≫
        (α_ (η.app a) (G.map f) (θ.app b)).hom ≫
          η.app a ◁ (θ.naturality f).hom ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
    (η.app a ◁ Γ.as.app a) ▷ H.map f
Tactic: rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc]