awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
simp :
  F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
        F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } ▷
          F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
        F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
      MonoidalCategoryStruct.whiskerRight
        (F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
        (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) =
    Iso.inv (MonoidalCategoryStruct.leftUnitor (F.map (𝟙 { as := { as := () } })))

Tactic:
simp only [tensorUnit_def, tensorObj_def, whiskerRight_def, Category.assoc, leftUnitor_def]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.whiskerRight_def, CategoryTheory.tensorObj_def, CategoryTheory.tensorUnit_def, CategoryTheory.leftUnitor_def
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
rw :
  F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.map₂ (λ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).hom ≫
        (λ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv
rw₁ :
  F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).hom ≫
        (λ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv
rw₂ rw₃ :
  (λ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
        F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } ▷
          F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) =
    (λ_ (F.map (𝟙 { as := { as := () } }))).inv

Tactic:
rw [F.mapComp_id_left, unitors_equal, F.map₂_inv_hom_assoc]

Premises used: CategoryTheory.Bicategory.unitors_equal, CategoryTheory.OplaxFunctor.toPrelaxFunctor, CategoryTheory.PrelaxFunctor.map₂_inv_hom_assoc, CategoryTheory.OplaxFunctor.mapComp_id_left
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
simp :
  (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
        F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
      F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
        F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
        F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
      MonoidalCategoryStruct.whiskerLeft
        (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))
        (F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) =
    Iso.inv (MonoidalCategoryStruct.rightUnitor (F.map (𝟙 { as := { as := () } })))

Tactic:
simp only [tensorUnit_def, tensorObj_def, whiskerLeft_def, rightUnitor_def]

Premises used: CategoryTheory.whiskerLeft_def, CategoryTheory.rightUnitor_def, CategoryTheory.tensorObj_def, CategoryTheory.tensorUnit_def
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
rw :
  F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
        F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
          F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
rw₁ :
  F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).hom ≫
        (ρ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
rw₂ rw₃ :
  (ρ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
        F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
      F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
        F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv

Tactic:
rw [Category.assoc, F.mapComp_id_right, F.map₂_inv_hom_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.OplaxFunctor.toPrelaxFunctor, CategoryTheory.OplaxFunctor.mapComp_id_right, CategoryTheory.PrelaxFunctor.map₂_inv_hom_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.map₂
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } ◁
            (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv) ≫
        F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
            (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } ≫
              𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
          F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
            F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
              (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) =
    F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.map₂
          ((ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ▷
            𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
        F.mapComp
            (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } ≫
              𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
            (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
          F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
                (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ▷
              F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
            (α_ (F.map (𝟙 { as := { as := () } })) (F.map (𝟙 { as := { as := () } }))
                (F.map (𝟙 { as := { as := () } }))).hom

Tactic:
simp only [whiskerLeft_rightUnitor_inv, PrelaxFunctor.map₂_comp, Category.assoc,
      OplaxFunctor.map₂_associator, whiskerRight_id, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.OplaxFunctor.map₂_associator, CategoryTheory.Bicategory.whiskerRight_id, CategoryTheory.Bicategory.whiskerLeft_rightUnitor_inv, CategoryTheory.PrelaxFunctor.map₂_comp, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 a : B
t : a ⟶ a
inst_1 : Comonad t
a_2 b c d : LocallyDiscrete (Discrete Unit)
x : a_2 ⟶ b
x_1 : b ⟶ c
x_2 : c ⟶ d
rw : Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_ t t t).hom
⊢ 𝟙 t ≫ Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_ t t t).hom

Tactic:
rw [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 a : B
t : a ⟶ a
inst_1 : Comonad t
a_2 b c d : LocallyDiscrete (Discrete Unit)
x : a_2 ⟶ b
x_1 : b ⟶ c
x_2 : c ⟶ d
⊢ Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_ t t t).hom

Tactic:
apply Comonad.comul_assoc

Premises used: CategoryTheory.Bicategory.Comonad.comul_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
t : a ⟶ a
inst_1 : Comonad t
⊢ (mkOfComonad t).hom = t

Tactic:
rfl

Premises used: CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.hom, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
t : a ⟶ a
inst_1 : Comonad t
⊢ Eq.{w + 1} (α := (mkOfComonad t).hom ⟶ 𝟙 (mkOfComonad t).obj) ε ε

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
t : a ⟶ a
inst_1 : Comonad t
change : 𝟙 t ≫ Δ = Δ
⊢ Eq.{w + 1} (α := (mkOfComonad t).hom ⟶ (mkOfComonad t).hom ≫ (mkOfComonad t).hom) Δ Δ

Tactic:
change 𝟙 t ≫ Δ = Δ

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
t : a ⟶ a
inst_1 : Comonad t
⊢ 𝟙 t ≫ Δ = Δ

Tactic:
apply Category.id_comp

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ η.vCompNaturality θ f ≫ F.map₂ β ▷ η.vCompApp θ b =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫ (η.naturality f ≫ F.map₂ β ▷ η.app b) ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
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)
⊢ 𝟙 ((η.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)

Tactic:
rw [naturality_naturality]

Premises used: CategoryTheory.Lax.LaxTrans.naturality_naturality
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : 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 ⊗≫ (η.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:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
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
⊢ 𝟙 ((η.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

Tactic:
rw [naturality_naturality]

Premises used: CategoryTheory.Lax.LaxTrans.naturality_naturality
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 ((η.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:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ η.vCompApp θ a ◁ H.mapId a ≫ η.vCompNaturality θ (𝟙 a) =
    𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapId a ≫ θ.naturality (𝟙 a)) ⊗≫
        η.naturality (𝟙 a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a : B
rw :
  𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      η.app a ◁ ((ρ_ (θ.app a)).hom ≫ (λ_ (θ.app a)).inv ≫ G.mapId a ▷ θ.app a) ⊗≫
        η.naturality (𝟙 a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a)
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapId a ≫ θ.naturality (𝟙 a)) ⊗≫
        η.naturality (𝟙 a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a)

Tactic:
rw [naturality_id]

Premises used: CategoryTheory.Lax.LaxTrans.naturality_id
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      η.app a ◁ ((ρ_ (θ.app a)).hom ≫ (λ_ (θ.app a)).inv ≫ G.mapId a ▷ θ.app a) ⊗≫
        η.naturality (𝟙 a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a : B
rw :
  𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      ((ρ_ (η.app a)).hom ≫ (λ_ (η.app a)).inv ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv ≫ F.mapId a ▷ η.vCompApp θ a
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv ≫ F.mapId a ▷ η.vCompApp θ a

Tactic:
rw [naturality_id]

Premises used: CategoryTheory.Lax.LaxTrans.naturality_id
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      ((ρ_ (η.app a)).hom ≫ (λ_ (η.app a)).inv ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv ≫ F.mapId a ▷ η.vCompApp θ a

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ η.vCompApp θ a ◁ H.mapComp f g ≫ η.vCompNaturality θ (f ≫ g) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapComp f g ≫ θ.naturality (f ≫ g)) ⊗≫
        η.naturality (f ≫ g) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
rw :
  𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁
          ((α_ (θ.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 ≫ G.mapComp f g ▷ θ.app c) ⊗≫
        η.naturality (f ≫ g) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapComp f g ≫ θ.naturality (f ≫ g)) ⊗≫
        η.naturality (f ≫ g) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)

Tactic:
rw [naturality_comp θ]

Premises used: CategoryTheory.Lax.LaxTrans.naturality_comp
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁
          ((α_ (θ.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 ≫ G.mapComp f g ▷ θ.app c) ⊗≫
        η.naturality (f ≫ g) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
rw :
  𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality 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 ≫ F.mapComp f g ▷ η.app c) ▷
            θ.app c ⊗≫
          𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ θ.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.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ θ.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.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)

Tactic:
rw [naturality_comp η]

Premises used: CategoryTheory.Lax.LaxTrans.naturality_comp
-- Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
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
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality 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 ≫ F.mapComp f g ▷ η.app c) ▷
            θ.app c ⊗≫
          𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ θ.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.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)

Tactic:
bicategory