C : Type u
inst✝¹ : Category C
D : Type u_1
inst✝ : Category 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
C : Type u
inst✝¹ : Category C
D : Type u_1
inst✝ : Category 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 =
    (inclLift F M hM).hom.app x ≫ M 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) → 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
rfl