awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
c c' : Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C)
φ : c ⟶ c'
x y : WithTerminal C
f : x ⟶ y
x_1 : Quiver.Hom.{v, u} (V := WithTerminal C) star star
⊢ Eq (α := (ofCommaObject c).obj star ⟶ (ofCommaObject c').obj star)
    ((ofCommaObject c).map x_1 ≫
      match (motive := (x : WithTerminal C) → (ofCommaObject c).obj x ⟶ (ofCommaObject c').obj x) star with
      | of x => φ.left.app x
      | star => φ.right)
    ((match (motive := (x : WithTerminal C) → (ofCommaObject c).obj x ⟶ (ofCommaObject c').obj x) star with
      | of x => φ.left.app x
      | star => φ.right) ≫
      (ofCommaObject c').map x_1)

Tactic:
simp
-- 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 : Functor.{v, v_1, u, u_1} (WithTerminal C) D
x y : C
f : x ⟶ y
simp :
  F.map (Functor.map incl f) ≫ F.map (Limits.IsTerminal.from starTerminal (of y)) =
    F.map (Limits.IsTerminal.from starTerminal (of x))
⊢ Eq (α := (incl ⋙ F).obj x ⟶ F.obj star)
    ((incl ⋙ F).map f ≫ (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) y)
    ((fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) x)

Tactic:
simp only [Functor.comp_obj, Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.comp_map
-- 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 : Functor.{v, v_1, u, u_1} (WithTerminal C) D
x y : C
f : x ⟶ y
rw :
  F.map (Functor.map incl f ≫ Limits.IsTerminal.from starTerminal (of y)) =
    F.map (Limits.IsTerminal.from starTerminal (of x))
⊢ F.map (Functor.map incl f) ≫ F.map (Limits.IsTerminal.from starTerminal (of y)) =
    F.map (Limits.IsTerminal.from starTerminal (of x))

Tactic:
rw [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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 : Functor.{v, v_1, u, u_1} (WithTerminal C) D
x : C
simp :
  F.map (Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x)) =
    F.map (Limits.IsTerminal.from starTerminal (of x))
⊢ F.map (Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x)) ≫ Iso.hom (Iso.refl (F.obj star)) =
    NatTrans.app (Iso.hom (Iso.refl (incl ⋙ F))) x ≫
      (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) x

Tactic:
simp only [Iso.refl_hom, Category.id_comp, Functor.comp_obj,
            NatTrans.id_app, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.id_app, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp
-- 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 : Functor.{v, v_1, u, u_1} (WithTerminal C) D
x : C
⊢ F.map (Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x)) =
    F.map (Limits.IsTerminal.from starTerminal (of 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
x y : Functor.{v, v_1, u, u_1} (WithTerminal C) D
f : x ⟶ y
a : C
⊢ Eq (α :=
    (Functor.obj (𝟭 (Functor.{v, v_1, u, u_1} (WithTerminal C) D)) x).obj (of a) ⟶
      (Functor.obj
            ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithTerminal C) D} ↦ mkCommaMorphism,
                map_id := ⋯, map_comp := ⋯ :
                Functor.{v, v_1, u, u_1} (WithTerminal C) D ⥤
                  Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) } ⋙
              { obj := ofCommaObject,
                map :=
                  fun
                    {X Y :
                      Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C)} ↦
                  ofCommaMorphism,
                map_id := ⋯, map_comp := ⋯ :
                Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) ⥤
                  Functor.{v, v_1, u, u_1} (WithTerminal C) D })
            y).obj
        (of a))
    (NatTrans.app
      (Functor.map (𝟭 (Functor.{v, v_1, u, u_1} (WithTerminal C) D)) f ≫
        Iso.hom
          ((fun (F : Functor.{v, v_1, u, u_1} (WithTerminal C) D) ↦
              (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) ⋯ F
                  (Iso.refl (incl ⋙ F)) (Iso.refl (F.obj star)) ⋯ :
                F ≅
                  lift (Z := F.obj star) (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x)))
                    ⋯))
            y))
      (of a))
    (NatTrans.app
      (Iso.hom
          ((fun (F : Functor.{v, v_1, u, u_1} (WithTerminal C) D) ↦
              (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) ⋯ F
                  (Iso.refl (incl ⋙ F)) (Iso.refl (F.obj star)) ⋯ :
                F ≅
                  lift (Z := F.obj star) (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x)))
                    ⋯))
            x) ≫
        Functor.map
          ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithTerminal C) D} ↦ mkCommaMorphism,
              map_id := ⋯, map_comp := ⋯ :
              Functor.{v, v_1, u, u_1} (WithTerminal C) D ⥤
                Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) } ⋙
            { obj := ofCommaObject,
              map :=
                fun
                  {X Y :
                    Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C)} ↦
                ofCommaMorphism,
              map_id := ⋯, map_comp := ⋯ :
              Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) ⥤
                Functor.{v, v_1, u, u_1} (WithTerminal C) D })
          f)
      (of a))

Tactic:
simp [incl]

Premises used: CategoryTheory.WithTerminal.incl
-- 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
x y : Functor.{v, v_1, u, u_1} (WithTerminal C) D
f : x ⟶ y
⊢ Eq (α :=
    (Functor.obj (𝟭 (Functor.{v, v_1, u, u_1} (WithTerminal C) D)) x).obj star ⟶
      (Functor.obj
            ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithTerminal C) D} ↦ mkCommaMorphism,
                map_id := ⋯, map_comp := ⋯ :
                Functor.{v, v_1, u, u_1} (WithTerminal C) D ⥤
                  Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) } ⋙
              { obj := ofCommaObject,
                map :=
                  fun
                    {X Y :
                      Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C)} ↦
                  ofCommaMorphism,
                map_id := ⋯, map_comp := ⋯ :
                Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) ⥤
                  Functor.{v, v_1, u, u_1} (WithTerminal C) D })
            y).obj
        star)
    (NatTrans.app
      (Functor.map (𝟭 (Functor.{v, v_1, u, u_1} (WithTerminal C) D)) f ≫
        Iso.hom
          ((fun (F : Functor.{v, v_1, u, u_1} (WithTerminal C) D) ↦
              (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) ⋯ F
                  (Iso.refl (incl ⋙ F)) (Iso.refl (F.obj star)) ⋯ :
                F ≅
                  lift (Z := F.obj star) (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x)))
                    ⋯))
            y))
      star)
    (NatTrans.app
      (Iso.hom
          ((fun (F : Functor.{v, v_1, u, u_1} (WithTerminal C) D) ↦
              (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x))) ⋯ F
                  (Iso.refl (incl ⋙ F)) (Iso.refl (F.obj star)) ⋯ :
                F ≅
                  lift (Z := F.obj star) (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsTerminal.from starTerminal (of x)))
                    ⋯))
            x) ≫
        Functor.map
          ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithTerminal C) D} ↦ mkCommaMorphism,
              map_id := ⋯, map_comp := ⋯ :
              Functor.{v, v_1, u, u_1} (WithTerminal C) D ⥤
                Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) } ⋙
            { obj := ofCommaObject,
              map :=
                fun
                  {X Y :
                    Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C)} ↦
                ofCommaMorphism,
              map_id := ⋯, map_comp := ⋯ :
              Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C) ⥤
                Functor.{v, v_1, u, u_1} (WithTerminal C) D })
          f)
      star)

Tactic:
simp [incl]

Premises used: CategoryTheory.WithTerminal.incl
-- 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
x : Functor.{v, v_1, u, u_1} (WithTerminal C) D
h₁ :
  ∀ (x_1 : C),
    NatTrans.app
        (CommaMorphism.left
          (mkCommaMorphism
            (Iso.hom
              (NatIso.ofComponents
                (fun (X : WithTerminal C) ↦
                  match (motive :=
                    (X : WithTerminal C) →
                      x.obj X ≅
                        match (motive := WithTerminal C → D) X with
                        | of x_2 => x.obj (Functor.obj.{v, v, u, u} incl x_2)
                        | star => x.obj star)
                    X with
                  | of x_2 => Iso.app (Iso.refl (incl ⋙ x)) x_2
                  | star => Iso.refl (x.obj star))
                ⋯))))
        x_1 =
      (CommaMorphism.left (𝟙 (mkCommaObject x))).app x_1
h₂ :
  CommaMorphism.right
      (mkCommaMorphism
        (Iso.hom
          (NatIso.ofComponents
            (fun (X : WithTerminal C) ↦
              match (motive :=
                (X : WithTerminal C) →
                  x.obj X ≅
                    match (motive := WithTerminal C → D) X with
                    | of x_1 => x.obj (Functor.obj.{v, v, u, u} incl x_1)
                    | star => x.obj star)
                X with
              | of x_1 => Iso.app (Iso.refl (incl ⋙ x)) x_1
              | star => Iso.refl (x.obj star))
            ⋯))) =
    CommaMorphism.right (𝟙 (mkCommaObject x))
⊢ mkCommaMorphism
      (Iso.hom
        (NatIso.ofComponents
          (fun (X : WithTerminal C) ↦
            match (motive :=
              (X : WithTerminal C) →
                x.obj X ≅
                  match (motive := WithTerminal C → D) X with
                  | of x_1 => x.obj (Functor.obj.{v, v, u, u} incl x_1)
                  | star => x.obj star)
              X with
            | of x_1 => Iso.app (Iso.refl (incl ⋙ x)) x_1
            | star => Iso.refl (x.obj star))
          ⋯)) =
    𝟙 (mkCommaObject x)

Tactic:
ext
-- 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
x : Functor.{v, v_1, u, u_1} (WithTerminal C) D
x_1 : C
⊢ NatTrans.app
      (CommaMorphism.left
        (mkCommaMorphism
          (Iso.hom
            (NatIso.ofComponents
              (fun (X : WithTerminal C) ↦
                match (motive :=
                  (X : WithTerminal C) →
                    x.obj X ≅
                      match (motive := WithTerminal C → D) X with
                      | of x_2 => x.obj (Functor.obj.{v, v, u, u} incl x_2)
                      | star => x.obj star)
                  X with
                | of x_2 => Iso.app (Iso.refl (incl ⋙ x)) x_2
                | star => Iso.refl (x.obj star))
              ⋯))))
      x_1 =
    (CommaMorphism.left (𝟙 (mkCommaObject x))).app 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
x : Functor.{v, v_1, u, u_1} (WithTerminal C) D
⊢ CommaMorphism.right
      (mkCommaMorphism
        (Iso.hom
          (NatIso.ofComponents
            (fun (X : WithTerminal C) ↦
              match (motive :=
                (X : WithTerminal C) →
                  x.obj X ≅
                    match (motive := WithTerminal C → D) X with
                    | of x_1 => x.obj (Functor.obj.{v, v, u, u} incl x_1)
                    | star => x.obj star)
                X with
              | of x_1 => Iso.app (Iso.refl (incl ⋙ x)) x_1
              | star => Iso.refl (x.obj star))
            ⋯))) =
    CommaMorphism.right (𝟙 (mkCommaObject x))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x x_1 : WithTerminal (Discrete J)
allEq : ∀ (a b : x ⟶ x_1), a = b
⊢ Subsingleton.{u_1 + 1} (x ⟶ x_1)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x x_1 : WithTerminal (Discrete J)
a b : x ⟶ x_1
allEq :
  ∀ (x x_2 : Discrete J) (a b : PLift (x.as = x_2.as)),
    { down := a : ULift.{u_1, 0} (PLift (x.as = x_2.as)) } = { down := b }
allEq₁ : ∀ (x : Discrete J), PUnit.unit = PUnit.unit
allEq₂ : PUnit.unit = PUnit.unit
⊢ a = b

Tactic:
casesm* WithTerminal _, (_ : WithTerminal _) ⟶ (_ : WithTerminal _)

Premises used: CategoryTheory.WithTerminal
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x x_1 : Discrete J
a b : PLift (x.as = x_1.as)
⊢ { down := a : ULift.{u_1, 0} (PLift (x.as = x_1.as)) } = { down := b }

Tactic:
congr_arg (ULift.up ∘ PLift.up) rfl

Premises used: Function.comp, CategoryTheory.WithTerminal.Hom, congr_arg, PLift.up, ULift.up, rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x x_1 : Discrete J
a b : PLift (x.as = x_1.as)
⊢ { down := a : ULift.{u_1, 0} (PLift (x.as = x_1.as)) } = { down := b }

Tactic:
exact congr_arg (ULift.up ∘ PLift.up) rfl

Premises used: Function.comp, congr_arg, PLift.up, ULift.up, rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x : Discrete J
⊢ PUnit.unit = PUnit.unit

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
⊢ PUnit.unit = PUnit.unit

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x : WidePullbackShape J
none :
  Eq.{u_1 + 1} (α := WidePullbackShape J)
    ((fun (x : WithTerminal (Discrete J)) ↦
        (match (motive := WithTerminal (Discrete J) → WidePullbackShape J) x with
          | of x => Option.some x.as
          | star => Option.none :
          WidePullbackShape J))
      ((fun (x : WidePullbackShape J) ↦
          (match (motive := WidePullbackShape J → WithTerminal (Discrete J)) x with
            | Option.some x => of { as := x }
            | Option.none => star :
            WithTerminal (Discrete J)))
        Option.none))
    Option.none
some :
  ∀ (val : J),
    (fun (x : WithTerminal (Discrete J)) ↦
          (match (motive := WithTerminal (Discrete J) → WidePullbackShape J) x with
            | of x => Option.some x.as
            | star => Option.none :
            WidePullbackShape J))
        ((fun (x : WidePullbackShape J) ↦
            (match (motive := WidePullbackShape J → WithTerminal (Discrete J)) x with
              | Option.some x => of { as := x }
              | Option.none => star :
              WithTerminal (Discrete J)))
          (Option.some val)) =
      Option.some val
⊢ (fun (x : WithTerminal (Discrete J)) ↦
        (match (motive := WithTerminal (Discrete J) → WidePullbackShape J) x with
          | of x => Option.some x.as
          | star => Option.none :
          WidePullbackShape J))
      ((fun (x : WidePullbackShape J) ↦
          (match (motive := WidePullbackShape J → WithTerminal (Discrete J)) x with
            | Option.some x => of { as := x }
            | Option.none => star :
            WithTerminal (Discrete J)))
        x) =
    x

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

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

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

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

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

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x_1 y_1 : WidePullbackShape J
x y : J
f :
  Quiver.Hom (V := WithTerminal (Discrete J))
    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some x) :
      WithTerminal (Discrete J))
    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some y) :
      WithTerminal (Discrete J))
⊢ x = y

Tactic:
have eq : x = y := PLift.down (ULift.down (down f))
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x_1 y_1 : WidePullbackShape J
x y : J
f :
  Quiver.Hom (V := WithTerminal (Discrete J))
    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some x) :
      WithTerminal (Discrete J))
    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some y) :
      WithTerminal (Discrete J))
eq : x = y
rw : WidePullbackShape.Hom (some y) (some y) = (some y ⟶ some y)
⊢ WidePullbackShape.Hom (some y) (some y) = (some x ⟶ some y)

Tactic:
rw [eq]
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x_1 y_1 : WidePullbackShape J
x y : J
f :
  Quiver.Hom (V := WithTerminal (Discrete J))
    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some x) :
      WithTerminal (Discrete J))
    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some y) :
      WithTerminal (Discrete J))
eq : x = y
⊢ WidePullbackShape.Hom (some y) (some y) = (some y ⟶ some y)

Tactic:
rfl
-- 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))
⊢ none ⟶ some y

Tactic:
cases f