[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a b c d : WithTerminal C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases a
[GOAL]
case of
C : Type u
inst✝ : Category.{v, u} C
b c d : WithTerminal C
g : b ⟶ c
h : c ⟶ d
a✝ : C
f : of a✝ ⟶ b
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases b
[GOAL]
case star
C : Type u
inst✝ : Category.{v, u} C
b c d : WithTerminal C
g : b ⟶ c
h : c ⟶ d
f : star ⟶ b
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases b
[GOAL]
case of.of
C : Type u
inst✝ : Category.{v, u} C
c d : WithTerminal C
h : c ⟶ d
a✝¹ a✝ : C
g : of a✝ ⟶ c
f : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case of.star
C : Type u
inst✝ : Category.{v, u} C
c d : WithTerminal C
h : c ⟶ d
a✝ : C
g : star ⟶ c
f : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case star.of
C : Type u
inst✝ : Category.{v, u} C
c d : WithTerminal C
h : c ⟶ d
a✝ : C
g : of a✝ ⟶ c
f : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case star.star
C : Type u
inst✝ : Category.{v, u} C
c d : WithTerminal C
h : c ⟶ d
g : star ⟶ c
f : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case of.of.of
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝ ⟶ d
g : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.of.star
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
h : star ⟶ d
g : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.star.of
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
a✝¹ : C
f : of a✝¹ ⟶ star
a✝ : C
h : of a✝ ⟶ d
g : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.star.star
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
a✝ : C
f : of a✝ ⟶ star
h : star ⟶ d
g : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.of.of
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
a✝¹ : C
f : star ⟶ of a✝¹
a✝ : C
h : of a✝ ⟶ d
g : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.of.star
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
a✝ : C
f : star ⟶ of a✝
h : star ⟶ d
g : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.star.of
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
f : star ⟶ star
a✝ : C
h : of a✝ ⟶ d
g : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.star.star
C : Type u
inst✝ : Category.{v, u} C
d : WithTerminal C
f : star ⟶ star
h : star ⟶ d
g : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝³ a✝² : C
f : of a✝³ ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝³ a✝² : C
f : of a✝³ ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : of a✝² ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : of a✝² ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : of a✝ ⟶ star
g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : of a✝ ⟶ star
g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : star ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : star ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : star ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : star ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.of.of
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.of.of
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.of.star
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.of.star
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.star.of
C : Type u
inst✝ : Category.{v, u} C
f g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.star.of
C : Type u
inst✝ : Category.{v, u} C
f g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.star.star
C : Type u
inst✝ : Category.{v, u} C
f g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.star.star
C : Type u
inst✝ : Category.{v, u} C
f g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
exact (h : PEmpty).elim
[GOAL]
case of.star.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : of a✝² ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
exact (g : PEmpty).elim
[GOAL]
case of.star.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
exact (h : PEmpty).elim
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : WithTerminal C
⊢ ∀ (a : X ⟶ star), a = default
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : 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
⊢ (lift F M hM).map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ (liftStar F M hM).hom =
    NatTrans.app (inclLift F M hM).hom x ≫ M x
[PROOFSTEP]
erw [Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : 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
⊢ (lift F M hM).map (Limits.IsTerminal.from starTerminal (incl.obj x)) = M x
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
⊢ ∀ {X Y : WithTerminal C} (f : X ⟶ Y),
    G.map f ≫
        ((fun X =>
              match X with
              | of x => h.app x
              | star => hG)
            Y).hom =
      ((fun X =>
              match X with
              | of x => h.app x
              | star => hG)
            X).hom ≫
        (lift F M hM).map f
[PROOFSTEP]
rintro (X | X) (Y | Y) f
[GOAL]
case of.of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
X Y : C
f : of X ⟶ of Y
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of Y)).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of X)).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
apply h.hom.naturality
[GOAL]
case of.star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
X : C
f : of X ⟶ star
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of X)).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
cases f
[GOAL]
case of.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
X : C
⊢ G.map PUnit.unit ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of X)).hom ≫
      (lift F M hM).map PUnit.unit
[PROOFSTEP]
exact hh _
[GOAL]
case star.of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
Y : C
f : star ⟶ of Y
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of Y)).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
cases f
[GOAL]
case star.star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
f : star ⟶ star
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
cases f
[GOAL]
case star.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
⊢ G.map PUnit.unit ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map PUnit.unit
[PROOFSTEP]
change G.map (𝟙 _) ≫ hG.hom = hG.hom ≫ 𝟙 _
[GOAL]
case star.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.139406, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (Limits.IsTerminal.from starTerminal (incl.obj x)) ≫ hG.hom = NatTrans.app h.hom x ≫ M x
⊢ G.map (𝟙 star) ≫ hG.hom = hG.hom ≫ 𝟙 Z
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
a b c d : WithInitial C
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases a
[GOAL]
case of
C : Type u
inst✝ : Category.{v, u} C
b c d : WithInitial C
g : b ⟶ c
h : c ⟶ d
a✝ : C
f : of a✝ ⟶ b
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases b
[GOAL]
case star
C : Type u
inst✝ : Category.{v, u} C
b c d : WithInitial C
g : b ⟶ c
h : c ⟶ d
f : star ⟶ b
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases b
[GOAL]
case of.of
C : Type u
inst✝ : Category.{v, u} C
c d : WithInitial C
h : c ⟶ d
a✝¹ a✝ : C
g : of a✝ ⟶ c
f : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case of.star
C : Type u
inst✝ : Category.{v, u} C
c d : WithInitial C
h : c ⟶ d
a✝ : C
g : star ⟶ c
f : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case star.of
C : Type u
inst✝ : Category.{v, u} C
c d : WithInitial C
h : c ⟶ d
a✝ : C
g : of a✝ ⟶ c
f : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case star.star
C : Type u
inst✝ : Category.{v, u} C
c d : WithInitial C
h : c ⟶ d
g : star ⟶ c
f : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases c
[GOAL]
case of.of.of
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝ ⟶ d
g : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.of.star
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
h : star ⟶ d
g : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.star.of
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
a✝¹ : C
f : of a✝¹ ⟶ star
a✝ : C
h : of a✝ ⟶ d
g : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.star.star
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
a✝ : C
f : of a✝ ⟶ star
h : star ⟶ d
g : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.of.of
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
a✝¹ : C
f : star ⟶ of a✝¹
a✝ : C
h : of a✝ ⟶ d
g : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.of.star
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
a✝ : C
f : star ⟶ of a✝
h : star ⟶ d
g : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.star.of
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
f : star ⟶ star
a✝ : C
h : of a✝ ⟶ d
g : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case star.star.star
C : Type u
inst✝ : Category.{v, u} C
d : WithInitial C
f : star ⟶ star
h : star ⟶ d
g : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
cases d
[GOAL]
case of.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝³ a✝² : C
f : of a✝³ ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝³ a✝² : C
f : of a✝³ ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : of a✝² ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : of a✝² ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.star.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : of a✝ ⟶ star
g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case of.star.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : of a✝ ⟶ star
g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : star ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : star ⟶ of a✝²
a✝¹ : C
g : of a✝² ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.of.star
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
a✝ : C
g : of a✝¹ ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : star ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : star ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.of.star.star
C : Type u
inst✝ : Category.{v, u} C
a✝ : C
f : star ⟶ of a✝
g : of a✝ ⟶ star
h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.of.of
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.of.of
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.of.star
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.of.star
C : Type u
inst✝ : Category.{v, u} C
f : star ⟶ star
a✝ : C
g : star ⟶ of a✝
h : of a✝ ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.star.of
C : Type u
inst✝ : Category.{v, u} C
f g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.star.of
C : Type u
inst✝ : Category.{v, u} C
f g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case star.star.star.star
C : Type u
inst✝ : Category.{v, u} C
f g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
try aesop_cat
[GOAL]
case star.star.star.star
C : Type u
inst✝ : Category.{v, u} C
f g h : star ⟶ star
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
aesop_cat
[GOAL]
case of.of.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝² a✝¹ : C
f : of a✝² ⟶ of a✝¹
g : of a✝¹ ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
exact (g : PEmpty).elim
[GOAL]
case of.star.of.of
C : Type u
inst✝ : Category.{v, u} C
a✝² : C
f : of a✝² ⟶ star
a✝¹ : C
g : star ⟶ of a✝¹
a✝ : C
h : of a✝¹ ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
exact (f : PEmpty).elim
[GOAL]
case of.star.star.of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ : C
f : of a✝¹ ⟶ star
g : star ⟶ star
a✝ : C
h : star ⟶ of a✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
exact (f : PEmpty).elim
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : WithInitial C
⊢ ∀ (a : star ⟶ X), a = default
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
x : C
⊢ (liftStar F M hM).hom ≫ (lift F M hM).map (Limits.IsInitial.to starInitial (incl.obj x)) =
    M x ≫ NatTrans.app (inclLift F M hM).hom x
[PROOFSTEP]
erw [Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
x : C
⊢ (lift F M hM).map (Limits.IsInitial.to starInitial (incl.obj x)) = M x
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
⊢ ∀ {X Y : WithInitial C} (f : X ⟶ Y),
    G.map f ≫
        ((fun X =>
              match X with
              | of x => h.app x
              | star => hG)
            Y).hom =
      ((fun X =>
              match X with
              | of x => h.app x
              | star => hG)
            X).hom ≫
        (lift F M hM).map f
[PROOFSTEP]
rintro (X | X) (Y | Y) f
[GOAL]
case of.of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
X Y : C
f : of X ⟶ of Y
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of Y)).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of X)).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
apply h.hom.naturality
[GOAL]
case of.star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
X : C
f : of X ⟶ star
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of X)).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
cases f
[GOAL]
case star.of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
Y : C
f : star ⟶ of Y
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of Y)).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
cases f
[GOAL]
case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
Y : C
⊢ G.map PUnit.unit ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          (of Y)).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map PUnit.unit
[PROOFSTEP]
change G.map _ ≫ h.hom.app _ = hG.hom ≫ _
[GOAL]
case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
Y : C
⊢ G.map PUnit.unit ≫ NatTrans.app h.hom Y = hG.hom ≫ (lift F M hM).map PUnit.unit
[PROOFSTEP]
symm
[GOAL]
case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
Y : C
⊢ hG.hom ≫ (lift F M hM).map PUnit.unit = G.map PUnit.unit ≫ NatTrans.app h.hom Y
[PROOFSTEP]
erw [← Iso.eq_inv_comp, ← Category.assoc, hh]
[GOAL]
case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
Y : C
⊢ (lift F M hM).map PUnit.unit = (M Y ≫ NatTrans.app h.symm.hom Y) ≫ NatTrans.app h.hom Y
[PROOFSTEP]
simp
[GOAL]
case star.star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
f : star ⟶ star
⊢ G.map f ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map f
[PROOFSTEP]
cases f
[GOAL]
case star.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
⊢ G.map PUnit.unit ≫
      ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom =
    ((fun X =>
            match X with
            | of x => h.app x
            | star => hG)
          star).hom ≫
      (lift F M hM).map PUnit.unit
[PROOFSTEP]
change G.map (𝟙 _) ≫ hG.hom = hG.hom ≫ 𝟙 _
[GOAL]
case star.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{?u.289890, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (incl.obj x)) = M x ≫ NatTrans.app h.symm.hom x
⊢ G.map (𝟙 star) ≫ hG.hom = hG.hom ≫ 𝟙 Z
[PROOFSTEP]
simp
