awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
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
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
⊢ ((α_ (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

Tactic:
rw [whisker_exchange_assoc]

Premises used: CategoryTheory.Bicategory.whisker_exchange_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
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 ≫
                  η.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:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
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 ≫
      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 =
    F.mapComp f g ▷ (η.app c ≫ θ.app c) ≫
      (α_ (F.map f) (F.map g) (η.app c ≫ θ.app c)).hom ≫
        F.map f ◁
            ((α_ (F.map g) (η.app c) (θ.app c)).inv ≫
              η.naturality g ▷ θ.app c ≫
                (α_ (η.app b) (G.map g) (θ.app c)).hom ≫
                  η.app b ◁ θ.naturality g ≫ (α_ (η.app b) (θ.app b) (H.map g)).inv) ≫
          (α_ (F.map f) (η.app b ≫ θ.app b) (H.map g)).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) ▷
                H.map g ≫
              (α_ (η.app a ≫ θ.app a) (H.map f) (H.map g)).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
⊢ (id F).toOplax = OplaxTrans.id F

Tactic:
rfl

Premises used: CategoryTheory.Oplax.OplaxTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
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
θ : StrongTrans 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).hom = f ◁ (θ.naturality g).hom ≫ f ◁ θ.app a ◁ H.map₂ β

Tactic:
apply θ.toOplax.whiskerLeft_naturality_naturality

Premises used: CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_naturality, CategoryTheory.Oplax.StrongTrans.toOplax
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
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
η : StrongTrans 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).hom ▷ h =
    (η.naturality f).hom ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv

Tactic:
η.toOplax.whiskerRight_naturality_naturality _ _

Premises used: CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality, CategoryTheory.Oplax.StrongTrans.toOplax
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
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
θ : StrongTrans G H
a b c : B
a' : C
f : a' ⟶ G.obj a
g : a ⟶ b
h : b ⟶ c
⊢ f ◁ (θ.naturality (g ≫ h)).hom ≫ 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).hom ≫
          f ◁ (α_ (G.map g) (θ.app b) (H.map h)).inv ≫
            f ◁ (θ.naturality g).hom ▷ H.map h ≫ f ◁ (α_ (θ.app a) (H.map g) (H.map h)).hom

Tactic:
θ.toOplax.whiskerLeft_naturality_comp _ _ _

Premises used: CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp, CategoryTheory.Oplax.StrongTrans.toOplax
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
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
η : StrongTrans F G
a b c : B
a' : C
f : a ⟶ b
g : b ⟶ c
h : G.obj c ⟶ a'
⊢ (η.naturality (f ≫ g)).hom ▷ 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).hom ▷ h ≫
            (α_ (F.map f) (η.app b ≫ G.map g) h).inv ≫
              (α_ (F.map f) (η.app b) (G.map g)).inv ▷ h ≫
                (η.naturality f).hom ▷ 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:
η.toOplax.whiskerRight_naturality_comp _ _ _

Premises used: CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_comp, CategoryTheory.Oplax.StrongTrans.toOplax
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
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
θ : StrongTrans G H
a : B
a' : C
f : a' ⟶ G.obj a
⊢ f ◁ (θ.naturality (𝟙 a)).hom ≫ f ◁ θ.app a ◁ H.mapId a =
    f ◁ G.mapId a ▷ θ.app a ≫ f ◁ (λ_ (θ.app a)).hom ≫ f ◁ (ρ_ (θ.app a)).inv

Tactic:
θ.toOplax.whiskerLeft_naturality_id _

Premises used: CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_id, CategoryTheory.Oplax.StrongTrans.toOplax
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
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
η : StrongTrans F G
a : B
a' : C
f : G.obj a ⟶ a'
⊢ (η.naturality (𝟙 a)).hom ▷ 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

Tactic:
η.toOplax.whiskerRight_naturality_id _

Premises used: CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_id, CategoryTheory.Oplax.StrongTrans.toOplax
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : F ⟶ G
θ : G ⟶ H
a : B
⊢ (η ≫ θ).app a = η.app a ≫ θ.app a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
⊢ Oplax.StrongTrans.id F.toOplax = StrongTrans.toOplax (𝟙 F)

Tactic:
rfl

Premises used: CategoryTheory.Pseudofunctor.StrongTrans.toOplax, CategoryTheory.Oplax.StrongTrans.mkOfOplax, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
G H : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
θ : 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).hom = f ◁ (θ.naturality g).hom ≫ f ◁ θ.app a ◁ H.map₂ β

Tactic:
θ.toOplax.whiskerLeft_naturality_naturality _ _

Premises used: CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_naturality, CategoryTheory.Pseudofunctor.StrongTrans.toOplax
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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
a' : C
f g : a ⟶ b
β : f ⟶ g
h : G.obj b ⟶ a'
⊢ F.map₂ β ▷ η.app b ▷ h ≫ (η.naturality g).hom ▷ h =
    (η.naturality f).hom ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv

Tactic:
η.toOplax.whiskerRight_naturality_naturality _ _

Premises used: CategoryTheory.Pseudofunctor.StrongTrans.toOplax, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_naturality
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
G H : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
θ : G ⟶ H
a b c : B
a' : C
f : a' ⟶ G.obj a
g : a ⟶ b
h : b ⟶ c
⊢ f ◁ (θ.naturality (g ≫ h)).hom ≫ f ◁ θ.app a ◁ (H.mapComp g h).hom =
    f ◁ (G.mapComp g h).hom ▷ θ.app c ≫
      f ◁ (α_ (G.map g) (G.map h) (θ.app c)).hom ≫
        f ◁ G.map g ◁ (θ.naturality h).hom ≫
          f ◁ (α_ (G.map g) (θ.app b) (H.map h)).inv ≫
            f ◁ (θ.naturality g).hom ▷ H.map h ≫ f ◁ (α_ (θ.app a) (H.map g) (H.map h)).hom

Tactic:
θ.toOplax.whiskerLeft_naturality_comp _ _ _

Premises used: CategoryTheory.Pseudofunctor.StrongTrans.toOplax, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_comp
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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 c : B
a' : C
f : a ⟶ b
g : b ⟶ c
h : G.obj c ⟶ a'
⊢ (η.naturality (f ≫ g)).hom ▷ h ≫ (α_ (η.app a) (G.map (f ≫ g)) h).hom ≫ η.app a ◁ (G.mapComp f g).hom ▷ h =
    (F.mapComp f g).hom ▷ η.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).hom ▷ h ≫
            (α_ (F.map f) (η.app b ≫ G.map g) h).inv ≫
              (α_ (F.map f) (η.app b) (G.map g)).inv ▷ h ≫
                (η.naturality f).hom ▷ 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:
η.toOplax.whiskerRight_naturality_comp _ _ _

Premises used: CategoryTheory.Pseudofunctor.StrongTrans.toOplax, CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
G H : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
θ : G ⟶ H
a : B
a' : C
f : a' ⟶ G.obj a
⊢ f ◁ (θ.naturality (𝟙 a)).hom ≫ f ◁ θ.app a ◁ (H.mapId a).hom =
    f ◁ (G.mapId a).hom ▷ θ.app a ≫ f ◁ (λ_ (θ.app a)).hom ≫ f ◁ (ρ_ (θ.app a)).inv

Tactic:
θ.toOplax.whiskerLeft_naturality_id _

Premises used: CategoryTheory.Pseudofunctor.StrongTrans.toOplax, CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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
a' : C
f : G.obj a ⟶ a'
⊢ (η.naturality (𝟙 a)).hom ▷ f ≫ (α_ (η.app a) (G.map (𝟙 a)) f).hom ≫ η.app a ◁ (G.mapId a).hom ▷ f =
    (F.mapId a).hom ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom

Tactic:
η.toOplax.whiskerRight_naturality_id _

Premises used: CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_id, CategoryTheory.Pseudofunctor.StrongTrans.toOplax
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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)).hom =
    (F.mapId a).hom ▷ α.app a ≫ (λ_ (α.app a)).hom ≫ (ρ_ (α.app a)).inv ≫ α.app a ◁ (G.mapId a).inv

Tactic:
simp [← assoc, ← IsIso.comp_inv_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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
w :
  (α.naturality (𝟙 a)).hom =
    (F.mapId a ▷ᵢ α.app a ≪≫ λ_ (α.app a) ≪≫ (ρ_ (α.app a)).symm ≪≫ α.app a ◁ᵢ (G.mapId a).symm).hom
⊢ α.naturality (𝟙 a) = F.mapId a ▷ᵢ α.app a ≪≫ λ_ (α.app a) ≪≫ (ρ_ (α.app a)).symm ≪≫ α.app a ◁ᵢ (G.mapId a).symm

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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)).hom =
    (F.mapId a ▷ᵢ α.app a ≪≫ λ_ (α.app a) ≪≫ (ρ_ (α.app a)).symm ≪≫ α.app a ◁ᵢ (G.mapId a).symm).hom

Tactic:
simp [naturality_id_hom]

Premises used: CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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)).inv =
    α.app a ◁ (G.mapId a).hom ≫ (ρ_ (α.app a)).hom ≫ (λ_ (α.app a)).inv ≫ (F.mapId a).inv ▷ α.app a

Tactic:
simp [naturality_id_iso]

Premises used: CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_iso
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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₂ η.inv ▷ α.app b ≫ (α.naturality f).hom ≫ α.app a ◁ G.map₂ η.hom

Tactic:
simp [← IsIso.inv_comp_eq, ← G.map₂_inv η.inv]

Premises used: CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.Pseudofunctor.toPrelaxFunctor, CategoryTheory.PrelaxFunctor.map₂_inv, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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
w : (α.naturality g).hom = (F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η).hom
⊢ α.naturality g = F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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
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
⊢ (α.naturality g).hom = (F.map₂Iso η.symm ▷ᵢ α.app b ≪≫ α.naturality f ≪≫ α.app a ◁ᵢ G.map₂Iso η).hom

Tactic:
rw [naturality_naturality_hom α η]

Premises used: CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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).inv = α.app a ◁ G.map₂ η.inv ≫ (α.naturality f).inv ≫ F.map₂ η.hom ▷ α.app b

Tactic:
simp [naturality_naturality_iso α η]

Premises used: CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_iso
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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 c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α.naturality (f ≫ g)).hom =
    (F.mapComp f g).hom ▷ α.app c ≫
      (α_ (F.map f) (F.map g) (α.app c)).hom ≫
        F.map f ◁ (α.naturality g).hom ≫
          (α_ (F.map f) (α.app b) (G.map g)).inv ≫
            (α.naturality f).hom ▷ G.map g ≫ (α_ (α.app a) (G.map f) (G.map g)).hom ≫ α.app a ◁ (G.mapComp f g).inv

Tactic:
simp [← assoc, ← IsIso.comp_inv_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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 c : B
f : a ⟶ b
g : b ⟶ c
w :
  (α.naturality (f ≫ g)).hom =
    (F.mapComp f g ▷ᵢ α.app c ≪≫
        α_ (F.map f) (F.map g) (α.app c) ≪≫
          F.map f ◁ᵢ α.naturality g ≪≫
            (α_ (F.map f) (α.app b) (G.map g)).symm ≪≫
              α.naturality f ▷ᵢ G.map g ≪≫ α_ (α.app a) (G.map f) (G.map g) ≪≫ α.app a ◁ᵢ (G.mapComp f g).symm).hom
⊢ α.naturality (f ≫ g) =
    F.mapComp f g ▷ᵢ α.app c ≪≫
      α_ (F.map f) (F.map g) (α.app c) ≪≫
        F.map f ◁ᵢ α.naturality g ≪≫
          (α_ (F.map f) (α.app b) (G.map g)).symm ≪≫
            α.naturality f ▷ᵢ G.map g ≪≫ α_ (α.app a) (G.map f) (G.map g) ≪≫ α.app a ◁ᵢ (G.mapComp f g).symm

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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 c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α.naturality (f ≫ g)).hom =
    (F.mapComp f g ▷ᵢ α.app c ≪≫
        α_ (F.map f) (F.map g) (α.app c) ≪≫
          F.map f ◁ᵢ α.naturality g ≪≫
            (α_ (F.map f) (α.app b) (G.map g)).symm ≪≫
              α.naturality f ▷ᵢ G.map g ≪≫ α_ (α.app a) (G.map f) (G.map g) ≪≫ α.app a ◁ᵢ (G.mapComp f g).symm).hom

Tactic:
simp [naturality_comp_hom α f g]

Premises used: CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
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 c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α.naturality (f ≫ g)).inv =
    α.app a ◁ (G.mapComp f g).hom ≫
      (α_ (α.app a) (G.map f) (G.map g)).inv ≫
        (α.naturality f).inv ▷ G.map g ≫
          (α_ (F.map f) (α.app b) (G.map g)).hom ≫
            F.map f ◁ (α.naturality g).inv ≫ (α_ (F.map f) (F.map g) (α.app c)).inv ≫ (F.mapComp f g).inv ▷ α.app c

Tactic:
simp [naturality_comp_iso α f g]

Premises used: CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_iso
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ (op2 η).unop2 = η

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : Bᵒᵖ
f g : a ⟶ b
η : f ⟶ g
⊢ op2 η.unop2 = η

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, Bicategory.Opposite.op2, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ op2 (η ≫ θ) = op2 η ≫ op2 θ

Tactic:
rfl

Premises used: Quiver.Hom.unop, Bicategory.Opposite.op2, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
⊢ op2 (𝟙 f) = 𝟙 f.op

Tactic:
rfl

Premises used: Quiver.Hom.unop, Bicategory.Opposite.op2, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Opposites
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : Bᵒᵖ
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ (η ≫ θ).unop2 = η.unop2 ≫ θ.unop2

Tactic:
rfl

Premises used: rfl