T : Type u₁
inst✝ : Category T
X : T
A B : Under X
f : A ⟶ B
this : (Functor.fromPUnit X).map f.left ≫ B.hom = A.hom ≫ (𝟭 T).map f.right
⊢ A.hom ≫ f.right = B.hom
T : Type u₁
inst✝ : Category T
X : T
A B : Under X
f : A ⟶ B
⊢ A.hom ≫ f.right = B.hom
have := f.w
no goals
T : Type u₁
inst✝ : Category T
X : T
A B : Under X
f : A ⟶ B
this : (Functor.fromPUnit X).map f.left ≫ B.hom = A.hom ≫ (𝟭 T).map f.right
⊢ A.hom ≫ f.right = B.hom
aesop_cat