awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
        η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
    𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
        η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
have rw : 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
    ((α_ (F.map f) (F.map g) (η.app c)).hom ≫
          F.map f ◁ η.naturality g ≫
            (α_ (F.map f) (η.app b) (G.map g)).inv ≫
              η.naturality f ▷ G.map g ≫ (α_ (η.app a) (G.map f) (G.map g)).hom ≫ η.app a ◁ G.mapComp f g) ▷
        θ.app c ⊗≫
      η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
  𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
    (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
      η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
Tactic: rw [η.naturality_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
        η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
    𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
        (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
          η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
have rw : 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
    (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
      η.app a ◁
          ((α_ (G.map f) (G.map g) (θ.app c)).hom ≫
            G.map f ◁ θ.naturality g ≫
              (α_ (G.map f) (θ.app b) (H.map g)).inv ≫
                θ.naturality f ▷ H.map g ≫ (α_ (θ.app a) (H.map f) (H.map g)).hom ≫ θ.app a ◁ H.mapComp f g) ⊗≫
        𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
  𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
    F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
      (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
        η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
Tactic: rw [θ.naturality_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
        (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
          η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
    (α_ (F.map f) (F.map g) (η.vCompApp θ c)).hom ≫
      F.map f ◁ η.vCompNaturality θ g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).inv ≫
          η.vCompNaturality θ f ▷ H.map g ≫
            (α_ (η.vCompApp θ a) (H.map f) (H.map g)).hom ≫ η.vCompApp θ a ◁ H.mapComp f g
have rw : 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
    F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
      ((F.map f ≫ η.app b) ◁ θ.naturality g ≫ η.naturality f ▷ (θ.app b ≫ H.map g)) ⊗≫
        η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
  (α_ (F.map f) (F.map g) (η.vCompApp θ c)).hom ≫
    F.map f ◁ η.vCompNaturality θ g ≫
      (α_ (F.map f) (η.vCompApp θ b) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫ (α_ (η.vCompApp θ a) (H.map f) (H.map g)).hom ≫ η.vCompApp θ a ◁ H.mapComp f g
Tactic: rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ F.mapComp f g ▷ η.vCompApp θ c ≫ η.vCompNaturality θ (f ≫ g) =
    (α_ (F.map f) (F.map g) (η.vCompApp θ c)).hom ≫
      F.map f ◁ η.vCompNaturality θ g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).inv ≫
          η.vCompNaturality θ f ▷ H.map g ≫
            (α_ (η.vCompApp θ a) (H.map f) (H.map g)).hom ≫ η.vCompApp θ a ◁ H.mapComp f g
have _ : F.mapComp f g ▷ η.vCompApp θ c ≫ η.vCompNaturality θ (f ≫ g) =
  𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
    (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
      η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
Tactic: calc
    _ = 𝟙 _ ⊗≫ (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
          η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
          η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 _ := by
      rw [η.naturality_comp]
      bicategory
    _ = 𝟙 _ ⊗≫ F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
          (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
            η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 _ := by
      rw [θ.naturality_comp]
      bicategory
    _ = _ := by
      rw [← whisker_exchange]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
_ :
  F.mapComp f g ▷ η.vCompApp θ c ≫ η.vCompNaturality θ (f ≫ g) =
    𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
        η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
⊢ F.mapComp f g ▷ η.vCompApp θ c ≫ η.vCompNaturality θ (f ≫ g) =
    (α_ (F.map f) (F.map g) (η.vCompApp θ c)).hom ≫
      F.map f ◁ η.vCompNaturality θ g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).inv ≫
          η.vCompNaturality θ f ▷ H.map g ≫
            (α_ (η.vCompApp θ a) (H.map f) (H.map g)).hom ≫ η.vCompApp θ a ◁ H.mapComp f g
have _₁ : 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
    (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
      η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
  𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
    (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
      η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
Tactic: calc
    _ = 𝟙 _ ⊗≫ (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
          η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
          η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 _ := by
      rw [η.naturality_comp]
      bicategory
    _ = 𝟙 _ ⊗≫ F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
          (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
            η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 _ := by
      rw [θ.naturality_comp]
      bicategory
    _ = _ := by
      rw [← whisker_exchange]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
_ :
  F.mapComp f g ▷ η.vCompApp θ c ≫ η.vCompNaturality θ (f ≫ g) =
    𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
        η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
_₁ :
  𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
        η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
    𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
        η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
⊢ F.mapComp f g ▷ η.vCompApp θ c ≫ η.vCompNaturality θ (f ≫ g) =
    (α_ (F.map f) (F.map g) (η.vCompApp θ c)).hom ≫
      F.map f ◁ η.vCompNaturality θ g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).inv ≫
          η.vCompNaturality θ f ▷ H.map g ≫
            (α_ (η.vCompApp θ a) (H.map f) (H.map g)).hom ≫ η.vCompApp θ a ◁ H.mapComp f g
have _₂ : 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
    (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
      η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
  𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
    F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
      (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
        η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
Tactic: calc
    _ = 𝟙 _ ⊗≫ (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
          η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
          η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 _ := by
      rw [η.naturality_comp]
      bicategory
    _ = 𝟙 _ ⊗≫ F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
          (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
            η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 _ := by
      rw [θ.naturality_comp]
      bicategory
    _ = _ := by
      rw [← whisker_exchange]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
_ :
  F.mapComp f g ▷ η.vCompApp θ c ≫ η.vCompNaturality θ (f ≫ g) =
    𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
        η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
_₁ :
  𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
        η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
    𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
        η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
_₂ :
  𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
        η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
    𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
        (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
          η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))
⊢ F.mapComp f g ▷ η.vCompApp θ c ≫ η.vCompNaturality θ (f ≫ g) =
    (α_ (F.map f) (F.map g) (η.vCompApp θ c)).hom ≫
      F.map f ◁ η.vCompNaturality θ g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).inv ≫
          η.vCompNaturality θ f ▷ H.map g ≫
            (α_ (η.vCompApp θ a) (H.map f) (H.map g)).hom ≫ η.vCompApp θ a ◁ H.mapComp f g
have _₃ : 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
    F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
      (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
        η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
  (α_ (F.map f) (F.map g) (η.vCompApp θ c)).hom ≫
    F.map f ◁ η.vCompNaturality θ g ≫
      (α_ (F.map f) (η.vCompApp θ b) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫ (α_ (η.vCompApp θ a) (H.map f) (H.map g)).hom ≫ η.vCompApp θ a ◁ H.mapComp f g
Tactic: calc
    _ = 𝟙 _ ⊗≫ (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
          η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
          η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 _ := by
      rw [η.naturality_comp]
      bicategory
    _ = 𝟙 _ ⊗≫ F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
          (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
            η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 _ := by
      rw [θ.naturality_comp]
      bicategory
    _ = _ := by
      rw [← whisker_exchange]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} 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 ⊗≫ (η.naturality f ≫ F.map₂ β ▷ η.app b) ▷ θ.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)
have rw : 𝟙 ((η.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: rw [naturality_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} 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 ≫ G.map₂ β ▷ θ.app b) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
    η.vCompApp θ a ◁ H.map₂ β ≫ η.vCompNaturality θ g
have rw : 𝟙 ((η.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: rw [naturality_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ θ.naturality (𝟙 a) ⊗≫
        (η.naturality (𝟙 a) ≫ F.mapId a ▷ η.app a) ▷ θ.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)
have rw : 𝟙 ((η.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: rw [η.naturality_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ (θ.naturality (𝟙 a) ≫ G.mapId a ▷ θ.app a) ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) =
    η.vCompApp θ a ◁ H.mapId a ≫ (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv
have rw : 𝟙 ((η.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: rw [θ.naturality_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ η.vCompNaturality θ (𝟙 a) ≫ F.mapId a ▷ η.vCompApp θ a =
    η.vCompApp θ a ◁ H.mapId a ≫ (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv
have _ : η.vCompNaturality θ (𝟙 a) ≫ F.mapId a ▷ η.vCompApp θ a =
  𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
    η.app a ◁ θ.naturality (𝟙 a) ⊗≫
      (η.naturality (𝟙 a) ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a)
Tactic: calc
    _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality (𝟙 a) ⊗≫
          (η.naturality (𝟙 a) ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.naturality (𝟙 a) ≫ G.mapId a ▷ θ.app a) ⊗≫ 𝟙 _ := by
      rw [η.naturality_id]
      bicategory
    _ = _ := by
      rw [θ.naturality_id]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : LaxTrans F G
θ : LaxTrans G H
a : B
_ :
  η.vCompNaturality θ (𝟙 a) ≫ F.mapId a ▷ η.vCompApp θ a =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ θ.naturality (𝟙 a) ⊗≫
        (η.naturality (𝟙 a) ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a)
⊢ η.vCompNaturality θ (𝟙 a) ≫ F.mapId a ▷ η.vCompApp θ a =
    η.vCompApp θ a ◁ H.mapId a ≫ (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv
have _₁ : 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
    η.app a ◁ θ.naturality (𝟙 a) ⊗≫
      (η.naturality (𝟙 a) ≫ F.mapId a ▷ η.app a) ▷ θ.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: calc
    _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality (𝟙 a) ⊗≫
          (η.naturality (𝟙 a) ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.naturality (𝟙 a) ≫ G.mapId a ▷ θ.app a) ⊗≫ 𝟙 _ := by
      rw [η.naturality_id]
      bicategory
    _ = _ := by
      rw [θ.naturality_id]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : LaxTrans F G
θ : LaxTrans G H
a : B
_ :
  η.vCompNaturality θ (𝟙 a) ≫ F.mapId a ▷ η.vCompApp θ a =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ θ.naturality (𝟙 a) ⊗≫
        (η.naturality (𝟙 a) ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a)
_₁ :
  𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
      η.app a ◁ θ.naturality (𝟙 a) ⊗≫
        (η.naturality (𝟙 a) ≫ F.mapId a ▷ η.app a) ▷ θ.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)
⊢ η.vCompNaturality θ (𝟙 a) ≫ F.mapId a ▷ η.vCompApp θ a =
    η.vCompApp θ a ◁ H.mapId a ≫ (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv
have _₂ : 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) ⊗≫
    η.app a ◁ (θ.naturality (𝟙 a) ≫ G.mapId a ▷ θ.app a) ⊗≫ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) =
  η.vCompApp θ a ◁ H.mapId a ≫ (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv
Tactic: calc
    _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality (𝟙 a) ⊗≫
          (η.naturality (𝟙 a) ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.naturality (𝟙 a) ≫ G.mapId a ▷ θ.app a) ⊗≫ 𝟙 _ := by
      rw [η.naturality_id]
      bicategory
    _ = _ := by
      rw [θ.naturality_id]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} 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) ⊗≫
        (η.naturality (f ≫ g) ≫ F.mapComp f g ▷ η.app c) ▷ θ.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)
have rw : 𝟙 ((η.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: rw [η.naturality_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} 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) ≫ 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) =
    𝟙 ((η.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)
have rw : 𝟙 ((η.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: rw [θ.naturality_comp]