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