awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x y : WidePullbackShape J
f : x ⟶ y
⊢ (fun
          (f :
            Quiver.Hom (V := WithTerminal (Discrete J))
              ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) x :
                WithTerminal (Discrete J))
              ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) y :
                WithTerminal (Discrete J))) ↦
        (match (motive :=
            (x y : WidePullbackShape J) →
              (f :
                  Quiver.Hom (V := WithTerminal (Discrete J))
                    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) x :
                      WithTerminal (Discrete J))
                    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) y :
                      WithTerminal (Discrete J))) →
                x ⟶ y)
            x, y, f with
          | some x, some y, f => cast ⋯ (Hom.id (some y))
          | none, some y, f => PEmpty.casesOn (fun (t : PEmpty.{u_1 + 1}) ↦ (h : f = t) → none ⟶ some y) f ⋯
          | some x, none, f => Hom.term x
          | none, none, f => Hom.id none :
          x ⟶ y))
      ((fun (x_1 : x ⟶ y) ↦
          (match (motive :=
              (y x : WidePullbackShape J) →
                (x ⟶ y) →
                  Quiver.Hom (V := WithTerminal (Discrete J))
                    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) x :
                      WithTerminal (Discrete J))
                    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) y :
                      WithTerminal (Discrete J)))
              y, x, x_1 with
            | .(none), .(some j), Hom.term j => PUnit.unit
            | y, .(y), Hom.id .(y) =>
              𝟙 ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) y) :
            Quiver.Hom (V := WithTerminal (Discrete J))
              ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) x :
                WithTerminal (Discrete J))
              ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) y :
                WithTerminal (Discrete J))))
        f) =
    f

Tactic:
apply Subsingleton.allEq

Premises used: Subsingleton.allEq
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x y_1 : WidePullbackShape J
y : J
f :
  Quiver.Hom (V := WithTerminal (Discrete J))
    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) none :
      WithTerminal (Discrete J))
    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some y) :
      WithTerminal (Discrete J))
⊢ (fun (x : none ⟶ some y) ↦
        (match (motive :=
            (y x : WidePullbackShape J) →
              (x ⟶ y) →
                Quiver.Hom (V := WithTerminal (Discrete J))
                  ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) x :
                    WithTerminal (Discrete J))
                  ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) y :
                    WithTerminal (Discrete J)))
            some y, none, x with
          | .(none), .(some j), Hom.term j => PUnit.unit
          | y, .(y), Hom.id .(y) =>
            𝟙 ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) y) :
          Quiver.Hom (V := WithTerminal (Discrete J))
            ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) none :
              WithTerminal (Discrete J))
            ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some y) :
              WithTerminal (Discrete J))))
      ((fun
            (f :
              Quiver.Hom (V := WithTerminal (Discrete J))
                ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) none :
                  WithTerminal (Discrete J))
                ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some y) :
                  WithTerminal (Discrete J))) ↦
          (match (motive :=
              (x y : WidePullbackShape J) →
                (f :
                    Quiver.Hom (V := WithTerminal (Discrete J))
                      ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) x :
                        WithTerminal (Discrete J))
                      ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) y :
                        WithTerminal (Discrete J))) →
                  x ⟶ y)
              none, some y, f with
            | some x, some y, f => cast ⋯ (Hom.id (some y))
            | none, some y, f => PEmpty.casesOn (fun (t : PEmpty.{u_1 + 1}) ↦ (h : f = t) → none ⟶ some y) f ⋯
            | some x, none, f => Hom.term x
            | none, none, f => Hom.id none :
            none ⟶ some y))
        f) =
    f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
X Y : WithTerminal (Discrete J)
f : X ⟶ Y
⊢ (widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J))
      ((Equiv.symm widePullbackShapeEquivObj : (a : WithTerminal (Discrete J)) → WidePullbackShape J) X :
        WidePullbackShape J) =
    X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
X Y : WithTerminal (Discrete J)
f : X ⟶ Y
⊢ Y =
    (widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J))
      ((Equiv.symm widePullbackShapeEquivObj : (a : WithTerminal (Discrete J)) → WidePullbackShape J) Y :
        WidePullbackShape J)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x : WidePullbackShape J
⊢ Functor.obj (𝟭 (WidePullbackShape J)) x =
    Functor.obj
      ({ obj := (⇑widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)),
          map := fun {X Y : WidePullbackShape J} ↦
            (⇑(widePullbackShapeEquivMap X Y) :
              (a : X ⟶ Y) →
                (widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) X ⟶
                  (widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) Y),
          map_id := ⋯, map_comp := ⋯ : WidePullbackShape J ⥤ WithTerminal (Discrete J) } ⋙
        { obj := (⇑(Equiv.symm widePullbackShapeEquivObj) : (a : WithTerminal (Discrete J)) → WidePullbackShape J),
          map := fun {X Y : WithTerminal (Discrete J)} (f : X ⟶ Y) ↦
            (Equiv.symm
                  (widePullbackShapeEquivMap
                    ((Equiv.symm widePullbackShapeEquivObj : (a : WithTerminal (Discrete J)) → WidePullbackShape J) X)
                    ((Equiv.symm widePullbackShapeEquivObj : (a : WithTerminal (Discrete J)) → WidePullbackShape J)
                      Y)) :
                (a :
                    (widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J))
                        ((widePullbackShapeEquivObj.symm : (a : WithTerminal (Discrete J)) → WidePullbackShape J) X) ⟶
                      (widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J))
                        ((widePullbackShapeEquivObj.symm : (a : WithTerminal (Discrete J)) → WidePullbackShape J) Y)) →
                  (widePullbackShapeEquivObj.symm : (a : WithTerminal (Discrete J)) → WidePullbackShape J) X ⟶
                    (widePullbackShapeEquivObj.symm : (a : WithTerminal (Discrete J)) → WidePullbackShape J) Y)
              (eqToHom ⋯ ≫ f ≫ eqToHom ⋯),
          map_id := ⋯, map_comp := ⋯ })
      x

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x : WithTerminal (Discrete J)
⊢ Functor.obj
      ({ obj := (⇑(Equiv.symm widePullbackShapeEquivObj) : (a : WithTerminal (Discrete J)) → WidePullbackShape J),
          map := fun {X Y : WithTerminal (Discrete J)} (f : X ⟶ Y) ↦
            (Equiv.symm
                  (widePullbackShapeEquivMap
                    ((Equiv.symm widePullbackShapeEquivObj : (a : WithTerminal (Discrete J)) → WidePullbackShape J) X)
                    ((Equiv.symm widePullbackShapeEquivObj : (a : WithTerminal (Discrete J)) → WidePullbackShape J)
                      Y)) :
                (a :
                    (widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J))
                        ((widePullbackShapeEquivObj.symm : (a : WithTerminal (Discrete J)) → WidePullbackShape J) X) ⟶
                      (widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J))
                        ((widePullbackShapeEquivObj.symm : (a : WithTerminal (Discrete J)) → WidePullbackShape J) Y)) →
                  (widePullbackShapeEquivObj.symm : (a : WithTerminal (Discrete J)) → WidePullbackShape J) X ⟶
                    (widePullbackShapeEquivObj.symm : (a : WithTerminal (Discrete J)) → WidePullbackShape J) Y)
              (eqToHom ⋯ ≫ f ≫ eqToHom ⋯),
          map_id := ⋯, map_comp := ⋯ } ⋙
        { obj := (⇑widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)),
          map := fun {X Y : WidePullbackShape J} ↦
            (⇑(widePullbackShapeEquivMap X Y) :
              (a : X ⟶ Y) →
                (widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) X ⟶
                  (widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) Y),
          map_id := ⋯, map_comp := ⋯ : WidePullbackShape J ⥤ WithTerminal (Discrete J) })
      x =
    Functor.obj (𝟭 (WithTerminal (Discrete J))) x

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : (of X).Hom star
⊢ False

Tactic:
(f : PEmpty).elim

Premises used: PEmpty.elim
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ Eq.{v + 1} (α := X ⟶ X) (down (𝟙 (of X))) (𝟙 X)

Tactic:
rfl

Premises used: CategoryTheory.WithInitial.id, CategoryTheory.WithInitial.down, rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : of X ⟶ of Y
g : of Y ⟶ of Z
⊢ down (f ≫ g) = down f ≫ down g

Tactic:
rfl

Premises used: CategoryTheory.WithInitial.down, CategoryTheory.WithInitial.comp, rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : of X ⟶ star
⊢ False

Tactic:
(f : PEmpty).elim

Premises used: PEmpty.elim
-- 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 : WithInitial 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 : WithInitial C) → (map F).obj X ⟶ (map G).obj X) of y with
      | of x => η.app x
      | star => 𝟙 star)
    ((match (motive := (X : WithInitial C) → (map F).obj X ⟶ (map G).obj X) of x with
      | of x => η.app x
      | star => 𝟙 star) ≫
      (map G).map f)

Tactic:
η.naturality f

Premises used: CategoryTheory.WithInitial.down, CategoryTheory.NatTrans.naturality, CategoryTheory.WithInitial.comp, CategoryTheory.WithInitial.Hom
-- 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 : WithInitial 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 : WithInitial C) → (map F).obj X ⟶ (map G).obj X) of y with
      | of x => η.app x
      | star => 𝟙 star)
    ((match (motive := (X : WithInitial 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 : WithInitial C
f : X ⟶ Y
x : C
x_1 : star ⟶ of x
⊢ ((map F).map x_1 ≫
      match (motive := (X : WithInitial C) → (map F).obj X ⟶ (map G).obj X) of x with
      | of x => η.app x
      | star => 𝟙 star) =
    (match (motive := (X : WithInitial C) → (map F).obj X ⟶ (map G).obj X) star 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 : WithInitial C
f : X ⟶ Y
x : Quiver.Hom.{v, u} (V := WithInitial C) star star
⊢ ((map F).map x ≫
      match (motive := (X : WithInitial C) → (map F).obj X ⟶ (map G).obj X) star with
      | of x => η.app x
      | star => 𝟙 star) =
    (match (motive := (X : WithInitial 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 : WithInitial C
f : X ⟶ Y
⊢ Eq (α := (map F).obj X ⟶ (map G).obj Y)
    ((map F).map f ≫
      match (motive := (X : WithInitial C) → (map F).obj X ⟶ (map G).obj X) Y with
      | of x => η.app x
      | star => 𝟙 star)
    ((match (motive := (X : WithInitial 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
    | star, of x, _ => 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 (WithInitial (↑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 (WithInitial (↑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 g h_1 : a ⟶ b
η : f ⟶ g
θ : g ⟶ h_1
h :
  ∀ (X : (↑(Cat.of (WithInitial (↑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 (WithInitial (↑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 c d : Cat
f : a ⟶ b
g : b ⟶ c
h_1 : c ⟶ d
h :
  ∀ (X : (↑(prelaxfunctor.obj a) : Type u_1)),
    (prelaxfunctor.map₂ (Bicategory.associator f g h_1).hom).toNatTrans.app X =
      ((Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h_1.toFunctor)).hom ≫
              Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h_1) ≫
                (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h_1)).hom ≫
                  Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv ≫
                    (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ h_1).toFunctor)).inv).toNatTrans.app
        X
⊢ prelaxfunctor.map₂ (Bicategory.associator f g h_1).hom =
    (Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h_1.toFunctor)).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h_1) ≫
        (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h_1)).hom ≫
          Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv ≫
            (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ 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 : (↑(prelaxfunctor.obj a) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α :=
      (prelaxfunctor.map ((f ≫ g) ≫ h_1)).toFunctor.obj (of a_1) ⟶
        (prelaxfunctor.map (f ≫ g ≫ h_1)).toFunctor.obj (of a_1))
      ((prelaxfunctor.map₂ (Bicategory.associator f g h_1).hom).toNatTrans.app (of a_1))
      (((Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h_1.toFunctor)).hom ≫
              Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h_1) ≫
                (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h_1)).hom ≫
                  Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv ≫
                    (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ h_1).toFunctor)).inv).toNatTrans.app
        (of a_1))
h₁ :
  Eq (α :=
    (prelaxfunctor.map ((f ≫ g) ≫ h_1)).toFunctor.obj star ⟶ (prelaxfunctor.map (f ≫ g ≫ h_1)).toFunctor.obj star)
    ((prelaxfunctor.map₂ (Bicategory.associator f g h_1).hom).toNatTrans.app star)
    (((Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h_1.toFunctor)).hom ≫
            Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h_1) ≫
              (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h_1)).hom ≫
                Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv ≫
                  (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ h_1).toFunctor)).inv).toNatTrans.app
      star)
⊢ (prelaxfunctor.map₂ (Bicategory.associator f g h_1).hom).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h_1.toFunctor)).hom ≫
            Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h_1) ≫
              (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h_1)).hom ≫
                Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv ≫
                  (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ 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 (α :=
    (prelaxfunctor.map ((f ≫ g) ≫ h)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map (f ≫ g ≫ h)).toFunctor.obj (of a_1))
    ((prelaxfunctor.map₂ (Bicategory.associator f g h).hom).toNatTrans.app (of a_1))
    (((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).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 (α := (prelaxfunctor.map ((f ≫ g) ≫ h)).toFunctor.obj star ⟶ (prelaxfunctor.map (f ≫ g ≫ h)).toFunctor.obj star)
    ((prelaxfunctor.map₂ (Bicategory.associator f g h).hom).toNatTrans.app star)
    (((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).toNatTrans.app
      star)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : WithInitial C
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (a : star ⟶ X),
    a =
      match (motive := (X : WithInitial C) → star ⟶ X) X with
      | of _x => PUnit.unit
      | star => PUnit.unit
⊢ ∀ (a : star ⟶ X),
    a =
      match (motive := (X : WithInitial C) → star ⟶ X) X with
      | of _x => PUnit.unit
      | star => PUnit.unit

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Limits.HasInitial.{v, u} (WithInitial C)

Tactic:
Limits.hasInitial_of_unique star

Premises used: CategoryTheory.Limits.hasInitial_of_unique, CategoryTheory.WithInitial.star
-- 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
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
x : C
⊢ (liftStar F M hM).hom ≫ (lift F M hM).map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) =
    M x ≫ (inclLift F M hM).hom.app x

Tactic:
simp [incl]

Premises used: CategoryTheory.WithInitial.incl