awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
X : C
K : J ⥤ Over.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t t₁ t₂ : Cone K
f : t₁ ⟶ t₂
a : J
⊢ Eq (α :=
    Cone.pt.{w', v₁, w, u₁} (J := WithTerminal J) (F := Functor.obj liftFromOver K)
        { pt := t₁.pt.left,
          π :=
            {
              app := fun (x : WithTerminal J) ↦
                match (motive :=
                  (x : WithTerminal J) →
                    Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithTerminal J)) t₁.pt.left) x ⟶
                      (Functor.obj liftFromOver K).obj x)
                  x with
                | of a => Over.Hom.left (t₁.π.app a)
                | star => t₁.pt.hom,
              naturality := ⋯ :
              NatTrans (Functor.obj (Functor.const (WithTerminal J)) t₁.pt.left) (Functor.obj liftFromOver K) } :
          Cone (Functor.obj liftFromOver K) } ⟶
      (Functor.obj liftFromOver K).obj (of a))
    (Over.Hom.left f.hom ≫
      NatTrans.app
        (Cone.π
          { pt := t₂.pt.left,
            π :=
              {
                app := fun (x : WithTerminal J) ↦
                  match (motive :=
                    (x : WithTerminal J) →
                      Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithTerminal J)) t₂.pt.left) x ⟶
                        (Functor.obj liftFromOver K).obj x)
                    x with
                  | of a => Over.Hom.left (t₂.π.app a)
                  | star => t₂.pt.hom,
                naturality := ⋯ } })
        (of a))
    (NatTrans.app
      (Cone.π
        { pt := t₁.pt.left,
          π :=
            {
              app := fun (x : WithTerminal J) ↦
                match (motive :=
                  (x : WithTerminal J) →
                    Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithTerminal J)) t₁.pt.left) x ⟶
                      (Functor.obj liftFromOver K).obj x)
                  x with
                | of a => Over.Hom.left (t₁.π.app a)
                | star => t₁.pt.hom,
              naturality := ⋯ } })
      (of a))

Tactic:
simp [← Comma.comp_left]

Premises used: CategoryTheory.Comma.comp_left
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
X : C
K : J ⥤ Over.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t_1 : Cone K
t : Cone (Functor.obj liftFromOver K)
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    Over.left (X := X)
        (Functor.obj
            (Functor.obj (Functor.const J)
              (Over.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t.pt)
                  star)
                (t.π.app star)))
            x :
          Over.{v₁, u₁} X) ⟶
      (K.obj x_1).left)
    (Over.Hom.left
        (CategoryStruct.comp (Y :=
          Functor.obj
            (Functor.obj (Functor.const J)
              (Over.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t.pt)
                  star)
                (t.π.app star)))
            x_1)
          (Functor.map
            (Functor.obj (Functor.const J)
              (Over.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t.pt)
                  star)
                (t.π.app star)))
            f)
          (Over.homMk (t.π.app (of x_1)) ⋯)) :
      Over.left (X := X)
          (Functor.obj
              (Functor.obj (Functor.const J)
                (Over.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t.pt)
                    star)
                  (t.π.app star)))
              x :
            Over.{v₁, u₁} X) ⟶
        (K.obj x_1).left)
    (Over.Hom.left (Over.homMk (t.π.app (of x)) ⋯ ≫ K.map f) :
      Over.left (X := X)
          (Functor.obj
              (Functor.obj (Functor.const J)
                (Over.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t.pt)
                    star)
                  (t.π.app star)))
              x :
            Over.{v₁, u₁} X) ⟶
        (K.obj x_1).left)

Tactic:
simpa using (t.w (incl.map f)).symm

Premises used: CategoryTheory.WithTerminal.incl, CategoryTheory.Functor.map, CategoryTheory.Limits.Cone.w, Eq.symm
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
X : C
K : J ⥤ Over.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t : Cone K
t₁ t₂ : Cone (Functor.obj liftFromOver K)
f : t₁ ⟶ t₂
⊢ Eq (α :=
    Over.left (X := X)
        (Cone.pt (J := J) (F := K)
            {
              pt :=
                Over.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₁.pt)
                    star)
                  (t₁.π.app star),
              π :=
                { app := fun (a : J) ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ :
                  NatTrans
                    (Functor.obj (Functor.const J)
                      (Over.mk (Y :=
                        Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J)
                          (Functor.obj (Functor.const (WithTerminal J)) t₁.pt) star)
                        (t₁.π.app star)))
                    K } :
              Cone K } :
          Over.{v₁, u₁} X) ⟶
      X)
    (f.hom ≫
      Over.hom
        (Cone.pt (J := J) (F := K)
          {
            pt :=
              Over.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₂.pt)
                  star)
                (t₂.π.app star),
            π := { app := fun (a : J) ↦ Over.homMk (t₂.π.app (of a)) ⋯, naturality := ⋯ } }))
    (Over.hom
      (Cone.pt (J := J) (F := K)
        {
          pt :=
            Over.mk (Y :=
              Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t₁.pt)
                star)
              (t₁.π.app star),
          π := { app := fun (a : J) ↦ Over.homMk (t₁.π.app (of a)) ⋯, naturality := ⋯ } }))

Tactic:
simp [dsimp% f.w star]

Premises used: CategoryTheory.Limits.ConeMorphism.w, CategoryTheory.WithTerminal.star
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type w
inst_1 : Category.{w', w} J
X : C
K : J ⥤ Over.{v₁, u₁} X
t : Cone K
⊢ (Functor.obj (Equivalence.functor coneEquiv) t).π.app star = t.pt.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type w
inst_1 : Category.{w', w} J
X : C
K : J ⥤ Over.{v₁, u₁} X
t : Cone K
Y : J
⊢ (Functor.obj (Equivalence.functor coneEquiv) t).π.app (of Y) = Over.Hom.left (t.π.app Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type w
inst_1 : Category.{w', w} J
X : C
F : J ⥤ Over.{v₁, u₁} X
inst_2 : HasLimit (Functor.obj liftFromOver F)
⊢ HasLimit F

Tactic:
⟨_, isLimitEquiv <| .ofIsoLimit
    (limit.isLimit (liftFromOver.obj F)) (coneEquiv.counitIso.app _).symm⟩

Premises used: CategoryTheory.WithTerminal.coneEquiv, CategoryTheory.WithTerminal.isLimitEquiv, Nonempty.intro, CategoryTheory.Limits.limit.isLimit, CategoryTheory.WithTerminal.liftFromOver, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Limits.IsLimit.ofIsoLimit, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
X : C
K : J ⥤ Under.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t_1 t : Cocone K
x : Quiver.Hom.{w', w} (V := WithInitial J) star star
⊢ Eq (α :=
    (Functor.obj liftFromUnder K).obj star ⟶
      Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt.right) star)
    ((Functor.obj liftFromUnder K).map x ≫
      match (motive :=
        (x : WithInitial J) →
          (Functor.obj liftFromUnder K).obj x ⟶
            Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t.pt.right) x)
        star with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom)
    ((match (motive :=
        (x : WithInitial J) →
          (Functor.obj liftFromUnder K).obj x ⟶
            Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t.pt.right) x)
        star with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) ≫
      Functor.map (Functor.obj (Functor.const (WithInitial J)) t.pt.right) x)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
X : C
K : J ⥤ Under.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t_1 t : Cocone K
b : J
x : star ⟶ of b
⊢ Eq (α :=
    (Functor.obj liftFromUnder K).obj star ⟶
      Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t.pt.right) (of b))
    ((Functor.obj liftFromUnder K).map x ≫
      match (motive :=
        (x : WithInitial J) →
          (Functor.obj liftFromUnder K).obj x ⟶
            Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t.pt.right) x)
        of b with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom)
    ((match (motive :=
        (x : WithInitial J) →
          (Functor.obj liftFromUnder K).obj x ⟶
            Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t.pt.right) x)
        star with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) ≫
      Functor.map (Functor.obj (Functor.const (WithInitial J)) t.pt.right) x)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
X : C
K : J ⥤ Under.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t_1 t : Cocone K
a b : J
f : of a ⟶ of b
⊢ Eq (α :=
    (Functor.obj liftFromUnder K).obj (of a) ⟶
      Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t.pt.right) (of b))
    ((Functor.obj liftFromUnder K).map f ≫
      match (motive :=
        (x : WithInitial J) →
          (Functor.obj liftFromUnder K).obj x ⟶
            Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t.pt.right) x)
        of b with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom)
    ((match (motive :=
        (x : WithInitial J) →
          (Functor.obj liftFromUnder K).obj x ⟶
            Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithInitial J)) t.pt.right) x)
        of a with
      | of a => Under.Hom.right (t.ι.app a)
      | star => t.pt.hom) ≫
      Functor.map (Functor.obj (Functor.const (WithInitial J)) t.pt.right) f)

Tactic:
simp [← Comma.comp_right]

Premises used: CategoryTheory.Comma.comp_right
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
X : C
K : J ⥤ Under.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t_1 : Cocone K
t : Cocone (Functor.obj liftFromUnder K)
x x_1 : J
f : x ⟶ x_1
h :
  Eq (α :=
    (K.obj x).right ⟶
      Under.right (X := X)
        (Functor.obj
            (Functor.obj (Functor.const J)
              (Under.mk (Y :=
                Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt)
                  star)
                (t.ι.app star)))
            x_1 :
          Under.{v₁, u₁} X))
    (Under.Hom.right (K.map f ≫ Under.homMk (t.ι.app (of x_1)) ⋯))
    (Under.Hom.right
      (CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.obj (Functor.const J)
            (Under.mk (Y :=
              Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt) star)
              (t.ι.app star)))
          x)
        (Under.homMk (t.ι.app (of x)) ⋯)
        (Functor.map
          (Functor.obj (Functor.const J)
            (Under.mk (Y :=
              Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt) star)
              (t.ι.app star)))
          f)))
⊢ Eq (α :=
    K.obj x ⟶
      Functor.obj
        (Functor.obj (Functor.const J)
          (Under.mk (Y :=
            Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt) star)
            (t.ι.app star)))
        x_1)
    (K.map f ≫ Under.homMk (t.ι.app (of x_1)) ⋯)
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const J)
          (Under.mk (Y :=
            Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt) star)
            (t.ι.app star)))
        x)
      (Under.homMk (t.ι.app (of x)) ⋯)
      (Functor.map
        (Functor.obj (Functor.const J)
          (Under.mk (Y :=
            Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt) star)
            (t.ι.app star)))
        f))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
X : C
K : J ⥤ Under.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t : Cocone K
t₁ t₂ : Cocone (Functor.obj liftFromUnder K)
f : t₁ ⟶ t₂
j : J
⊢ Eq (α :=
    (K.obj j).right ⟶
      Under.right (X := X)
        (Cocone.pt (J := J) (F := K)
            {
              pt :=
                Under.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₂.pt)
                    star)
                  (t₂.ι.app star),
              ι := { app := fun (a : J) ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } } :
          Under.{v₁, u₁} X))
    (Under.Hom.right
        (CategoryStruct.comp (Y :=
          Cocone.pt (J := J) (F := K)
            {
              pt :=
                Under.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₁.pt)
                    star)
                  (t₁.ι.app star),
              ι := { app := fun (a : J) ↦ Under.homMk (t₁.ι.app (of a)) ⋯, naturality := ⋯ } })
          (NatTrans.app
            (Cocone.ι
              {
                pt :=
                  Under.mk (Y :=
                    Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₁.pt)
                      star)
                    (t₁.ι.app star),
                ι := { app := fun (a : J) ↦ Under.homMk (t₁.ι.app (of a)) ⋯, naturality := ⋯ } })
            j)
          (Under.homMk f.hom ⋯)) :
      (K.obj j).right ⟶
        Under.right (X := X)
          (Cocone.pt (J := J) (F := K)
              {
                pt :=
                  Under.mk (Y :=
                    Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₂.pt)
                      star)
                    (t₂.ι.app star),
                ι := { app := fun (a : J) ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } } :
            Under.{v₁, u₁} X))
    (Under.Hom.right
        (NatTrans.app
          (Cocone.ι
            {
              pt :=
                Under.mk (Y :=
                  Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₂.pt)
                    star)
                  (t₂.ι.app star),
              ι := { app := fun (a : J) ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } })
          j) :
      (K.obj j).right ⟶
        Under.right (X := X)
          (Cocone.pt (J := J) (F := K)
              {
                pt :=
                  Under.mk (Y :=
                    Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t₂.pt)
                      star)
                    (t₂.ι.app star),
                ι := { app := fun (a : J) ↦ Under.homMk (t₂.ι.app (of a)) ⋯, naturality := ⋯ } } :
            Under.{v₁, u₁} X))

Tactic:
simp [dsimp% f.w (of j)]

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.WithInitial.of
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type w
inst_1 : Category.{w', w} J
X : C
K : J ⥤ Under.{v₁, u₁} X
t : Cocone K
⊢ (Functor.obj (Equivalence.functor coconeEquiv) t).ι.app star = t.pt.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type w
inst_1 : Category.{w', w} J
X : C
K : J ⥤ Under.{v₁, u₁} X
t : Cocone K
Y : J
⊢ (Functor.obj (Equivalence.functor coconeEquiv) t).ι.app (of Y) = Under.Hom.right (t.ι.app Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Cone
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type w
inst_1 : Category.{w', w} J
X : C
F : J ⥤ Under.{v₁, u₁} X
inst_2 : HasColimit (Functor.obj liftFromUnder F)
⊢ HasColimit F

Tactic:
⟨_, isColimitEquiv <| .ofIsoColimit
    (colimit.isColimit (liftFromUnder.obj F)) (coconeEquiv.counitIso.app _).symm⟩

Premises used: CategoryTheory.WithInitial.liftFromUnder, CategoryTheory.WithInitial.coconeEquiv, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.ofIsoColimit, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.WithInitial.isColimitEquiv, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.WithTerminal.FinCategory
Goal:
C : Type u
inst : Category.{v, u} C
a : Option C
none :
  Eq.{u + 1} (α := Option C)
    ((fun (x : WithTerminal C) ↦
        (match (motive := WithTerminal C → Option C) x with
          | of a => Option.some a
          | star => Option.none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithTerminal C) x with
            | Option.some a => of a
            | Option.none => star :
            WithTerminal C))
        Option.none))
    Option.none
some :
  ∀ (val : C),
    (fun (x : WithTerminal C) ↦
          (match (motive := WithTerminal C → Option C) x with
            | of a => Option.some a
            | star => Option.none :
            Option C))
        ((fun (x : Option C) ↦
            (match (motive := Option C → WithTerminal C) x with
              | Option.some a => of a
              | Option.none => star :
              WithTerminal C))
          (Option.some val)) =
      Option.some val
⊢ (fun (x : WithTerminal C) ↦
        (match (motive := WithTerminal C → Option C) x with
          | of a => Option.some a
          | star => Option.none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithTerminal C) x with
            | Option.some a => of a
            | Option.none => star :
            WithTerminal C))
        a) =
    a

Tactic:
cases a
-- Module: Mathlib.CategoryTheory.WithTerminal.FinCategory
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq.{u + 1} (α := Option C)
    ((fun (x : WithTerminal C) ↦
        (match (motive := WithTerminal C → Option C) x with
          | of a => some a
          | star => none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithTerminal C) x with
            | some a => of a
            | none => star :
            WithTerminal C))
        none))
    none

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.FinCategory
Goal:
C : Type u
inst : Category.{v, u} C
val : C
⊢ (fun (x : WithTerminal C) ↦
        (match (motive := WithTerminal C → Option C) x with
          | of a => some a
          | star => none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithTerminal C) x with
            | some a => of a
            | none => star :
            WithTerminal C))
        (some val)) =
    some val

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.FinCategory
Goal:
C : Type u
inst : Category.{v, u} C
a : WithTerminal C
of :
  ∀ (a : C),
    (fun (x : Option C) ↦
          (match (motive := Option C → WithTerminal C) x with
            | some a => WithTerminal.of a
            | none => WithTerminal.star :
            WithTerminal C))
        ((fun (x : WithTerminal C) ↦
            (match (motive := WithTerminal C → Option C) x with
              | WithTerminal.of a => some a
              | WithTerminal.star => none :
              Option C))
          (WithTerminal.of a)) =
      WithTerminal.of a
star :
  Eq.{u + 1} (α := WithTerminal C)
    ((fun (x : Option C) ↦
        (match (motive := Option C → WithTerminal C) x with
          | some a => WithTerminal.of a
          | none => WithTerminal.star :
          WithTerminal C))
      ((fun (x : WithTerminal C) ↦
          (match (motive := WithTerminal C → Option C) x with
            | WithTerminal.of a => some a
            | WithTerminal.star => none :
            Option C))
        WithTerminal.star))
    WithTerminal.star
⊢ (fun (x : Option C) ↦
        (match (motive := Option C → WithTerminal C) x with
          | some a => WithTerminal.of a
          | none => WithTerminal.star :
          WithTerminal C))
      ((fun (x : WithTerminal C) ↦
          (match (motive := WithTerminal C → Option C) x with
            | WithTerminal.of a => some a
            | WithTerminal.star => none :
            Option C))
        a) =
    a

Tactic:
cases a
-- Module: Mathlib.CategoryTheory.WithTerminal.FinCategory
Goal:
C : Type u
inst : Category.{v, u} C
a : C
⊢ (fun (x : Option C) ↦
        (match (motive := Option C → WithTerminal C) x with
          | some a => of a
          | none => star :
          WithTerminal C))
      ((fun (x : WithTerminal C) ↦
          (match (motive := WithTerminal C → Option C) x with
            | of a => some a
            | star => none :
            Option C))
        (of a)) =
    of a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.FinCategory
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq.{u + 1} (α := WithTerminal C)
    ((fun (x : Option C) ↦
        (match (motive := Option C → WithTerminal C) x with
          | some a => of a
          | none => star :
          WithTerminal C))
      ((fun (x : WithTerminal C) ↦
          (match (motive := WithTerminal C → Option C) x with
            | of a => some a
            | star => none :
            Option C))
        star))
    star

Tactic:
simp