C : Type u
inst✝¹ : Category C
D : Type u_1
inst✝ : Category 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
C : Type u
inst✝¹ : Category C
D : Type u_1
inst✝ : Category 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 ≫ (inclLift F M hM).hom.app x
erw [Category.id_comp, Category.comp_id]
no goals
C : Type u
inst✝¹ : Category C
D : Type u_1
inst✝ : Category 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
rfl