C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ A.op
inst✝ : Mono f.unop.left.op
⊢ f.unop.left.op.unop ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop =
    (Subobject.arrow (Subobject.mk f.unop.left.op)).unop
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ A.op
inst✝ : Mono f.unop.left.op
⊢ f.unop.left ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop = (Subobject.arrow (Subobject.mk f.unop.left.op)).unop
conv_lhs =>
  congr
  rw [← Quiver.Hom.unop_op f.unop.left]
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ A.op
inst✝ : Mono f.unop.left.op
⊢ f.unop.left.op.unop ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop =
    (Subobject.arrow (Subobject.mk f.unop.left.op)).unop
rw [← unop_comp, Subobject.underlyingIso_hom_comp_eq_mk]