awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ◁ (θ.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) =
    η.vCompApp θ a ◁ H.mapComp f g ≫
      (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫
          (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
            F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv
have rw : 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
    η.app a ◁ (θ.app a ◁ H.mapComp f g ⊗≫ θ.naturality f ▷ H.map g) ⊗≫
      (η.naturality f ▷ (θ.app b ≫ H.map g) ≫ (F.map f ≫ η.app b) ◁ θ.naturality g) ⊗≫
        F.map f ◁ η.naturality g ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) =
  η.vCompApp θ a ◁ H.mapComp f g ≫
    (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
      η.vCompNaturality θ f ▷ H.map g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
          F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv
Tactic: rw [whisker_exchange]
-- 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
⊢ η.vCompNaturality θ (f ≫ g) ≫ F.mapComp f g ▷ η.vCompApp θ c =
    η.vCompApp θ a ◁ H.mapComp f g ≫
      (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫
          (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
            F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv
have _ : η.vCompNaturality θ (f ≫ g) ≫ F.mapComp f g ▷ η.vCompApp θ 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)
Tactic: calc
    _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality (f ≫ g) ⊗≫
          (η.naturality (f ≫ g) ≫ F.mapComp f g ▷ η.app c) ▷ θ.app c ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.naturality (f ≫ g) ≫ G.mapComp f g ▷ θ.app c) ⊗≫
          (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 _ := by
      rw [η.naturality_comp]
      bicategory
    _ = 𝟙 _ ⊗≫ η.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 ⊗≫ 𝟙 _ := 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 c : B
f : a ⟶ b
g : b ⟶ c
_ :
  η.vCompNaturality θ (f ≫ g) ≫ F.mapComp f g ▷ η.vCompApp θ 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)
⊢ η.vCompNaturality θ (f ≫ g) ≫ F.mapComp f g ▷ η.vCompApp θ c =
    η.vCompApp θ a ◁ H.mapComp f g ≫
      (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫
          (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
            F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv
have _₁ : 𝟙 ((η.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)
Tactic: calc
    _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality (f ≫ g) ⊗≫
          (η.naturality (f ≫ g) ≫ F.mapComp f g ▷ η.app c) ▷ θ.app c ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.naturality (f ≫ g) ≫ G.mapComp f g ▷ θ.app c) ⊗≫
          (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 _ := by
      rw [η.naturality_comp]
      bicategory
    _ = 𝟙 _ ⊗≫ η.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 ⊗≫ 𝟙 _ := 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 c : B
f : a ⟶ b
g : b ⟶ c
_ :
  η.vCompNaturality θ (f ≫ g) ≫ F.mapComp f g ▷ η.vCompApp θ 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) ⊗≫
        (η.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)
⊢ η.vCompNaturality θ (f ≫ g) ≫ F.mapComp f g ▷ η.vCompApp θ c =
    η.vCompApp θ a ◁ H.mapComp f g ≫
      (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫
          (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
            F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv
have _₂ : 𝟙 ((η.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)
Tactic: calc
    _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality (f ≫ g) ⊗≫
          (η.naturality (f ≫ g) ≫ F.mapComp f g ▷ η.app c) ▷ θ.app c ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.naturality (f ≫ g) ≫ G.mapComp f g ▷ θ.app c) ⊗≫
          (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 _ := by
      rw [η.naturality_comp]
      bicategory
    _ = 𝟙 _ ⊗≫ η.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 ⊗≫ 𝟙 _ := 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 c : B
f : a ⟶ b
g : b ⟶ c
_ :
  η.vCompNaturality θ (f ≫ g) ≫ F.mapComp f g ▷ η.vCompApp θ 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) ⊗≫
        (η.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)
_₂ :
  𝟙 ((η.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)
⊢ η.vCompNaturality θ (f ≫ g) ≫ F.mapComp f g ▷ η.vCompApp θ c =
    η.vCompApp θ a ◁ H.mapComp f g ≫
      (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫
          (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
            F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv
have _₃ : 𝟙 ((η.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) =
  η.vCompApp θ a ◁ H.mapComp f g ≫
    (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
      η.vCompNaturality θ f ▷ H.map g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
          F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv
Tactic: calc
    _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality (f ≫ g) ⊗≫
          (η.naturality (f ≫ g) ≫ F.mapComp f g ▷ η.app c) ▷ θ.app c ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.naturality (f ≫ g) ≫ G.mapComp f g ▷ θ.app c) ⊗≫
          (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 _ := by
      rw [η.naturality_comp]
      bicategory
    _ = 𝟙 _ ⊗≫ η.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 ⊗≫ 𝟙 _ := 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
G H : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
θ : OplaxTrans G H
a b : B
a' : C
f : a' ⟶ G.obj a
g h : a ⟶ b
β : g ⟶ h
⊢ f ◁ G.map₂ β ▷ θ.app b ≫ f ◁ θ.naturality h = f ◁ θ.naturality g ≫ f ◁ θ.app a ◁ H.map₂ β
have simp_rw : f ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality h) = f ◁ (θ.naturality g ≫ θ.app a ◁ H.map₂ β)
Tactic: simp_rw [← whiskerLeft_comp, 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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
a b : B
a' : C
f g : a ⟶ b
β : f ⟶ g
h : G.obj b ⟶ a'
⊢ F.map₂ β ▷ η.app b ▷ h ≫ η.naturality g ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
have rw : (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ h =
  η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
Tactic: rw [← comp_whiskerRight, naturality_naturality, comp_whiskerRight, whisker_assoc]
-- 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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
a b : B
a' : C
f g : a ⟶ b
β : f ⟶ g
h : G.obj b ⟶ a'
rw :
  (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
⊢ F.map₂ β ▷ η.app b ▷ h ≫ η.naturality g ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
have rw₁ : (η.naturality f ≫ η.app a ◁ G.map₂ β) ▷ h =
  η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
Tactic: rw [← comp_whiskerRight, naturality_naturality, comp_whiskerRight, whisker_assoc]
-- 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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
a b : B
a' : C
f g : a ⟶ b
β : f ⟶ g
h : G.obj b ⟶ a'
rw :
  (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
rw₁ :
  (η.naturality f ≫ η.app a ◁ G.map₂ β) ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
⊢ F.map₂ β ▷ η.app b ▷ h ≫ η.naturality g ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
have rw₂ : η.naturality f ▷ h ≫ (η.app a ◁ G.map₂ β) ▷ h =
  η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
Tactic: rw [← comp_whiskerRight, naturality_naturality, comp_whiskerRight, whisker_assoc]
-- 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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
a b : B
a' : C
f g : a ⟶ b
β : f ⟶ g
h : G.obj b ⟶ a'
rw :
  (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
rw₁ :
  (η.naturality f ≫ η.app a ◁ G.map₂ β) ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
rw₂ :
  η.naturality f ▷ h ≫ (η.app a ◁ G.map₂ β) ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
⊢ F.map₂ β ▷ η.app b ▷ h ≫ η.naturality g ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
have rw₃ : η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv =
  η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv
Tactic: rw [← comp_whiskerRight, naturality_naturality, comp_whiskerRight, whisker_assoc]
-- 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
G H : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
θ : OplaxTrans G H
a b c : B
a' : C
f : a' ⟶ G.obj a
g : a ⟶ b
h : b ⟶ c
⊢ f ◁ θ.naturality (g ≫ h) ≫ f ◁ θ.app a ◁ H.mapComp g h =
    f ◁ G.mapComp g h ▷ θ.app c ≫
      f ◁ (α_ (G.map g) (G.map h) (θ.app c)).hom ≫
        f ◁ G.map g ◁ θ.naturality h ≫
          f ◁ (α_ (G.map g) (θ.app b) (H.map h)).inv ≫
            f ◁ θ.naturality g ▷ H.map h ≫ f ◁ (α_ (θ.app a) (H.map g) (H.map h)).hom
have simp_rw : f ◁ (θ.naturality (g ≫ h) ≫ θ.app a ◁ H.mapComp g h) =
  f ◁
    (G.mapComp g h ▷ θ.app c ≫
      (α_ (G.map g) (G.map h) (θ.app c)).hom ≫
        G.map g ◁ θ.naturality h ≫
          (α_ (G.map g) (θ.app b) (H.map h)).inv ≫ θ.naturality g ▷ H.map h ≫ (α_ (θ.app a) (H.map g) (H.map h)).hom)
Tactic: simp_rw [← whiskerLeft_comp, 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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
a b c : B
a' : C
f : a ⟶ b
g : b ⟶ c
h : G.obj c ⟶ a'
⊢ η.naturality (f ≫ g) ▷ h ≫ (α_ (η.app a) (G.map (f ≫ g)) h).hom ≫ η.app a ◁ G.mapComp f g ▷ h =
    F.mapComp f g ▷ η.app c ▷ h ≫
      (α_ (F.map f) (F.map g) (η.app c)).hom ▷ h ≫
        (α_ (F.map f) (F.map g ≫ η.app c) h).hom ≫
          F.map f ◁ η.naturality g ▷ h ≫
            (α_ (F.map f) (η.app b ≫ G.map g) h).inv ≫
              (α_ (F.map f) (η.app b) (G.map g)).inv ▷ h ≫
                η.naturality f ▷ G.map g ▷ h ≫
                  (α_ (η.app a) (G.map f) (G.map g)).hom ▷ h ≫ (α_ (η.app a) (G.map f ≫ G.map g) h).hom
have rw : (F.mapComp f g ▷ η.app 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) ▷
      h ≫
    (α_ (η.app a) (G.map f ≫ G.map g) h).hom =
  F.mapComp f g ▷ η.app c ▷ h ≫
    (α_ (F.map f) (F.map g) (η.app c)).hom ▷ h ≫
      (α_ (F.map f) (F.map g ≫ η.app c) h).hom ≫
        F.map f ◁ η.naturality g ▷ h ≫
          (α_ (F.map f) (η.app b ≫ G.map g) h).inv ≫
            (α_ (F.map f) (η.app b) (G.map g)).inv ▷ h ≫
              η.naturality f ▷ G.map g ▷ h ≫
                (α_ (η.app a) (G.map f) (G.map g)).hom ▷ h ≫ (α_ (η.app a) (G.map f ≫ G.map g) h).hom
Tactic: rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, 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
G H : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
θ : OplaxTrans G H
a : B
a' : C
f : a' ⟶ G.obj a
⊢ f ◁ θ.naturality (𝟙 a) ≫ f ◁ θ.app a ◁ H.mapId a =
    f ◁ G.mapId a ▷ θ.app a ≫ f ◁ (λ_ (θ.app a)).hom ≫ f ◁ (ρ_ (θ.app a)).inv
have simp_rw : f ◁ (θ.naturality (𝟙 a) ≫ θ.app a ◁ H.mapId a) = f ◁ (G.mapId a ▷ θ.app a ≫ (λ_ (θ.app a)).hom ≫ (ρ_ (θ.app a)).inv)
Tactic: simp_rw [← whiskerLeft_comp, 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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
a : B
a' : C
f : G.obj a ⟶ a'
⊢ η.naturality (𝟙 a) ▷ f ≫ (α_ (η.app a) (G.map (𝟙 a)) f).hom ≫ η.app a ◁ G.mapId a ▷ f =
    F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom
have rw : (F.mapId a ▷ η.app a ≫ (λ_ (η.app a)).hom ≫ (ρ_ (η.app a)).inv) ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom =
  F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom
Tactic: rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, 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
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ ((α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
        η.naturality (f ≫ g) ▷ θ.app c ≫
          (α_ (η.app a) (G.map (f ≫ g)) (θ.app c)).hom ≫
            η.app a ◁ θ.naturality (f ≫ g) ≫ (α_ (η.app a) (θ.app a) (H.map (f ≫ g))).inv) ≫
      (η.app a ≫ θ.app a) ◁ H.mapComp f g =
    (α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      F.mapComp f g ▷ η.app c ▷ θ.app c ≫
        (α_ (F.map f) (F.map g) (η.app c)).hom ▷ θ.app c ≫
          (α_ (F.map f) (F.map g ≫ η.app c) (θ.app c)).hom ≫
            F.map f ◁ η.naturality g ▷ θ.app c ≫
              F.map f ◁ (α_ (η.app b) (G.map g) (θ.app c)).hom ≫
                (α_ (F.map f) (η.app b) (G.map g ≫ θ.app c)).inv ≫
                  (F.map f ≫ η.app b) ◁ θ.naturality g ≫
                    η.naturality f ▷ (θ.app b ≫ H.map g) ≫
                      (α_ (η.app a) (G.map f) (θ.app b ≫ H.map g)).hom ≫
                        η.app a ◁ (α_ (G.map f) (θ.app b) (H.map g)).inv ≫
                          η.app a ◁ θ.naturality f ▷ H.map g ≫
                            η.app a ◁ (α_ (θ.app a) (H.map f) (H.map g)).hom ≫
                              (α_ (η.app a) (θ.app a) (H.map f ≫ H.map g)).inv
have rw : ((α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      η.naturality (f ≫ g) ▷ θ.app c ≫
        (α_ (η.app a) (G.map (f ≫ g)) (θ.app c)).hom ≫
          η.app a ◁ θ.naturality (f ≫ g) ≫ (α_ (η.app a) (θ.app a) (H.map (f ≫ g))).inv) ≫
    (η.app a ≫ θ.app a) ◁ H.mapComp f g =
  (α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
    F.mapComp f g ▷ η.app c ▷ θ.app c ≫
      (α_ (F.map f) (F.map g) (η.app c)).hom ▷ θ.app c ≫
        (α_ (F.map f) (F.map g ≫ η.app c) (θ.app c)).hom ≫
          F.map f ◁ η.naturality g ▷ θ.app c ≫
            F.map f ◁ (α_ (η.app b) (G.map g) (θ.app c)).hom ≫
              (α_ (F.map f) (η.app b) (G.map g ≫ θ.app c)).inv ≫
                η.naturality f ▷ (G.map g ≫ θ.app c) ≫
                  (η.app a ≫ G.map f) ◁ θ.naturality g ≫
                    (α_ (η.app a) (G.map f) (θ.app b ≫ H.map g)).hom ≫
                      η.app a ◁ (α_ (G.map f) (θ.app b) (H.map g)).inv ≫
                        η.app a ◁ θ.naturality f ▷ H.map g ≫
                          η.app a ◁ (α_ (θ.app a) (H.map f) (H.map g)).hom ≫
                            (α_ (η.app a) (θ.app a) (H.map f ≫ H.map g)).inv
Tactic: rw [whisker_exchange_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
α : F ⟶ G
a : B
⊢ α.naturality (𝟙 a) = F.mapId a ▷ᵢ α.app a ≪≫ λ_ (α.app a) ≪≫ (ρ_ (α.app a)).symm ≪≫ α.app a ◁ᵢ (G.mapId a).symm
have w : (α.naturality (𝟙 a)).hom =
  (F.mapId a ▷ᵢ α.app a ≪≫ λ_ (α.app a) ≪≫ (ρ_ (α.app a)).symm ≪≫ α.app a ◁ᵢ (G.mapId a).symm).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ α.naturality g = F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η
have w : (α.naturality g).hom = (F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
α : F ⟶ G
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ (α.naturality g).hom = (F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η).hom
have w : F.map₂ η.inv ▷ α.app b ≫ (α.naturality f).hom ≫ α.app a ◁ G.map₂ η.hom =
  (F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η).hom
Tactic: rw [naturality_naturality_hom α η]