awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
h : HasStrongEpiMonoFactorisations.{v_1, u_1} C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this_1 : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
this : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e)
⊢ (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) ≫ F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y = f

Tactic:
simp only [asEquivalence_functor, Category.assoc, ← F.map_comp_assoc,
              MonoFactorisation.fac, fun_inv_map, id_obj, Iso.inv_hom_id_app, Category.comp_id,
              Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, CategoryTheory.Category.assoc, CategoryTheory.Functor.asEquivalence_functor, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.fun_inv_map, CategoryTheory.Functor.id_obj, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.inv_hom_id_app_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Images
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.IsEquivalence
h : HasStrongEpiMonoFactorisations.{v_1, u_1} C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this_1 : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
this : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e)
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
exact
      Nonempty.intro
        { I := F.obj em.I
          e := F.asEquivalence.counitIso.inv.app X ≫ F.map em.e
          m := F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y
          fac := by
            simp only [asEquivalence_functor, Category.assoc, ← F.map_comp_assoc,
              MonoFactorisation.fac, fun_inv_map, id_obj, Iso.inv_hom_id_app, Category.comp_id,
              Iso.inv_hom_id_app_assoc] }

Premises used: Nonempty.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
Y : C
⊢ ∀ ⦃X Y_1 : Discrete PEmpty.{1}⦄ (f : X ⟶ Y_1),
    Eq.{v₁ + 1} (α := Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) X ⟶ F.obj Y_1)
      (Functor.map (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) f ≫
        id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ Y ⟶ F.obj x) Y_1 fun (as : PEmpty.{1}) ↦ ⋯.elim))
      (id (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ Y ⟶ F.obj x) X fun (as : PEmpty.{1}) ↦ ⋯.elim) ≫
        F.map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
Y : C
t :
  IsLimit
    { pt := Y,
      π :=
        {
          app := fun (X : Discrete PEmpty.{1}) ↦
            id
              (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ Y ⟶ F.obj x) X fun (as : PEmpty.{1}) ↦
                ⋯.elim),
          naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) F } :
      Cone F }
X : C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    Eq.{v₁ + 1} (α := Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) X_1 ⟶ F.obj Y)
      (Functor.map (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) f ≫
        id (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ X ⟶ F.obj x) Y fun (as : PEmpty.{1}) ↦ ⋯.elim))
      (id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ X ⟶ F.obj x) X_1 fun (as : PEmpty.{1}) ↦
            ⋯.elim) ≫
        F.map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
Y : C
t :
  IsLimit
    { pt := Y,
      π :=
        {
          app := fun (X : Discrete PEmpty.{1}) ↦
            id
              (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ Y ⟶ F.obj x) X fun (as : PEmpty.{1}) ↦
                ⋯.elim),
          naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) F } :
      Cone F }
X : C
f : X ⟶ Y
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    Eq.{v₁ + 1} (α := Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) X_1 ⟶ F.obj Y)
      (Functor.map (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) f ≫
        id (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ X ⟶ F.obj x) Y fun (as : PEmpty.{1}) ↦ ⋯.elim))
      (id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ X ⟶ F.obj x) X_1 fun (as : PEmpty.{1}) ↦
            ⋯.elim) ≫
        F.map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
Y : C
t :
  IsLimit
    { pt := Y,
      π :=
        {
          app := fun (X : Discrete PEmpty.{1}) ↦
            id
              (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ Y ⟶ F.obj x) X fun (as : PEmpty.{1}) ↦
                ⋯.elim),
          naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) F } :
      Cone F }
X : C
f : X ⟶ Y
⊢ ∀ (j : Discrete PEmpty.{1}),
    f ≫
        { pt := Y,
                π :=
                  {
                    app := fun (X : Discrete PEmpty.{1}) ↦
                      id
                        (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ Y ⟶ F.obj x) X
                          fun (as : PEmpty.{1}) ↦ ⋯.elim),
                    naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) F } :
                Cone F }.π.app
          j =
      { pt := X,
              π :=
                {
                  app := fun (X_1 : Discrete PEmpty.{1}) ↦
                    id
                      (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ X ⟶ F.obj x) X_1
                        fun (as : PEmpty.{1}) ↦ ⋯.elim),
                  naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) F } }.π.app
        j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
Y : C
dsimp :
  ∀
    (x :
      IsLimit
        { pt := Y,
          π :=
            { app := fun (X : Discrete PEmpty.{1}) ↦ ⋯.elim, naturality := ⋯ :
              NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) F } :
          Cone F }),
    { lift := fun (s : Cone F) ↦ default, fac := ⋯, uniq := ⋯ } = x
⊢ Function.LeftInverse
    (fun (u : (X : C) → Unique (X ⟶ Y)) ↦ { lift := fun (s : Cone F) ↦ default, fac := ⋯, uniq := ⋯ })
    fun
      (t :
        IsLimit
          { pt := Y,
            π :=
              {
                app := fun (X : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ Y ⟶ F.obj x) X fun (as : PEmpty.{1}) ↦
                      ⋯.elim),
                naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) F } :
            Cone F })
      (X : C) ↦
    {
      default :=
        t.lift
          { pt := X,
            π :=
              {
                app := fun (X_1 : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ X ⟶ F.obj x) X_1
                      fun (as : PEmpty.{1}) ↦ ⋯.elim),
                naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) F } },
      uniq := ⋯ }

Tactic:
dsimp [Function.LeftInverse]

Premises used: Function.LeftInverse
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
Y : C
x :
  IsLimit
    { pt := Y,
      π :=
        { app := fun (X : Discrete PEmpty.{1}) ↦ ⋯.elim, naturality := ⋯ :
          NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) F } :
      Cone F }
⊢ { lift := fun (s : Cone F) ↦ default, fac := ⋯, uniq := ⋯ } = x

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
Y : C
dsimp : ∀ (x : (X : C) → Unique (X ⟶ Y)), (fun (X : C) ↦ { default := default, uniq := ⋯ }) = x
⊢ Function.RightInverse
    (fun (u : (X : C) → Unique (X ⟶ Y)) ↦ { lift := fun (s : Cone F) ↦ default, fac := ⋯, uniq := ⋯ })
    fun
      (t :
        IsLimit
          { pt := Y,
            π :=
              {
                app := fun (X : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ Y ⟶ F.obj x) X fun (as : PEmpty.{1}) ↦
                      ⋯.elim),
                naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) Y) F } :
            Cone F })
      (X : C) ↦
    {
      default :=
        t.lift
          { pt := X,
            π :=
              {
                app := fun (X_1 : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ X ⟶ F.obj x) X_1
                      fun (as : PEmpty.{1}) ↦ ⋯.elim),
                naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) F } },
      uniq := ⋯ }

Tactic:
dsimp [Function.RightInverse, Function.LeftInverse]

Premises used: Function.LeftInverse, Function.RightInverse
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
Y : C
⊢ ∀ (x : (X : C) → Unique (X ⟶ Y)), (fun (X : C) ↦ { default := default, uniq := ⋯ }) = x

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
X : C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    Eq (α := F.obj X_1 ⟶ Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) Y)
      (F.map f ≫
        id (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X) Y fun (as : PEmpty.{1}) ↦ ⋯.elim))
      (id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X) X_1 fun (as : PEmpty.{1}) ↦
            ⋯.elim) ≫
        Functor.map (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
X_1 : C
t :
  IsColimit
    { pt := X_1,
      ι :=
        {
          app := fun (X_1_1 : Discrete PEmpty.{1}) ↦
            id
              (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X_1) X_1_1 fun (as : PEmpty.{1}) ↦
                ⋯.elim),
          naturality := ⋯ : NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X_1) } :
      Cocone F }
X : C
⊢ ∀ ⦃X_2 Y : Discrete PEmpty.{1}⦄ (f : X_2 ⟶ Y),
    Eq (α := F.obj X_2 ⟶ Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) Y)
      (F.map f ≫
        id (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X) Y fun (as : PEmpty.{1}) ↦ ⋯.elim))
      (id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X) X_2 fun (as : PEmpty.{1}) ↦
            ⋯.elim) ≫
        Functor.map (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
X_1 : C
t :
  IsColimit
    { pt := X_1,
      ι :=
        {
          app := fun (X_1_1 : Discrete PEmpty.{1}) ↦
            id
              (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X_1) X_1_1 fun (as : PEmpty.{1}) ↦
                ⋯.elim),
          naturality := ⋯ : NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X_1) } :
      Cocone F }
X : C
f : X_1 ⟶ X
⊢ ∀ ⦃X_2 Y : Discrete PEmpty.{1}⦄ (f : X_2 ⟶ Y),
    Eq (α := F.obj X_2 ⟶ Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) Y)
      (F.map f ≫
        id (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X) Y fun (as : PEmpty.{1}) ↦ ⋯.elim))
      (id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X) X_2 fun (as : PEmpty.{1}) ↦
            ⋯.elim) ≫
        Functor.map (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
X_1 : C
t :
  IsColimit
    { pt := X_1,
      ι :=
        {
          app := fun (X_1_1 : Discrete PEmpty.{1}) ↦
            id
              (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X_1) X_1_1 fun (as : PEmpty.{1}) ↦
                ⋯.elim),
          naturality := ⋯ : NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X_1) } :
      Cocone F }
X : C
f : X_1 ⟶ X
⊢ ∀ (j : Discrete PEmpty.{1}),
    { pt := X_1,
                ι :=
                  {
                    app := fun (X_1_1 : Discrete PEmpty.{1}) ↦
                      id
                        (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X_1) X_1_1
                          fun (as : PEmpty.{1}) ↦ ⋯.elim),
                    naturality := ⋯ : NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X_1) } :
                Cocone F }.ι.app
          j ≫
        f =
      { pt := X,
              ι :=
                {
                  app := fun (X_2 : Discrete PEmpty.{1}) ↦
                    id
                      (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X) X_2
                        fun (as : PEmpty.{1}) ↦ ⋯.elim),
                  naturality := ⋯ : NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) } }.ι.app
        j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
X : C
dsimp :
  ∀
    (x :
      IsColimit
        { pt := X,
          ι :=
            { app := fun (X_1 : Discrete PEmpty.{1}) ↦ ⋯.elim, naturality := ⋯ :
              NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) } :
          Cocone F }),
    { desc := fun (s : Cocone F) ↦ default, fac := ⋯, uniq := ⋯ :
        IsColimit
          { pt := X,
            ι :=
              { app := fun (X_1 : Discrete PEmpty.{1}) ↦ ⋯.elim, naturality := ⋯ :
                NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) } :
            Cocone F } } =
      x
⊢ Function.LeftInverse
    (fun (u : (Y : C) → Unique (X ⟶ Y)) ↦ { desc := fun (s : Cocone F) ↦ default, fac := ⋯, uniq := ⋯ })
    fun
      (t :
        IsColimit
          { pt := X,
            ι :=
              {
                app := fun (X_1 : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X) X_1
                      fun (as : PEmpty.{1}) ↦ ⋯.elim),
                naturality := ⋯ : NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) } :
            Cocone F })
      (X_1 : C) ↦
    {
      default :=
        t.desc
          { pt := X_1,
            ι :=
              {
                app := fun (X_2 : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X_1) X_2
                      fun (as : PEmpty.{1}) ↦ ⋯.elim),
                naturality := ⋯ : NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X_1) } },
      uniq := ⋯ }

Tactic:
dsimp [Function.LeftInverse]

Premises used: Function.LeftInverse
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
X : C
x :
  IsColimit
    { pt := X,
      ι :=
        { app := fun (X_1 : Discrete PEmpty.{1}) ↦ ⋯.elim, naturality := ⋯ :
          NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) } :
      Cocone F }
⊢ { desc := fun (s : Cocone F) ↦ default, fac := ⋯, uniq := ⋯ :
      IsColimit
        { pt := X,
          ι :=
            { app := fun (X_1 : Discrete PEmpty.{1}) ↦ ⋯.elim, naturality := ⋯ :
              NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) } :
          Cocone F } } =
    x

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
X : C
⊢ Function.RightInverse
    (fun (u : (Y : C) → Unique (X ⟶ Y)) ↦ { desc := fun (s : Cocone F) ↦ default, fac := ⋯, uniq := ⋯ })
    fun
      (t :
        IsColimit
          { pt := X,
            ι :=
              {
                app := fun (X_1 : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X) X_1
                      fun (as : PEmpty.{1}) ↦ ⋯.elim),
                naturality := ⋯ : NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) } :
            Cocone F })
      (X_1 : C) ↦
    {
      default :=
        t.desc
          { pt := X_1,
            ι :=
              {
                app := fun (X_2 : Discrete PEmpty.{1}) ↦
                  id
                    (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X_1) X_2
                      fun (as : PEmpty.{1}) ↦ ⋯.elim),
                naturality := ⋯ : NatTrans F (Functor.obj (Functor.const (Discrete PEmpty.{1})) X_1) } },
      uniq := ⋯ }

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
t : IsTerminal.{v₁, u₁} X
f g : Y ⟶ X
⊢ ∀ (j : Discrete PEmpty.{1}),
    Eq (α := Y ⟶ Functor.obj.{0, v₁, 0, u₁} (Functor.empty C) j) (f ≫ NatTrans.app (Cone.π (asEmptyCone X)) j)
      (g ≫ NatTrans.app (Cone.π (asEmptyCone X)) j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z : C
t : IsTerminal.{v₁, u₁} Z
X Y : C
f : X ⟶ Y
⊢ f ≫ t.from Y = t.from X

Tactic:
t.hom_ext _ _

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
t : IsTerminal.{v₁, u₁} X
⊢ t.from X = 𝟙 X

Tactic:
t.hom_ext _ _

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
t : IsInitial.{v₁, u₁} X
f g : X ⟶ Y
⊢ ∀ (j : Discrete PEmpty.{1}),
    Eq.{v₁ + 1} (α := Functor.obj.{0, v₁, 0, u₁} (Functor.empty C) j ⟶ Y)
      (NatTrans.app (Cocone.ι (asEmptyCocone X)) j ≫ f) (NatTrans.app (Cocone.ι (asEmptyCocone X)) j ≫ g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
t : IsInitial.{v₁, u₁} X
Y Z : C
f : Y ⟶ Z
⊢ t.to Y ≫ f = t.to Z

Tactic:
t.hom_ext _ _

Premises used: CategoryTheory.Limits.IsInitial.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
t : IsInitial.{v₁, u₁} X
⊢ t.to X = 𝟙 X

Tactic:
t.hom_ext _ _

Premises used: CategoryTheory.Limits.IsInitial.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
t : IsTerminal.{v₁, u₁} X
f : X ⟶ Y
⊢ IsSplitMono f

Tactic:
IsSplitMono.mk' ⟨t.from _, t.hom_ext _ _⟩

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.SplitMono.mk, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.IsSplitMono.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
t : IsInitial.{v₁, u₁} X
f : Y ⟶ X
⊢ IsSplitEpi f

Tactic:
IsSplitEpi.mk' ⟨t.to _, t.hom_ext _ _⟩

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.IsInitial.to, CategoryTheory.SplitEpi.mk, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
t : IsTerminal.{v₁, u₁} X
f : X ⟶ Y
⊢ IsSplitMono f

Tactic:
haveI := t.isSplitMono_from f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
t : IsTerminal.{v₁, u₁} X
f : X ⟶ Y
this : IsSplitMono f
⊢ Mono f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
t : IsInitial.{v₁, u₁} X
f : Y ⟶ X
⊢ IsSplitEpi f

Tactic:
haveI := t.isSplitEpi_to f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
t : IsInitial.{v₁, u₁} X
f : Y ⟶ X
this : IsSplitEpi f
⊢ Epi f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
⊢ ∀ ⦃X Y : Discrete PEmpty.{w + 1}⦄ (f : X ⟶ Y),
    Eq.{v₁ + 1} (α :=
      Functor.obj.{w, v₁, w, u₁} (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) X ⟶ F₁.obj Y)
      (Functor.map (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) f ≫
        id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{w + 1}) ↦ c.pt ⟶ F₁.obj x) Y
            fun (as : PEmpty.{w + 1}) ↦ ⋯.elim))
      (id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{w + 1}) ↦ c.pt ⟶ F₁.obj x) X
            fun (as : PEmpty.{w + 1}) ↦ ⋯.elim) ≫
        F₁.map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
dsimp :
  f =
    hl.lift
        { pt := c.pt,
          π :=
            { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ ⋯.elim, naturality := ⋯ :
              NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) F₁ } } ≫
      hi.hom
⊢ f =
    hl.lift
        { pt := c.pt,
          π :=
            {
              app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦
                id
                  (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{w + 1}) ↦ c.pt ⟶ F₁.obj x) X_1
                    fun (as : PEmpty.{w + 1}) ↦ ⋯.elim),
              naturality := ⋯ : NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) F₁ } } ≫
      hi.hom

Tactic:
dsimp