C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ A.op
hf : Mono f
⊢ S.map (Subobject.arrow (Subobject.mk f.unop.left.op)).unop ≫
      S.map (Subobject.underlyingIso f.unop.left.op).inv.unop ≫ P.unop.hom =
    A.hom
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ A.op
hf : Mono f
⊢ S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫
      S.map (Iso.unop (Subobject.underlyingIso (MonoOver.arrow (MonoOver.mk' f)).unop.left.op)).inv ≫ P.unop.hom =
    A.hom
dsimp
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ A.op
hf : Mono f
⊢ S.map ((Subobject.underlyingIso f.unop.left.op).inv ≫ Subobject.arrow (Subobject.mk f.unop.left.op)).unop ≫
      P.unop.hom =
    A.hom
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ A.op
hf : Mono f
⊢ S.map (Subobject.arrow (Subobject.mk f.unop.left.op)).unop ≫
      S.map (Subobject.underlyingIso f.unop.left.op).inv.unop ≫ P.unop.hom =
    A.hom
rw [← Category.assoc, ← S.map_comp, ← unop_comp]
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ A.op
hf : Mono f
⊢ S.map ((Subobject.underlyingIso f.unop.left.op).inv ≫ Subobject.arrow (Subobject.mk f.unop.left.op)).unop ≫
      P.unop.hom =
    A.hom
simp