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

Tactic:
change G.map _ ≫ h.hom.app _ = hG.hom ≫ _

Premises used: CategoryTheory.Functor.map, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- 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) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : Functor.{v, v_1, u, u_1} (WithInitial C) D
h : incl ⋙ G ≅ F
hG : G.obj WithInitial.star ≅ Z
hh :
  ∀ (x : C),
    hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) = M x ≫ h.symm.hom.app x
Y : C
star : hG.hom ≫ (lift F M hM).map PUnit.unit = G.map PUnit.unit ≫ h.hom.app Y
⊢ G.map PUnit.unit ≫ h.hom.app Y = hG.hom ≫ (lift F M hM).map PUnit.unit

Tactic:
symm
-- 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) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : Functor.{v, v_1, u, u_1} (WithInitial C) D
h : incl ⋙ G ≅ F
hG : G.obj WithInitial.star ≅ Z
hh :
  ∀ (x : C),
    hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) = M x ≫ h.symm.hom.app x
Y : C
star : (lift F M hM).map PUnit.unit = (M Y ≫ h.symm.hom.app Y) ≫ h.hom.app Y
⊢ hG.hom ≫ (lift F M hM).map PUnit.unit = G.map PUnit.unit ≫ h.hom.app Y

Tactic:
erw [← Iso.eq_inv_comp, ← Category.assoc, hh]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_inv_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
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : Functor.{v, v_1, u, u_1} (WithInitial C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C),
    hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) = M x ≫ h.symm.hom.app x
Y : C
⊢ (lift F M hM).map PUnit.unit = (M Y ≫ h.symm.hom.app Y) ≫ h.hom.app Y

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

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

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

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

Premises used: CategoryTheory.Functor.map_comp, 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} (WithInitial C) D
x y : C
f : x ⟶ y
⊢ F.map (Limits.IsInitial.to starInitial (of y)) = F.map (Limits.IsInitial.to starInitial (of x) ≫ Functor.map incl f)

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

Tactic:
simpa using (c.hom.naturality f).symm

Premises used: CategoryTheory.Comma.hom, CategoryTheory.NatTrans.naturality, Eq.symm
-- 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 := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C) (𝟭 (Functor.{v, v_1, u, u_1} C D))
φ : c ⟶ c'
x y : WithInitial 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 : WithInitial C) → (ofCommaObject c).obj x ⟶ (ofCommaObject c').obj x) of a_1 with
      | of x => φ.right.app x
      | star => φ.left)
    ((match (motive := (x : WithInitial C) → (ofCommaObject c).obj x ⟶ (ofCommaObject c').obj x) of a with
      | of x => φ.right.app x
      | star => φ.left) ≫
      (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 := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C) (𝟭 (Functor.{v, v_1, u, u_1} C D))
φ : c ⟶ c'
x y : WithInitial C
f : x ⟶ y
a : C
x_1 : star ⟶ of a
⊢ Eq (α := (ofCommaObject c).obj star ⟶ (ofCommaObject c').obj (of a))
    ((ofCommaObject c).map x_1 ≫
      match (motive := (x : WithInitial C) → (ofCommaObject c).obj x ⟶ (ofCommaObject c').obj x) of a with
      | of x => φ.right.app x
      | star => φ.left)
    ((match (motive := (x : WithInitial C) → (ofCommaObject c).obj x ⟶ (ofCommaObject c').obj x) star with
      | of x => φ.right.app x
      | star => φ.left) ≫
      (ofCommaObject c').map x_1)

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

Premises used: congrArg, CategoryTheory.CommaMorphism.w, Eq.symm
-- 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 := D) (B := Functor.{v, v_1, u, u_1} C D) (Functor.const C) (𝟭 (Functor.{v, v_1, u, u_1} C D))
φ : c ⟶ c'
x y : WithInitial C
f : x ⟶ y
x_1 : Quiver.Hom.{v, u} (V := WithInitial C) star star
⊢ Eq (α := (ofCommaObject c).obj star ⟶ (ofCommaObject c').obj star)
    ((ofCommaObject c).map x_1 ≫
      match (motive := (x : WithInitial C) → (ofCommaObject c).obj x ⟶ (ofCommaObject c').obj x) star with
      | of x => φ.right.app x
      | star => φ.left)
    ((match (motive := (x : WithInitial C) → (ofCommaObject c).obj x ⟶ (ofCommaObject c').obj x) star with
      | of x => φ.right.app x
      | star => φ.left) ≫
      (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} (WithInitial C) D
x y : C
f : x ⟶ y
simp :
  F.map (Limits.IsInitial.to starInitial (of x)) ≫ F.map (Functor.map incl f) =
    F.map (Limits.IsInitial.to starInitial (of y))
⊢ Eq (α := F.obj star ⟶ (incl ⋙ F).obj y)
    ((fun (x : C) ↦ F.map (Limits.IsInitial.to starInitial (of x))) x ≫ (incl ⋙ F).map f)
    ((fun (x : C) ↦ F.map (Limits.IsInitial.to starInitial (of x))) y)

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} (WithInitial C) D
x y : C
f : x ⟶ y
rw :
  F.map (Limits.IsInitial.to starInitial (of x) ≫ Functor.map incl f) = F.map (Limits.IsInitial.to starInitial (of y))
⊢ F.map (Limits.IsInitial.to starInitial (of x)) ≫ F.map (Functor.map incl f) =
    F.map (Limits.IsInitial.to starInitial (of y))

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} (WithInitial C) D
x y : C
f : x ⟶ y
⊢ F.map (Limits.IsInitial.to starInitial (of x) ≫ Functor.map incl f) = F.map (Limits.IsInitial.to starInitial (of y))

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
F : Functor.{v, v_1, u, u_1} (WithInitial C) D
x : C
simp :
  F.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) =
    F.map (Limits.IsInitial.to starInitial (of x))
⊢ Iso.hom (Iso.symm (Iso.refl (F.obj star))) ≫
      F.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) =
    (fun (x : C) ↦ F.map (Limits.IsInitial.to starInitial (of x))) x ≫
      NatTrans.app (Iso.hom (Iso.symm (Iso.refl (incl ⋙ F)))) x

Tactic:
simp only [Iso.refl_symm, 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.Iso.refl_symm, 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} (WithInitial C) D
x : C
⊢ F.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) =
    F.map (Limits.IsInitial.to starInitial (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} (WithInitial C) D
f : x ⟶ y
a : C
⊢ Eq (α :=
    (Functor.obj (𝟭 (Functor.{v, v_1, u, u_1} (WithInitial C) D)) x).obj (of a) ⟶
      (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
        (of a))
    (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))
      (of a))
    (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)
      (of a))

Tactic:
simp [incl]

Premises used: CategoryTheory.WithInitial.incl