awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
X : (↑(prelaxfunctor.obj a) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α := (prelaxfunctor.map (𝟙 a ≫ f)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map f).toFunctor.obj (of a_1))
      ((prelaxfunctor.map₂ (Bicategory.leftUnitor f).hom).toNatTrans.app (of a_1))
      (((Cat.Hom.isoMk (mapComp (Cat.Hom.toFunctor (𝟙 a)) f.toFunctor)).hom ≫
              Bicategory.whiskerRight (Iso.hom (Cat.Hom.isoMk (mapId (↑a : Type u_1)))) (prelaxfunctor.map f) ≫
                (Bicategory.leftUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
        (of a_1))
h₁ :
  Eq (α := (prelaxfunctor.map (𝟙 a ≫ f)).toFunctor.obj star ⟶ (prelaxfunctor.map f).toFunctor.obj star)
    ((prelaxfunctor.map₂ (Bicategory.leftUnitor f).hom).toNatTrans.app star)
    (((Cat.Hom.isoMk (mapComp (Cat.Hom.toFunctor (𝟙 a)) f.toFunctor)).hom ≫
            Bicategory.whiskerRight (Iso.hom (Cat.Hom.isoMk (mapId (↑a : Type u_1)))) (prelaxfunctor.map f) ≫
              (Bicategory.leftUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
      star)
⊢ (prelaxfunctor.map₂ (Bicategory.leftUnitor f).hom).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp (Cat.Hom.toFunctor (𝟙 a)) f.toFunctor)).hom ≫
            Bicategory.whiskerRight (Iso.hom (Cat.Hom.isoMk (mapId (↑a : Type u_1)))) (prelaxfunctor.map f) ≫
              (Bicategory.leftUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
      X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
a_1 : (↑a : Type u_1)
⊢ Eq (α := (prelaxfunctor.map (𝟙 a ≫ f)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map f).toFunctor.obj (of a_1))
    ((prelaxfunctor.map₂ (Bicategory.leftUnitor f).hom).toNatTrans.app (of a_1))
    (((Cat.Hom.isoMk (mapComp (Cat.Hom.toFunctor (𝟙 a)) f.toFunctor)).hom ≫
            Bicategory.whiskerRight (Iso.hom (Cat.Hom.isoMk (mapId (↑a : Type u_1)))) (prelaxfunctor.map f) ≫
              (Bicategory.leftUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
      (of a_1))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
⊢ Eq (α := (prelaxfunctor.map (𝟙 a ≫ f)).toFunctor.obj star ⟶ (prelaxfunctor.map f).toFunctor.obj star)
    ((prelaxfunctor.map₂ (Bicategory.leftUnitor f).hom).toNatTrans.app star)
    (((Cat.Hom.isoMk (mapComp (Cat.Hom.toFunctor (𝟙 a)) f.toFunctor)).hom ≫
            Bicategory.whiskerRight (Iso.hom (Cat.Hom.isoMk (mapId (↑a : Type u_1)))) (prelaxfunctor.map f) ≫
              (Bicategory.leftUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
      star)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
h :
  ∀ (X : (↑(prelaxfunctor.obj a) : Type u_1)),
    (prelaxfunctor.map₂ (Bicategory.rightUnitor f).hom).toNatTrans.app X =
      ((Cat.Hom.isoMk (mapComp f.toFunctor (Cat.Hom.toFunctor (𝟙 b)))).hom ≫
              Bicategory.whiskerLeft (prelaxfunctor.map f) (Iso.hom (Cat.Hom.isoMk (mapId (↑b : Type u_1)))) ≫
                (Bicategory.rightUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
        X
⊢ prelaxfunctor.map₂ (Bicategory.rightUnitor f).hom =
    (Cat.Hom.isoMk (mapComp f.toFunctor (Cat.Hom.toFunctor (𝟙 b)))).hom ≫
      Bicategory.whiskerLeft (prelaxfunctor.map f) (Iso.hom (Cat.Hom.isoMk (mapId (↑b : Type u_1)))) ≫
        (Bicategory.rightUnitor (prelaxfunctor.map f)).hom

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
X : (↑(prelaxfunctor.obj a) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α := (prelaxfunctor.map (f ≫ 𝟙 b)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map f).toFunctor.obj (of a_1))
      ((prelaxfunctor.map₂ (Bicategory.rightUnitor f).hom).toNatTrans.app (of a_1))
      (((Cat.Hom.isoMk (mapComp f.toFunctor (Cat.Hom.toFunctor (𝟙 b)))).hom ≫
              Bicategory.whiskerLeft (prelaxfunctor.map f) (Iso.hom (Cat.Hom.isoMk (mapId (↑b : Type u_1)))) ≫
                (Bicategory.rightUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
        (of a_1))
h₁ :
  Eq (α := (prelaxfunctor.map (f ≫ 𝟙 b)).toFunctor.obj star ⟶ (prelaxfunctor.map f).toFunctor.obj star)
    ((prelaxfunctor.map₂ (Bicategory.rightUnitor f).hom).toNatTrans.app star)
    (((Cat.Hom.isoMk (mapComp f.toFunctor (Cat.Hom.toFunctor (𝟙 b)))).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (Iso.hom (Cat.Hom.isoMk (mapId (↑b : Type u_1)))) ≫
              (Bicategory.rightUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
      star)
⊢ (prelaxfunctor.map₂ (Bicategory.rightUnitor f).hom).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp f.toFunctor (Cat.Hom.toFunctor (𝟙 b)))).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (Iso.hom (Cat.Hom.isoMk (mapId (↑b : Type u_1)))) ≫
              (Bicategory.rightUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
      X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
a_1 : (↑a : Type u_1)
⊢ Eq (α := (prelaxfunctor.map (f ≫ 𝟙 b)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map f).toFunctor.obj (of a_1))
    ((prelaxfunctor.map₂ (Bicategory.rightUnitor f).hom).toNatTrans.app (of a_1))
    (((Cat.Hom.isoMk (mapComp f.toFunctor (Cat.Hom.toFunctor (𝟙 b)))).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (Iso.hom (Cat.Hom.isoMk (mapId (↑b : Type u_1)))) ≫
              (Bicategory.rightUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
      (of a_1))

Tactic:
simpa using (refl _)

Premises used: refl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
⊢ Eq (α := (prelaxfunctor.map (f ≫ 𝟙 b)).toFunctor.obj star ⟶ (prelaxfunctor.map f).toFunctor.obj star)
    ((prelaxfunctor.map₂ (Bicategory.rightUnitor f).hom).toNatTrans.app star)
    (((Cat.Hom.isoMk (mapComp f.toFunctor (Cat.Hom.toFunctor (𝟙 b)))).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (Iso.hom (Cat.Hom.isoMk (mapId (↑b : Type u_1)))) ≫
              (Bicategory.rightUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
      star)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Limits.HasTerminal.{v, u} (WithTerminal C)

Tactic:
Limits.hasTerminal_of_unique star

Premises used: CategoryTheory.Limits.hasTerminal_of_unique, CategoryTheory.WithTerminal.star
-- 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
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
x : C
simp :
  (match (motive :=
      (X Y : WithTerminal C) →
        (X ⟶ Y) →
          Quiver.Hom.{v_1, u_1} (V := D)
            (match (motive := WithTerminal C → D) X with
              | of x => F.obj x
              | star => Z :
              D)
            (match (motive := WithTerminal C → D) Y with
              | of x => F.obj x
              | star => Z :
              D))
      Functor.obj.{v, v, u, u} incl x, star, Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x) with
    | of a, of a_1, f => F.map (down f)
    | of x, star, x_1 => M x
    | star, star, x => 𝟙 Z) =
    M x
⊢ (lift F M hM).map (Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x)) ≫ (liftStar F M hM).hom =
    (inclLift F M hM).hom.app x ≫ M x

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
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
x : C
⊢ (match (motive :=
      (X Y : WithTerminal C) →
        (X ⟶ Y) →
          Quiver.Hom.{v_1, u_1} (V := D)
            (match (motive := WithTerminal C → D) X with
              | of x => F.obj x
              | star => Z :
              D)
            (match (motive := WithTerminal C → D) Y with
              | of x => F.obj x
              | star => Z :
              D))
      Functor.obj.{v, v, u, u} incl x, star, Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x) with
    | of a, of a_1, f => F.map (down f)
    | of x, star, x_1 => M x
    | star, star, x => 𝟙 Z) =
    M 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
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : Functor.{v, v_1, u, u_1} (WithTerminal C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x)) ≫ hG.hom = h.hom.app x ≫ M x
X Y : C
f : of X ⟶ of Y
⊢ G.map f ≫
      Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          (of Y)) =
    Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          (of X)) ≫
      (lift F M hM).map f

Tactic:
apply h.hom.naturality

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- 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
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : Functor.{v, v_1, u, u_1} (WithTerminal C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x)) ≫ hG.hom = h.hom.app x ≫ M x
X : C
f : WithTerminal.of X ⟶ star
of :
  Eq (α := G.obj (WithTerminal.of X) ⟶ (lift F M hM).obj star)
    (CategoryStruct.comp (Y := G.obj star) (G.map PUnit.unit)
      (Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | WithTerminal.of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          star)))
    (CategoryStruct.comp (Y := (lift F M hM).obj (WithTerminal.of X))
      (Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | WithTerminal.of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          (WithTerminal.of X)))
      ((lift F M hM).map PUnit.unit))
⊢ G.map f ≫
      Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | WithTerminal.of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          star) =
    Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | WithTerminal.of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          (WithTerminal.of X)) ≫
      (lift F M hM).map f

Tactic:
cases f
-- 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
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : Functor.{v, v_1, u, u_1} (WithTerminal C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x)) ≫ hG.hom = h.hom.app x ≫ M x
X : C
⊢ Eq (α := G.obj (of X) ⟶ (lift F M hM).obj star)
    (CategoryStruct.comp (Y := G.obj star) (G.map PUnit.unit)
      (Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          star)))
    (CategoryStruct.comp (Y := (lift F M hM).obj (of X))
      (Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          (of X)))
      ((lift F M hM).map PUnit.unit))

Tactic:
hh _

Premises used: CategoryTheory.Limits.IsTerminal.from
-- 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
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : Functor.{v, v_1, u, u_1} (WithTerminal C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x)) ≫ hG.hom = h.hom.app x ≫ M x
X : C
⊢ Eq (α := G.obj (of X) ⟶ (lift F M hM).obj star)
    (CategoryStruct.comp (Y := G.obj star) (G.map PUnit.unit)
      (Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          star)))
    (CategoryStruct.comp (Y := (lift F M hM).obj (of X))
      (Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          (of X)))
      ((lift F M hM).map PUnit.unit))

Tactic:
exact hh _
-- 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
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : Functor.{v, v_1, u, u_1} (WithTerminal C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x)) ≫ hG.hom = h.hom.app x ≫ M x
Y : C
f : star ⟶ of Y
⊢ G.map f ≫
      Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          (of Y)) =
    Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          star) ≫
      (lift F M hM).map f

Tactic:
cases f
-- 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
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : Functor.{v, v_1, u, u_1} (WithTerminal C) D
h : incl ⋙ G ≅ F
hG : G.obj WithTerminal.star ≅ Z
hh :
  ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x)) ≫ hG.hom = h.hom.app x ≫ M x
f : Quiver.Hom.{v, u} (V := WithTerminal C) WithTerminal.star WithTerminal.star
star :
  Eq (α := G.obj WithTerminal.star ⟶ (lift F M hM).obj WithTerminal.star)
    (CategoryStruct.comp (Y := G.obj WithTerminal.star) (G.map PUnit.unit)
      (Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | WithTerminal.star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          WithTerminal.star)))
    (CategoryStruct.comp (Y := (lift F M hM).obj WithTerminal.star)
      (Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | WithTerminal.star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          WithTerminal.star))
      ((lift F M hM).map PUnit.unit))
⊢ G.map f ≫
      Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | WithTerminal.star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          WithTerminal.star) =
    Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | WithTerminal.star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          WithTerminal.star) ≫
      (lift F M hM).map f

Tactic:
cases f
-- 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
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : Functor.{v, v_1, u, u_1} (WithTerminal C) D
h : incl ⋙ G ≅ F
hG : G.obj WithTerminal.star ≅ Z
hh :
  ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x)) ≫ hG.hom = h.hom.app x ≫ M x
star : G.map (𝟙 WithTerminal.star) ≫ hG.hom = hG.hom ≫ 𝟙 Z
⊢ Eq (α := G.obj WithTerminal.star ⟶ (lift F M hM).obj WithTerminal.star)
    (CategoryStruct.comp (Y := G.obj WithTerminal.star) (G.map PUnit.unit)
      (Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | WithTerminal.star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          WithTerminal.star)))
    (CategoryStruct.comp (Y := (lift F M hM).obj WithTerminal.star)
      (Iso.hom
        ((fun (X : WithTerminal C) ↦
            (match (motive := (X : WithTerminal C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | WithTerminal.star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          WithTerminal.star))
      ((lift F M hM).map PUnit.unit))

Tactic:
change G.map (𝟙 _) ≫ hG.hom = hG.hom ≫ 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, CategoryTheory.Iso.hom
-- 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
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : Functor.{v, v_1, u, u_1} (WithTerminal C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (Functor.obj.{v, v, u, u} incl x)) ≫ hG.hom = h.hom.app x ≫ M x
⊢ G.map (𝟙 star) ≫ hG.hom = hG.hom ≫ 𝟙 Z

Tactic:
simp
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : WithTerminal C
f : star ⟶ X
⊢ IsIso f

Tactic:
match X with
  | of _X => f.elim
  | star => ⟨f, rfl, rfl⟩

Premises used: _private.0.CategoryTheory.WithTerminal.isIso_of_from_star.match_1, CategoryTheory.IsIso, PEmpty.elim, And.intro, Exists.intro, CategoryTheory.IsIso.mk, 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
F : Functor.{v, v_1, u, u_1} (WithTerminal C) D
x y : C
f : x ⟶ y
dsimp :
  F.map (Functor.map incl f) ≫ F.map (Limits.IsTerminal.from starTerminal (of y)) =
    F.map (Limits.IsTerminal.from starTerminal (of x)) ≫ 𝟙 (F.obj star)
⊢ (Functor.obj (𝟭 (Functor.{v, v_1, u, u_1} C D)) (incl ⋙ F)).map f ≫
      F.map (Limits.IsTerminal.from starTerminal (of y)) =
    F.map (Limits.IsTerminal.from starTerminal (of x)) ≫ Functor.map (Functor.obj (Functor.const C) (F.obj star)) f

Tactic:
dsimp
-- 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)) ≫ 𝟙 (F.obj star)

Tactic:
rw [Category.comp_id, ← F.map_comp]

Premises used: CategoryTheory.Category.comp_id, 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 y : C
f : x ⟶ y
⊢ F.map (Functor.map incl f ≫ Limits.IsTerminal.from starTerminal (of y)) =
    F.map (Limits.IsTerminal.from starTerminal (of x))

Tactic:
congr 1
-- 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 : Comma (A := Functor.{v, v_1, u, u_1} C D) (𝟭 (Functor.{v, v_1, u, u_1} C D)) (Functor.const C)
x y : C
f : x ⟶ y
⊢ Eq (α := c.left.obj x ⟶ c.right) (c.left.map f ≫ (fun (x : C) ↦ c.hom.app x) y) ((fun (x : C) ↦ c.hom.app x) x)

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
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_1 : x ⟶ y
a a_1 : C
f : of a ⟶ of a_1
⊢ Eq (α := (ofCommaObject c).obj (of a) ⟶ (ofCommaObject c').obj (of a_1))
    ((ofCommaObject c).map f ≫
      match (motive := (x : WithTerminal C) → (ofCommaObject c).obj x ⟶ (ofCommaObject c').obj x) of a_1 with
      | of x => φ.left.app x
      | star => φ.right)
    ((match (motive := (x : WithTerminal C) → (ofCommaObject c).obj x ⟶ (ofCommaObject c').obj x) of a with
      | of x => φ.left.app x
      | star => φ.right) ≫
      (ofCommaObject c').map f)

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
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
a : C
x_1 : of a ⟶ star
simp : c.hom.app a ≫ φ.right = φ.left.app a ≫ c'.hom.app a
⊢ Eq (α := (ofCommaObject c).obj (of a) ⟶ (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) of a 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
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
a : C
x_1 : of a ⟶ star
⊢ c.hom.app a ≫ φ.right = φ.left.app a ≫ c'.hom.app a

Tactic:
simpa [-CommaMorphism.w] using (congrArg (fun f ↦ f.app a) φ.w).symm

Premises used: congrArg, CategoryTheory.CommaMorphism.w, Eq.symm