awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
X Y : (↑s.1 : Type v)
f : X ⟶ Y
j j' : J
h : j ⟶ j'
h₁ :
  Eq (α :=
    Quiver.Hom (V := objects.obj (F.obj j'))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') : (a : limit (F ⋙ objects)) → objects.obj (F.obj j'))
          ((@hom _ types TypeCat.Fun _ _ _ _ _
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
              X :
            limit (F ⋙ objects)) :
        objects.obj (F.obj j'))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') : (a : limit (F ⋙ objects)) → objects.obj (F.obj j'))
          ((@hom _ types TypeCat.Fun _ _ _ _ _
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
              Y :
            limit (F ⋙ objects)) :
        objects.obj (F.obj j')))
    (eqToHom ⋯ ≫ ((s.π.app j).toFunctor ⋙ (F.map h).toFunctor).map f ≫ eqToHom ⋯)
    (eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯)
⊢ Eq (α :=
    Quiver.Hom (V := objects.obj (F.obj j'))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') : (a : limit (F ⋙ objects)) → objects.obj (F.obj j'))
          ((@hom _ types TypeCat.Fun _ _ _ _ _
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
              X :
            limit (F ⋙ objects)) :
        objects.obj (F.obj j'))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') : (a : limit (F ⋙ objects)) → objects.obj (F.obj j'))
          ((@hom _ types TypeCat.Fun _ _ _ _ _
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
              Y :
            limit (F ⋙ objects)) :
        objects.obj (F.obj j')))
    (eqToHom ⋯ ≫ (F.map h).toFunctor.map (eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯)
    (eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯)

Tactic:
simp only [Functor.map_comp, eqToHom_map, ← Functor.comp_map, Category.assoc, eqToHom_trans,
          eqToHom_trans_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_map, CategoryTheory.Functor.map_comp, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.Functor.comp_map, CategoryTheory.eqToHom_trans
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
X Y : (↑s.1 : Type v)
f : X ⟶ Y
j j' : J
h : j ⟶ j'
⊢ (s.π.app j ≫ F.map h).toFunctor = (Functor.map (Functor.obj (Functor.const J) s.pt) h ≫ s.π.app j').toFunctor

Tactic:
have := congr($((s.π.naturality h).symm).toFunctor)
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
X Y : (↑s.1 : Type v)
f : X ⟶ Y
j j' : J
h : j ⟶ j'
this : (s.π.app j).toFunctor ⋙ (F.map h).toFunctor = 𝟭 (↑s.pt : Type v) ⋙ (s.π.app j').toFunctor
⊢ (s.π.app j).toFunctor ⋙ (F.map h).toFunctor = (s.π.app j').toFunctor

Tactic:
rw [Functor.id_comp] at this

Premises used: CategoryTheory.Functor.id_comp
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
X Y : (↑s.1 : Type v)
f : X ⟶ Y
j j' : J
h : j ⟶ j'
this : (s.π.app j).toFunctor ⋙ (F.map h).toFunctor = (s.π.app j').toFunctor
h₁ :
  Eq (α :=
    Quiver.Hom (V := objects.obj (F.obj j'))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') : (a : limit (F ⋙ objects)) → objects.obj (F.obj j'))
          ((@hom _ types TypeCat.Fun _ _ _ _ _
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
              X :
            limit (F ⋙ objects)) :
        objects.obj (F.obj j'))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') : (a : limit (F ⋙ objects)) → objects.obj (F.obj j'))
          ((@hom _ types TypeCat.Fun _ _ _ _ _
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
              Y :
            limit (F ⋙ objects)) :
        objects.obj (F.obj j')))
    (eqToHom ⋯ ≫ (eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯)
    (eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯)
⊢ Eq (α :=
    Quiver.Hom (V := objects.obj (F.obj j'))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') : (a : limit (F ⋙ objects)) → objects.obj (F.obj j'))
          ((@hom _ types TypeCat.Fun _ _ _ _ _
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
              X :
            limit (F ⋙ objects)) :
        objects.obj (F.obj j'))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') : (a : limit (F ⋙ objects)) → objects.obj (F.obj j'))
          ((@hom _ types TypeCat.Fun _ _ _ _ _
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
              Y :
            limit (F ⋙ objects)) :
        objects.obj (F.obj j')))
    (eqToHom ⋯ ≫ ((s.π.app j).toFunctor ⋙ (F.map h).toFunctor).map f ≫ eqToHom ⋯)
    (eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯)

Tactic:
rw [Functor.congr_hom this f]

Premises used: CategoryTheory.Functor.congr_hom
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
X Y : (↑s.1 : Type v)
f : X ⟶ Y
j j' : J
h : j ⟶ j'
this : (s.π.app j).toFunctor ⋙ (F.map h).toFunctor = (s.π.app j').toFunctor
⊢ Eq (α :=
    Quiver.Hom (V := objects.obj (F.obj j'))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') : (a : limit (F ⋙ objects)) → objects.obj (F.obj j'))
          ((@hom _ types TypeCat.Fun _ _ _ _ _
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
              X :
            limit (F ⋙ objects)) :
        objects.obj (F.obj j'))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j') : (a : limit (F ⋙ objects)) → objects.obj (F.obj j'))
          ((@hom _ types TypeCat.Fun _ _ _ _ _
                  (limit.lift (F ⋙ objects)
                    { pt := (↑s.pt : Type v),
                      π := { app := fun (j : J) ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }) :
                (a : (↑s.pt : Type v)) → limit (F ⋙ objects))
              Y :
            limit (F ⋙ objects)) :
        objects.obj (F.obj j')))
    (eqToHom ⋯ ≫ (eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯)
    (eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
j : J
h : X = Y
subst :
  Eq (α := (fun (X : Type v) ↦ X) ((homDiagram X X).obj j))
    ((hom (FC := TypeCat.Fun) (limit.π (homDiagram X X) j) :
          (a : (fun (X : Type v) ↦ X) (limit (homDiagram X X))) → (fun (X : Type v) ↦ X) ((homDiagram X X).obj j))
        (eqToHom ⋯) :
      (fun (X : Type v) ↦ X) ((homDiagram X X).obj j))
    (eqToHom ⋯ :
      Quiver.Hom (V := (F ⋙ objects).obj j)
        ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) : (a : limit (F ⋙ objects)) → (F ⋙ objects).obj j) X :
          (F ⋙ objects).obj j)
        ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) : (a : limit (F ⋙ objects)) → (F ⋙ objects).obj j) X :
          (F ⋙ objects).obj j))
⊢ Eq (α := (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
    ((hom (FC := TypeCat.Fun) (limit.π (homDiagram X Y) j) :
          (a : (fun (X : Type v) ↦ X) (limit (homDiagram X Y))) → (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
        (eqToHom h) :
      (fun (X : Type v) ↦ X) ((homDiagram X Y).obj j))
    (eqToHom ⋯ :
      Quiver.Hom (V := (F ⋙ objects).obj j)
        ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) : (a : limit (F ⋙ objects)) → (F ⋙ objects).obj j) X :
          (F ⋙ objects).obj j)
        ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) : (a : limit (F ⋙ objects)) → (F ⋙ objects).obj j) Y :
          (F ⋙ objects).obj j))

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
X : limit (F ⋙ objects)
j : J
⊢ Eq (α := (fun (X : Type v) ↦ X) ((homDiagram X X).obj j))
    ((hom (FC := TypeCat.Fun) (limit.π (homDiagram X X) j) :
          (a : (fun (X : Type v) ↦ X) (limit (homDiagram X X))) → (fun (X : Type v) ↦ X) ((homDiagram X X).obj j))
        (eqToHom ⋯) :
      (fun (X : Type v) ↦ X) ((homDiagram X X).obj j))
    (eqToHom ⋯ :
      Quiver.Hom (V := (F ⋙ objects).obj j)
        ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) : (a : limit (F ⋙ objects)) → (F ⋙ objects).obj j) X :
          (F ⋙ objects).obj j)
        ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) : (a : limit (F ⋙ objects)) → (F ⋙ objects).obj j) X :
          (F ⋙ objects).obj j))

Tactic:
simp [-homDiagram_obj]

Premises used: CategoryTheory.Cat.HasLimits.homDiagram_obj
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
X : (↑s.pt : Type v)
⊢ (limitConeLift F s ≫ (limitCone F).π.app j).toFunctor.obj X = (s.π.app j).toFunctor.obj X

Tactic:
simp [← comp_apply]

Premises used: CategoryTheory.comp_apply
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
symm : limitConeLift F s = m
⊢ m = limitConeLift F s

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
h : (limitConeLift F s).toFunctor = m.toFunctor
⊢ limitConeLift F s = m

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ (limitConeLift F s).toFunctor = m.toFunctor

Tactic:
CategoryTheory.Functor.ext ?_ ?_

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
h : ∀ (X : (↑s.pt : Type v)), (limitConeLift F s).toFunctor.obj X = m.toFunctor.obj X
h₁ :
  ∀ (X Y : (↑s.pt : Type v)) (f : X ⟶ Y),
    (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯
⊢ (limitConeLift F s).toFunctor = m.toFunctor

Tactic:
refine CategoryTheory.Functor.ext ?_ ?_

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X : (↑s.pt : Type v)
h :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
            (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
          ((limitConeLift F s).toFunctor.obj X) :
        (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
      ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
            (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
          (m.toFunctor.obj X) :
        (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
⊢ (limitConeLift F s).toFunctor.obj X = m.toFunctor.obj X

Tactic:
apply Types.limit_ext.{v, v}
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X : (↑s.pt : Type v)
j : J
⊢ Eq (α := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
    ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
        ((limitConeLift F s).toFunctor.obj X) :
      (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
    ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
        (m.toFunctor.obj X) :
      (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))

Tactic:
simp [← comp_apply, ← w j]

Premises used: CategoryTheory.comp_apply
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X Y : (↑s.pt : Type v)
f : X ⟶ Y
⊢ ∀ (j : J),
    Eq (α :=
      Quiver.Hom (V := (↑(F.obj j) : Type v)) (Functor.obj (Hom.toFunctor (s.π.app j)) X)
        (Functor.obj (Hom.toFunctor (s.π.app j)) Y))
      (Functor.map (Hom.toFunctor (s.π.app j)) f)
      (eqToHom ⋯ ≫ Functor.map (Hom.toFunctor (m ≫ (limitCone F).π.app j)) f ≫ eqToHom ⋯)

Tactic:
have (j : _) := Functor.congr_hom congr($((w j).symm).toFunctor) f
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X Y : (↑s.pt : Type v)
f : X ⟶ Y
this :
  ∀ (j : J),
    Eq (α :=
      Quiver.Hom (V := (↑(F.obj j) : Type v)) (Functor.obj (Hom.toFunctor (s.π.app j)) X)
        (Functor.obj (Hom.toFunctor (s.π.app j)) Y))
      (Functor.map (Hom.toFunctor (s.π.app j)) f)
      (eqToHom ⋯ ≫ Functor.map (Hom.toFunctor (m ≫ (limitCone F).π.app j)) f ≫ eqToHom ⋯)
⊢ (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯

Tactic:
simp [this, -homDiagram_obj, limit_π_homDiagram_eqToHom]

Premises used: CategoryTheory.Cat.HasLimits.limit_π_homDiagram_eqToHom, CategoryTheory.Cat.HasLimits.homDiagram_obj
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
J_1 : Type v
inst_1 : Category.{v, v} J_1
F : J_1 ⥤ Cat
⊢ (limit.cone (F ⋙ objects)).pt ≅ (limit.cone (F ⋙ objects)).pt

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Cat.Limit
Goal:
J : Type v
inst : SmallCategory J
J_1 : Type v
inst_1 : Category.{v, v} J_1
F : J_1 ⥤ Cat
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (j : J_1),
    (limit.cone (F ⋙ objects)).π.app j =
      Iso.hom (Iso.refl (limit.cone (F ⋙ objects)).pt) ≫ (objects.mapCone (HasLimits.limitCone F)).π.app j
⊢ ∀ (j : J_1),
    (limit.cone (F ⋙ objects)).π.app j =
      Iso.hom (Iso.refl (limit.cone (F ⋙ objects)).pt) ≫ (objects.mapCone (HasLimits.limitCone F)).π.app j

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Category.Cat.Terminal
Goal:
T : Type u
inst : Category.{v, u} T
inst_1 : Unique T
inst_2 : IsDiscrete.{v, u} T
x : Cat
x_1 : x ⟶ of T
⊢ ∀ (X : (↑x : Type u)),
    x_1.toFunctor.obj X =
      obj
        (Hom.toFunctor
          ((fun (X : Cat.{v, u}) ↦ (toCatHom (obj (const (↑X : Type u)) default) : of (↑X : Type u) ⟶ of T)) x))
        X

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Category.Cat.Terminal
Goal:
⊢ IsDiscrete.{v, u} (ShrinkHoms.{u} PUnit.{u + 1})

Tactic:
have : IsDiscrete (ShrinkHoms.{u} PUnit.{u + 1}) := {
    subsingleton _ _ := { allEq _ _ := eq_of_comp_right_eq (congrFun rfl) }
    eq_of_hom _ := rfl
  }
-- Module: Mathlib.CategoryTheory.Category.Cat.Terminal
Goal:
this : IsDiscrete.{v, u} (ShrinkHoms.{u} PUnit.{u + 1})
⊢ HasTerminal Cat

Tactic:
IsTerminal.hasTerminal (X := Cat.of (ShrinkHoms PUnit)) isTerminalOfUniqueOfIsDiscrete

Premises used: CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscrete, CategoryTheory.Limits.IsTerminal.hasTerminal
-- Module: Mathlib.CategoryTheory.Category.Cat.Terminal
Goal:
this : IsDiscrete.{v, u} (ShrinkHoms.{u} PUnit.{u + 1})
⊢ HasTerminal Cat

Tactic:
exact IsTerminal.hasTerminal (X := Cat.of (ShrinkHoms PUnit)) isTerminalOfUniqueOfIsDiscrete

Premises used: CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscrete, CategoryTheory.Limits.IsTerminal.hasTerminal
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
F G : C ⟶ D
h : F.toFunctor = G.toFunctor
⊢ F = G

Tactic:
congrArg (Functor.toCatHom) h

Premises used: congrArg, CategoryTheory.Functor.toCatHom, CategoryTheory.Cat.of, CategoryTheory.Cat, CategoryTheory.Bundled.of
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Type u
inst : Category.{v, u} C
inst_1 : Category.{v, u} D
F : Functor.{v, v, u, u} C D
⊢ NatTrans.toCatHom₂ (𝟙 F) = 𝟙 F.toCatHom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Type u
inst : Category.{v, u} C
inst_1 : Category.{v, u} D
F G H : Functor.{v, v, u, u} C D
η₁ : F ⟶ G
η₂ : G ⟶ H
⊢ NatTrans.toCatHom₂ (η₁ ≫ η₂) = NatTrans.toCatHom₂ η₁ ≫ NatTrans.toCatHom₂ η₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
F : C ⟶ D
⊢ Hom₂.toNatTrans (𝟙 F) = 𝟙 F.toFunctor

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
F G H : C ⟶ D
η₁ : F ⟶ G
η₂ : G ⟶ H
⊢ (η₁ ≫ η₂).toNatTrans = η₁.toNatTrans ≫ η₂.toNatTrans

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
F G : C ⟶ D
η₁ η₂ : F ⟶ G
h : η₁.toNatTrans = η₂.toNatTrans
⊢ η₁ = η₂

Tactic:
congr($(h).toCatHom₂)

Premises used: congrArg, id, CategoryTheory.NatTrans.toCatHom₂
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y : Cat
F G : X ⟶ Y
e : F ≅ G
⊢ isoMk (toNatIso e) = e

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, CategoryTheory.Cat.of, CategoryTheory.Cat, CategoryTheory.Bundled.of, CategoryTheory.NatTrans.toCatHom₂, rfl, CategoryTheory.Cat.Hom.isoMk
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Type u
inst : Category.{v, u} C
inst_1 : Category.{v, u} D
F G : Functor.{v, v, u, u} C D
e : F ≅ G
⊢ toNatIso (isoMk e) = e

Tactic:
rfl

Premises used: CategoryTheory.Cat.Hom.toNatIso, rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y : Cat
F G : X ⟶ Y
e : F ≅ G
⊢ IsIso e.hom.toNatTrans

Tactic:
(toNatIso e).isIso_hom

Premises used: CategoryTheory.Cat.Hom.toNatIso, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y : Cat
F G : X ⟶ Y
e : F ≅ G
⊢ IsIso e.inv.toNatTrans

Tactic:
(toNatIso e).isIso_inv

Premises used: CategoryTheory.Cat.Hom.toNatIso, CategoryTheory.Iso.isIso_inv
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y : Cat
F G : X ⟶ Y
e : F ≅ G
⊢ e.hom.toNatTrans ≫ e.inv.toNatTrans = 𝟙 F.toFunctor

Tactic:
(toNatIso e).hom_inv_id

Premises used: CategoryTheory.Cat.Hom.toNatIso, CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y : Cat
F G : X ⟶ Y
e : F ≅ G
⊢ e.inv.toNatTrans ≫ e.hom.toNatTrans = 𝟙 G.toFunctor

Tactic:
(toNatIso e).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Cat.Hom.toNatIso
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y : Cat
F G : X ⟶ Y
e : F ≅ G
A : (↑X : Type u)
⊢ e.hom.toNatTrans.app A ≫ e.inv.toNatTrans.app A = 𝟙 (F.toFunctor.obj A)

Tactic:
(toNatIso e).hom_inv_id_app A

Premises used: CategoryTheory.Cat.Hom.toNatIso, CategoryTheory.Iso.hom_inv_id_app
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y : Cat
F G : X ⟶ Y
e : F ≅ G
A : (↑X : Type u)
⊢ e.inv.toNatTrans.app A ≫ e.hom.toNatTrans.app A = 𝟙 (G.toFunctor.obj A)

Tactic:
(toNatIso e).inv_hom_id_app A

Premises used: CategoryTheory.Cat.Hom.toNatIso, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
F : C ⟶ D
ofFunctor :
  ∀ (toFunctor : Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u)),
    𝟙 C ≫ { toFunctor := toFunctor : C.Hom D } = { toFunctor := toFunctor }
⊢ 𝟙 C ≫ F = F

Tactic:
cases F
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
toFunctor : Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u)
⊢ 𝟙 C ≫ { toFunctor := toFunctor : C.Hom D } = { toFunctor := toFunctor }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
F : C ⟶ D
ofFunctor :
  ∀ (toFunctor : Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u)),
    { toFunctor := toFunctor : C.Hom D } ≫ 𝟙 D = { toFunctor := toFunctor : C.Hom D }
⊢ F ≫ 𝟙 D = F

Tactic:
cases F
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
toFunctor : Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u)
⊢ { toFunctor := toFunctor : C.Hom D } ≫ 𝟙 D = { toFunctor := toFunctor : C.Hom D }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
a b c d : Cat
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C : Cat
⊢ toFunctor (𝟙 C) = 𝟭 (↑C : Type u)

Tactic:
rfl

Premises used: CategoryTheory.Functor.id, rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C : Cat
X : (↑C : Type u)
⊢ (toFunctor (𝟙 C)).obj X = X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C : Cat
X Y : (↑C : Type u)
f : X ⟶ Y
⊢ (toFunctor (𝟙 C)).map f = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D E : Cat
F : C ⟶ D
G : D ⟶ E
⊢ (F ≫ G).toFunctor = F.toFunctor ⋙ G.toFunctor

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D E : Cat
F : C ⟶ D
G : D ⟶ E
X : (↑C : Type u)
⊢ (F ≫ G).toFunctor.obj X = G.toFunctor.obj (F.toFunctor.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D E : Cat
F : C ⟶ D
G : D ⟶ E
X Y : (↑C : Type u)
f : X ⟶ Y
⊢ (F ≫ G).toFunctor.map f = G.toFunctor.map (F.toFunctor.map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
F : C ⟶ D
X : (↑C : Type u)
⊢ (toNatTrans (𝟙 F)).app X = 𝟙 (F.toFunctor.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
F G H : C ⟶ D
α : F ⟶ G
β : G ⟶ H
X : (↑C : Type u)
⊢ (α ≫ β).toNatTrans.app X = α.toNatTrans.app X ≫ β.toNatTrans.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
F G : C ⟶ D
h : F = G
refl : toNatTrans (eqToHom ⋯) = eqToHom ⋯
⊢ toNatTrans (eqToHom h) = eqToHom ⋯

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
F : C ⟶ D
⊢ toNatTrans (eqToHom ⋯) = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D : Cat
F G : C ⟶ D
h : F = G
X : (↑C : Type u)
⊢ (Hom₂.toNatTrans (eqToHom h)).app X = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D E : Cat
F : C ⟶ D
G H : D ⟶ E
η : G ⟶ H
⊢ (F ◁ η).toNatTrans = F.toFunctor.whiskerLeft η.toNatTrans

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerLeft, rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D E : Cat
F : C ⟶ D
G H : D ⟶ E
η : G ⟶ H
X : (↑C : Type u)
⊢ (F ◁ η).toNatTrans.app X = η.toNatTrans.app (F.toFunctor.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D E : Cat
F G : C ⟶ D
H : D ⟶ E
η : F ⟶ G
⊢ (η ▷ H).toNatTrans = Functor.whiskerRight η.toNatTrans H.toFunctor

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerRight, rfl