no goals
C : Type u
inst✝ : Category C
X✝ : SimplicialObject C
X Y : Augmented C
f : X ⟶ Y
⊢ (drop.map f).app [0].op ≫ Y.hom.app [0].op = X.hom.app [0].op ≫ point.map f
convert congr_app f.w (op (SimplexCategory.mk 0))