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
x y : Functor.{v, v_1, u, u_1} (WithInitial C) D
f : x ⟶ y
⊢ Eq (α :=
    (Functor.obj (𝟭 (Functor.{v, v_1, u, u_1} (WithInitial C) D)) x).obj star ⟶
      (Functor.obj
            ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithInitial C) D} ↦ mkCommaMorphism,
                map_id := ⋯, map_comp := ⋯ :
                Functor.{v, v_1, u, u_1} (WithInitial C) D ⥤
                  Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                    (𝟭 (Functor.{v, v_1, u, u_1} C D)) } ⋙
              { obj := ofCommaObject,
                map :=
                  fun
                    {X Y :
                      Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                        (𝟭 (Functor.{v, v_1, u, u_1} C D))} ↦
                  ofCommaMorphism,
                map_id := ⋯, map_comp := ⋯ :
                Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                    (𝟭 (Functor.{v, v_1, u, u_1} C D)) ⥤
                  Functor.{v, v_1, u, u_1} (WithInitial C) D })
            y).obj
        star)
    (NatTrans.app
      (Functor.map (𝟭 (Functor.{v, v_1, u, u_1} (WithInitial C) D)) f ≫
        Iso.hom
          ((fun (F : Functor.{v, v_1, u, u_1} (WithInitial C) D) ↦
              (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsInitial.to starInitial (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.IsInitial.to starInitial (of x))) ⋯))
            y))
      star)
    (NatTrans.app
      (Iso.hom
          ((fun (F : Functor.{v, v_1, u, u_1} (WithInitial C) D) ↦
              (liftUnique (incl ⋙ F) (fun (x : C) ↦ F.map (Limits.IsInitial.to starInitial (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.IsInitial.to starInitial (of x))) ⋯))
            x) ≫
        Functor.map
          ({ obj := mkCommaObject, map := fun {X Y : Functor.{v, v_1, u, u_1} (WithInitial C) D} ↦ mkCommaMorphism,
              map_id := ⋯, map_comp := ⋯ :
              Functor.{v, v_1, u, u_1} (WithInitial C) D ⥤
                Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                  (𝟭 (Functor.{v, v_1, u, u_1} C D)) } ⋙
            { obj := ofCommaObject,
              map :=
                fun
                  {X Y :
                    Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C)
                      (𝟭 (Functor.{v, v_1, u, u_1} C D))} ↦
                ofCommaMorphism,
              map_id := ⋯, map_comp := ⋯ :
              Comma (A := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C) (𝟭 (Functor.{v, v_1, u, u_1} C D)) ⥤
                Functor.{v, v_1, u, u_1} (WithInitial C) D })
          f)
      star)

Tactic:
simp [incl]

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

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a : Cᵒᵖ
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
      (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star :
        (WithTerminal C)ᵒᵖ)
      (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star :
        (WithTerminal C)ᵒᵖ))
    (match (motive :=
        (x y : WithInitial Cᵒᵖ) →
          (x ⟶ y) →
            Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
              (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) x with
                | WithInitial.of x => op (of (unop x))
                | WithInitial.star => op star :
                (WithTerminal C)ᵒᵖ)
              (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) y with
                | WithInitial.of x => op (of (unop x))
                | WithInitial.star => op star :
                (WithTerminal C)ᵒᵖ))
        WithInitial.of a, WithInitial.of a, 𝟙 (WithInitial.of a) with
      | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
      | WithInitial.star, WithInitial.of (op unop), x =>
        op
          (Limits.IsTerminal.from starTerminal
            (Opposite.unop
              (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of (op unop) with
              | WithInitial.of x => op (of (Opposite.unop x))
              | WithInitial.star => op star)))
      | WithInitial.star, WithInitial.star, x =>
        𝟙
          (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
          | WithInitial.of x => op (of (unop x))
          | WithInitial.star => op star) :
      Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
          | WithInitial.of x => op (of (unop x))
          | WithInitial.star => op star :
          (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
          | WithInitial.of x => op (of (unop x))
          | WithInitial.star => op star :
          (WithTerminal C)ᵒᵖ))
    (𝟙
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star) :
      Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
          | WithInitial.of x => op (of (unop x))
          | WithInitial.star => op star :
          (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of a with
          | WithInitial.of x => op (of (unop x))
          | WithInitial.star => op star :
          (WithTerminal C)ᵒᵖ))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
      (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star :
        (WithTerminal C)ᵒᵖ)
      (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star :
        (WithTerminal C)ᵒᵖ))
    (match (motive :=
        (x y : WithInitial Cᵒᵖ) →
          (x ⟶ y) →
            Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
              (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) x with
                | WithInitial.of x => op (of (unop x))
                | WithInitial.star => op star :
                (WithTerminal C)ᵒᵖ)
              (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) y with
                | WithInitial.of x => op (of (unop x))
                | WithInitial.star => op star :
                (WithTerminal C)ᵒᵖ))
        WithInitial.star, WithInitial.star, 𝟙 WithInitial.star with
      | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
      | WithInitial.star, WithInitial.of (op unop), x =>
        op
          (Limits.IsTerminal.from starTerminal
            (Opposite.unop
              (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.of (op unop) with
              | WithInitial.of x => op (of (Opposite.unop x))
              | WithInitial.star => op star)))
      | WithInitial.star, WithInitial.star, x =>
        𝟙
          (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
          | WithInitial.of x => op (of (unop x))
          | WithInitial.star => op star) :
      Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
          | WithInitial.of x => op (of (unop x))
          | WithInitial.star => op star :
          (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
          | WithInitial.of x => op (of (unop x))
          | WithInitial.star => op star :
          (WithTerminal C)ᵒᵖ))
    (𝟙
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star) :
      Quiver.Hom (V := (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
          | WithInitial.of x => op (of (unop x))
          | WithInitial.star => op star :
          (WithTerminal C)ᵒᵖ)
        (match (motive := WithInitial Cᵒᵖ → (WithTerminal C)ᵒᵖ) WithInitial.star with
          | WithInitial.of x => op (of (unop x))
          | WithInitial.star => op star :
          (WithTerminal C)ᵒᵖ))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x_1 y_1 : (WithTerminal C)ᵒᵖ
f_1 : unop y_1 ⟶ unop x_1
x y : C
f : unop (op (of y)) ⟶ unop (op (of x))
x_2 : op (of x) ⟶ op (of y)
⊢ op f = WithInitial.down (down f).op

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x_1 : (WithTerminal C)ᵒᵖ
x_2 : WithTerminal C
x : C
⊢ Eq.{v + 1} (α := WithInitial.of (op x) ⟶ WithInitial.of (op x)) (Quiver.Hom.op (down (unop (𝟙 (op (of x))))))
    (𝟙 (WithInitial.of (op x)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a : Cᵒᵖ
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := (WithInitial C)ᵒᵖ)
      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star :
        (WithInitial C)ᵒᵖ)
      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star :
        (WithInitial C)ᵒᵖ))
    (match (motive :=
        (x y : WithTerminal Cᵒᵖ) →
          (x ⟶ y) →
            Quiver.Hom (V := (WithInitial C)ᵒᵖ)
              (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                | WithTerminal.of x => op (of (unop x))
                | WithTerminal.star => op star :
                (WithInitial C)ᵒᵖ)
              (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
                | WithTerminal.of x => op (of (unop x))
                | WithTerminal.star => op star :
                (WithInitial C)ᵒᵖ))
        WithTerminal.of a, WithTerminal.of a, 𝟙 (WithTerminal.of a) with
      | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
      | WithTerminal.of (op unop), WithTerminal.star, x =>
        op
          (Limits.IsInitial.to starInitial
            (Opposite.unop
              (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of (op unop) with
              | WithTerminal.of x => op (of (Opposite.unop x))
              | WithTerminal.star => op star)))
      | WithTerminal.star, WithTerminal.star, x =>
        𝟙
          (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
          | WithTerminal.of x => op (of (unop x))
          | WithTerminal.star => op star) :
      Quiver.Hom (V := (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
          | WithTerminal.of x => op (of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
          | WithTerminal.of x => op (of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ))
    (𝟙
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star) :
      Quiver.Hom (V := (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
          | WithTerminal.of x => op (of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of a with
          | WithTerminal.of x => op (of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := (WithInitial C)ᵒᵖ)
      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star :
        (WithInitial C)ᵒᵖ)
      (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star :
        (WithInitial C)ᵒᵖ))
    (match (motive :=
        (x y : WithTerminal Cᵒᵖ) →
          (x ⟶ y) →
            Quiver.Hom (V := (WithInitial C)ᵒᵖ)
              (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) x with
                | WithTerminal.of x => op (of (unop x))
                | WithTerminal.star => op star :
                (WithInitial C)ᵒᵖ)
              (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) y with
                | WithTerminal.of x => op (of (unop x))
                | WithTerminal.star => op star :
                (WithInitial C)ᵒᵖ))
        WithTerminal.star, WithTerminal.star, 𝟙 WithTerminal.star with
      | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
      | WithTerminal.of (op unop), WithTerminal.star, x =>
        op
          (Limits.IsInitial.to starInitial
            (Opposite.unop
              (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.of (op unop) with
              | WithTerminal.of x => op (of (Opposite.unop x))
              | WithTerminal.star => op star)))
      | WithTerminal.star, WithTerminal.star, x =>
        𝟙
          (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
          | WithTerminal.of x => op (of (unop x))
          | WithTerminal.star => op star) :
      Quiver.Hom (V := (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
          | WithTerminal.of x => op (of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
          | WithTerminal.of x => op (of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ))
    (𝟙
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star) :
      Quiver.Hom (V := (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
          | WithTerminal.of x => op (of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ)
        (match (motive := WithTerminal Cᵒᵖ → (WithInitial C)ᵒᵖ) WithTerminal.star with
          | WithTerminal.of x => op (of (unop x))
          | WithTerminal.star => op star :
          (WithInitial C)ᵒᵖ))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x_1 y_1 : (WithInitial C)ᵒᵖ
f_1 : x_1 ⟶ y_1
x y : C
f : op (of x) ⟶ op (of y)
⊢ f = down (WithTerminal.down (unop f)).op

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x_1 : (WithInitial C)ᵒᵖ
x_2 : WithInitial C
x : C
⊢ Eq.{v + 1} (α := WithTerminal.of (op x) ⟶ WithTerminal.of (op x))
    (Quiver.Hom.op (WithTerminal.down (unop (𝟙 (op (of x)))))) (𝟙 (WithTerminal.of (op x)))

Tactic:
rfl
-- 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 t : Cone K
x : Quiver.Hom.{w', w} (V := WithTerminal J) star star
⊢ Eq.{v₁ + 1} (α :=
    Functor.obj.{w', v₁, w, u₁} (C := WithTerminal J) (Functor.obj (Functor.const (WithTerminal J)) t.pt.left) star ⟶
      (Functor.obj liftFromOver K).obj star)
    (Functor.map (Functor.obj (Functor.const (WithTerminal J)) t.pt.left) x ≫
      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)
        star with
      | of a => Over.Hom.left (t.π.app a)
      | star => t.pt.hom)
    ((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)
        star with
      | of a => Over.Hom.left (t.π.app a)
      | star => t.pt.hom) ≫
      (Functor.obj liftFromOver K).map 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 ⥤ Over.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t_1 t : Cone K
a : J
x : of a ⟶ star
⊢ Eq.{v₁ + 1} (α :=
    Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithTerminal J)) t.pt.left) (of a) ⟶
      (Functor.obj liftFromOver K).obj star)
    (Functor.map (Functor.obj (Functor.const (WithTerminal J)) t.pt.left) x ≫
      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)
        star with
      | of a => Over.Hom.left (t.π.app a)
      | star => t.pt.hom)
    ((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)
        of a with
      | of a => Over.Hom.left (t.π.app a)
      | star => t.pt.hom) ≫
      (Functor.obj liftFromOver K).map 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 ⥤ Over.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t_1 t : Cone K
a b : J
f : of a ⟶ of b
⊢ Eq.{v₁ + 1} (α :=
    Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const (WithTerminal J)) t.pt.left) (of a) ⟶
      (Functor.obj liftFromOver K).obj (of b))
    (Functor.map (Functor.obj (Functor.const (WithTerminal J)) t.pt.left) f ≫
      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)
        of b with
      | of a => Over.Hom.left (t.π.app a)
      | star => t.pt.hom)
    ((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)
        of a with
      | of a => Over.Hom.left (t.π.app a)
      | star => t.pt.hom) ≫
      (Functor.obj liftFromOver K).map f)

Tactic:
simp [← Comma.comp_left]

Premises used: CategoryTheory.Comma.comp_left