awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v, v_1, u, u_1} C D
η : F ⟶ G
X Y : WithTerminal C
f_1 : X ⟶ Y
x y : C
f : of x ⟶ of y
⊢ Eq (α := (map F).obj (of x) ⟶ (map G).obj (of y))
    ((map F).map f ≫
      match (motive := (X : WithTerminal C) → (map F).obj X ⟶ (map G).obj X) of y with
      | of x => η.app x
      | star => 𝟙 star)
    ((match (motive := (X : WithTerminal C) → (map F).obj X ⟶ (map G).obj X) of x with
      | of x => η.app x
      | star => 𝟙 star) ≫
      (map G).map f)

Tactic:
exact η.naturality f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v, v_1, u, u_1} C D
η : F ⟶ G
X Y : WithTerminal C
f : X ⟶ Y
x : C
x_1 : of x ⟶ star
⊢ Eq (α := (map F).obj (of x) ⟶ (map G).obj star)
    ((map F).map x_1 ≫
      match (motive := (X : WithTerminal C) → (map F).obj X ⟶ (map G).obj X) star with
      | of x => η.app x
      | star => 𝟙 star)
    ((match (motive := (X : WithTerminal C) → (map F).obj X ⟶ (map G).obj X) of x with
      | of x => η.app x
      | star => 𝟙 star) ≫
      (map G).map x_1)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v, v_1, u, u_1} C D
η : F ⟶ G
X Y : WithTerminal C
f : X ⟶ Y
x : Quiver.Hom.{v, u} (V := WithTerminal C) star star
⊢ ((map F).map x ≫
      match (motive := (X : WithTerminal C) → (map F).obj X ⟶ (map G).obj X) star with
      | of x => η.app x
      | star => 𝟙 star) =
    (match (motive := (X : WithTerminal C) → (map F).obj X ⟶ (map G).obj X) star with
      | of x => η.app x
      | star => 𝟙 star) ≫
      (map G).map x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v, v_1, u, u_1} C D
η : F ⟶ G
X Y : WithTerminal C
f : X ⟶ Y
⊢ Eq (α := (map F).obj X ⟶ (map G).obj Y)
    ((map F).map f ≫
      match (motive := (X : WithTerminal C) → (map F).obj X ⟶ (map G).obj X) Y with
      | of x => η.app x
      | star => 𝟙 star)
    ((match (motive := (X : WithTerminal C) → (map F).obj X ⟶ (map G).obj X) X with
      | of x => η.app x
      | star => 𝟙 star) ≫
      (map G).map f)

Tactic:
match X, Y, f with
    | of x, of y, f => exact η.naturality f
    | of x, star, _ => rfl
    | star, star, _ => rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
h :
  ∀ (X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)),
    (NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f)))).toNatTrans.app X =
      (Cat.Hom₂.toNatTrans (𝟙 (map f.toFunctor).toCatHom)).app X
⊢ NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f))) = 𝟙 (map f.toFunctor).toCatHom

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj (of a_1) ⟶ (map f.toFunctor).toCatHom.toFunctor.obj (of a_1))
      ((NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f)))).toNatTrans.app (of a_1))
      ((Cat.Hom₂.toNatTrans (𝟙 (map f.toFunctor).toCatHom)).app (of a_1))
h₁ :
  Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj star ⟶ (map f.toFunctor).toCatHom.toFunctor.obj star)
    ((NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f)))).toNatTrans.app star)
    ((Cat.Hom₂.toNatTrans (𝟙 (map f.toFunctor).toCatHom)).app star)
⊢ (NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f)))).toNatTrans.app X =
    (Cat.Hom₂.toNatTrans (𝟙 (map f.toFunctor).toCatHom)).app X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
a_1 : (↑a : Type u_1)
⊢ Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj (of a_1) ⟶ (map f.toFunctor).toCatHom.toFunctor.obj (of a_1))
    ((NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f)))).toNatTrans.app (of a_1))
    ((Cat.Hom₂.toNatTrans (𝟙 (map f.toFunctor).toCatHom)).app (of a_1))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
⊢ Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj star ⟶ (map f.toFunctor).toCatHom.toFunctor.obj star)
    ((NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f)))).toNatTrans.app star)
    ((Cat.Hom₂.toNatTrans (𝟙 (map f.toFunctor).toCatHom)).app star)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f g h_1 : a ⟶ b
η : f ⟶ g
θ : g ⟶ h_1
h :
  ∀ (X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)),
    (NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans)).toNatTrans.app X =
      (NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)).toNatTrans.app X
⊢ NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans) =
    NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f g h_1 : a ⟶ b
η : f ⟶ g
θ : g ⟶ h_1
X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj (of a_1) ⟶ (map h_1.toFunctor).toCatHom.toFunctor.obj (of a_1))
      ((NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans)).toNatTrans.app (of a_1))
      ((NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)).toNatTrans.app (of a_1))
h₁ :
  Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj star ⟶ (map h_1.toFunctor).toCatHom.toFunctor.obj star)
    ((NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans)).toNatTrans.app star)
    ((NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)).toNatTrans.app star)
⊢ (NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans)).toNatTrans.app X =
    (NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)).toNatTrans.app X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
a_1 : (↑a : Type u_1)
⊢ Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj (of a_1) ⟶ (map h.toFunctor).toCatHom.toFunctor.obj (of a_1))
    ((NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans)).toNatTrans.app (of a_1))
    ((NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)).toNatTrans.app (of a_1))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj star ⟶ (map h.toFunctor).toCatHom.toFunctor.obj star)
    ((NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans)).toNatTrans.app star)
    ((NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)).toNatTrans.app star)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f : a ⟶ b
g h_1 : b ⟶ c
η : g ⟶ h_1
h :
  ∀ (X : (↑(prelaxfunctor.obj a) : Type u_1)),
    (prelaxfunctor.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app X =
      ((Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
              Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
                (Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).inv).toNatTrans.app
        X
⊢ prelaxfunctor.map₂ (Bicategory.whiskerLeft f η) =
    (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
      Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
        (Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).inv

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f : a ⟶ b
g h_1 : b ⟶ c
η : g ⟶ h_1
X : (↑(prelaxfunctor.obj a) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α := (prelaxfunctor.map (f ≫ g)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map (f ≫ h_1)).toFunctor.obj (of a_1))
      ((prelaxfunctor.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app (of a_1))
      (((Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
              Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
                (Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).inv).toNatTrans.app
        (of a_1))
h₁ :
  Eq (α := (prelaxfunctor.map (f ≫ g)).toFunctor.obj star ⟶ (prelaxfunctor.map (f ≫ h_1)).toFunctor.obj star)
    ((prelaxfunctor.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app star)
    (((Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
              (Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).inv).toNatTrans.app
      star)
⊢ (prelaxfunctor.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
              (Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).inv).toNatTrans.app
      X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
a_1 : (↑a : Type u_1)
⊢ Eq (α := (prelaxfunctor.map (f ≫ g)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map (f ≫ h)).toFunctor.obj (of a_1))
    ((prelaxfunctor.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app (of a_1))
    (((Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
              (Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).inv).toNatTrans.app
      (of a_1))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ Eq (α := (prelaxfunctor.map (f ≫ g)).toFunctor.obj star ⟶ (prelaxfunctor.map (f ≫ h)).toFunctor.obj star)
    ((prelaxfunctor.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app star)
    (((Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
              (Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).inv).toNatTrans.app
      star)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f g : a ⟶ b
η : f ⟶ g
h_1 : b ⟶ c
h :
  ∀ (X : (↑(prelaxfunctor.obj a) : Type u_1)),
    (prelaxfunctor.map₂ (Bicategory.whiskerRight η h_1)).toNatTrans.app X =
      ((Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).hom ≫
              Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h_1) ≫
                (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv).toNatTrans.app
        X
⊢ prelaxfunctor.map₂ (Bicategory.whiskerRight η h_1) =
    (Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).hom ≫
      Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h_1) ≫
        (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f g : a ⟶ b
η : f ⟶ g
h_1 : b ⟶ c
X : (↑(prelaxfunctor.obj a) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α :=
      (prelaxfunctor.map (f ≫ h_1)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map (g ≫ h_1)).toFunctor.obj (of a_1))
      ((prelaxfunctor.map₂ (Bicategory.whiskerRight η h_1)).toNatTrans.app (of a_1))
      (((Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).hom ≫
              Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h_1) ≫
                (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv).toNatTrans.app
        (of a_1))
h₁ :
  Eq (α := (prelaxfunctor.map (f ≫ h_1)).toFunctor.obj star ⟶ (prelaxfunctor.map (g ≫ h_1)).toFunctor.obj star)
    ((prelaxfunctor.map₂ (Bicategory.whiskerRight η h_1)).toNatTrans.app star)
    (((Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).hom ≫
            Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h_1) ≫
              (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv).toNatTrans.app
      star)
⊢ (prelaxfunctor.map₂ (Bicategory.whiskerRight η h_1)).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).hom ≫
            Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h_1) ≫
              (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv).toNatTrans.app
      X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f g : a ⟶ b
η : f ⟶ g
h_1 : b ⟶ c
a_1 : (↑a : Type u_1)
h : h_1.toFunctor.map (η.toNatTrans.app a_1) = h_1.toFunctor.map (down (η.toNatTrans.app a_1))
⊢ Eq (α := (prelaxfunctor.map (f ≫ h_1)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map (g ≫ h_1)).toFunctor.obj (of a_1))
    ((prelaxfunctor.map₂ (Bicategory.whiskerRight η h_1)).toNatTrans.app (of a_1))
    (((Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).hom ≫
            Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h_1) ≫
              (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv).toNatTrans.app
      (of a_1))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
a_1 : (↑a : Type u_1)
⊢ h.toFunctor.map (η.toNatTrans.app a_1) = h.toFunctor.map (down (η.toNatTrans.app a_1))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
⊢ Eq (α := (prelaxfunctor.map (f ≫ h)).toFunctor.obj star ⟶ (prelaxfunctor.map (g ≫ h)).toFunctor.obj star)
    ((prelaxfunctor.map₂ (Bicategory.whiskerRight η h)).toNatTrans.app star)
    (((Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).hom ≫
            Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h) ≫
              (Cat.Hom.isoMk (mapComp g.toFunctor h.toFunctor)).inv).toNatTrans.app
      star)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c d : Cat
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
dsimp :
  NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h.toFunctor).hom) =
    NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h.toFunctor).hom ≫
      Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom) (map h.toFunctor).toCatHom ≫
        (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom (map h.toFunctor).toCatHom).hom ≫
          Bicategory.whiskerLeft (map f.toFunctor).toCatHom (NatTrans.toCatHom₂ (mapComp g.toFunctor h.toFunctor).inv) ≫
            NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h.toFunctor)).inv
⊢ prelaxfunctor.map₂ (Bicategory.associator f g h).hom =
    (Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h.toFunctor)).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h) ≫
        (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h)).hom ≫
          Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h.toFunctor)).inv ≫
            (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ h).toFunctor)).inv

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c d : Cat
f : a ⟶ b
g : b ⟶ c
h_1 : c ⟶ d
h :
  ∀ (X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)),
    (NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h_1.toFunctor).hom)).toNatTrans.app X =
      (NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h_1.toFunctor).hom ≫
              Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom)
                  (map h_1.toFunctor).toCatHom ≫
                (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom
                      (map h_1.toFunctor).toCatHom).hom ≫
                  Bicategory.whiskerLeft (map f.toFunctor).toCatHom
                      (NatTrans.toCatHom₂ (mapComp g.toFunctor h_1.toFunctor).inv) ≫
                    NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h_1.toFunctor)).inv).toNatTrans.app
        X
⊢ NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h_1.toFunctor).hom) =
    NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h_1.toFunctor).hom ≫
      Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom) (map h_1.toFunctor).toCatHom ≫
        (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom (map h_1.toFunctor).toCatHom).hom ≫
          Bicategory.whiskerLeft (map f.toFunctor).toCatHom
              (NatTrans.toCatHom₂ (mapComp g.toFunctor h_1.toFunctor).inv) ≫
            NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h_1.toFunctor)).inv

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c d : Cat
f : a ⟶ b
g : b ⟶ c
h_1 : c ⟶ d
X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α :=
      (map ((f.toFunctor ⋙ g.toFunctor) ⋙ h_1.toFunctor)).toCatHom.toFunctor.obj (of a_1) ⟶
        (map (f.toFunctor ⋙ g.toFunctor ⋙ h_1.toFunctor)).toCatHom.toFunctor.obj (of a_1))
      ((NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h_1.toFunctor).hom)).toNatTrans.app (of a_1))
      ((NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h_1.toFunctor).hom ≫
              Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom)
                  (map h_1.toFunctor).toCatHom ≫
                (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom
                      (map h_1.toFunctor).toCatHom).hom ≫
                  Bicategory.whiskerLeft (map f.toFunctor).toCatHom
                      (NatTrans.toCatHom₂ (mapComp g.toFunctor h_1.toFunctor).inv) ≫
                    NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h_1.toFunctor)).inv).toNatTrans.app
        (of a_1))
h₁ :
  Eq (α :=
    (map ((f.toFunctor ⋙ g.toFunctor) ⋙ h_1.toFunctor)).toCatHom.toFunctor.obj star ⟶
      (map (f.toFunctor ⋙ g.toFunctor ⋙ h_1.toFunctor)).toCatHom.toFunctor.obj star)
    ((NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h_1.toFunctor).hom)).toNatTrans.app star)
    ((NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h_1.toFunctor).hom ≫
            Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom)
                (map h_1.toFunctor).toCatHom ≫
              (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom
                    (map h_1.toFunctor).toCatHom).hom ≫
                Bicategory.whiskerLeft (map f.toFunctor).toCatHom
                    (NatTrans.toCatHom₂ (mapComp g.toFunctor h_1.toFunctor).inv) ≫
                  NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h_1.toFunctor)).inv).toNatTrans.app
      star)
⊢ (NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h_1.toFunctor).hom)).toNatTrans.app X =
    (NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h_1.toFunctor).hom ≫
            Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom)
                (map h_1.toFunctor).toCatHom ≫
              (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom
                    (map h_1.toFunctor).toCatHom).hom ≫
                Bicategory.whiskerLeft (map f.toFunctor).toCatHom
                    (NatTrans.toCatHom₂ (mapComp g.toFunctor h_1.toFunctor).inv) ≫
                  NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h_1.toFunctor)).inv).toNatTrans.app
      X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c d : Cat
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
a_1 : (↑a : Type u_1)
⊢ Eq (α :=
    (map ((f.toFunctor ⋙ g.toFunctor) ⋙ h.toFunctor)).toCatHom.toFunctor.obj (of a_1) ⟶
      (map (f.toFunctor ⋙ g.toFunctor ⋙ h.toFunctor)).toCatHom.toFunctor.obj (of a_1))
    ((NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h.toFunctor).hom)).toNatTrans.app (of a_1))
    ((NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h.toFunctor).hom ≫
            Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom)
                (map h.toFunctor).toCatHom ≫
              (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom
                    (map h.toFunctor).toCatHom).hom ≫
                Bicategory.whiskerLeft (map f.toFunctor).toCatHom
                    (NatTrans.toCatHom₂ (mapComp g.toFunctor h.toFunctor).inv) ≫
                  NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h.toFunctor)).inv).toNatTrans.app
      (of a_1))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b c d : Cat
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ Eq (α :=
    (map ((f.toFunctor ⋙ g.toFunctor) ⋙ h.toFunctor)).toCatHom.toFunctor.obj star ⟶
      (map (f.toFunctor ⋙ g.toFunctor ⋙ h.toFunctor)).toCatHom.toFunctor.obj star)
    ((NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h.toFunctor).hom)).toNatTrans.app star)
    ((NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h.toFunctor).hom ≫
            Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom)
                (map h.toFunctor).toCatHom ≫
              (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom
                    (map h.toFunctor).toCatHom).hom ≫
                Bicategory.whiskerLeft (map f.toFunctor).toCatHom
                    (NatTrans.toCatHom₂ (mapComp g.toFunctor h.toFunctor).inv) ≫
                  NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h.toFunctor)).inv).toNatTrans.app
      star)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
h :
  ∀ (X : (↑(prelaxfunctor.obj a) : Type u_1)),
    (prelaxfunctor.map₂ (Bicategory.leftUnitor f).hom).toNatTrans.app X =
      ((Cat.Hom.isoMk (mapComp (Cat.Hom.toFunctor (𝟙 a)) f.toFunctor)).hom ≫
              Bicategory.whiskerRight (Iso.hom (Cat.Hom.isoMk (mapId (↑a : Type u_1)))) (prelaxfunctor.map f) ≫
                (Bicategory.leftUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
        X
⊢ prelaxfunctor.map₂ (Bicategory.leftUnitor f).hom =
    (Cat.Hom.isoMk (mapComp (Cat.Hom.toFunctor (𝟙 a)) f.toFunctor)).hom ≫
      Bicategory.whiskerRight (Iso.hom (Cat.Hom.isoMk (mapId (↑a : Type u_1)))) (prelaxfunctor.map f) ≫
        (Bicategory.leftUnitor (prelaxfunctor.map f)).hom

Tactic:
ext X