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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f
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
⊢ ∀ ⦃A_1 : (CostructuredArrow S T)ᵒᵖ⦄ (f : A_1 ⟶ A.op) [inst : Mono f]
    {q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right}
    (hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom),
    liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f
intro P f hf q hq
case i
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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ (mk q).op ≅ P

case w
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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ ?i.hom ≫ f = (homMk (Subobject.arrow (projectQuotient (Subobject.mk f))).unop).op
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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f
fapply Subobject.mk_eq_mk_of_comm
case i.refine'_1
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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ P.unop.left ≅ (mk q).left

case i.refine'_2
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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ S.map ?i.refine'_1.hom ≫ (mk q).hom = P.unop.hom
case i
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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ (mk q).op ≅ P
refine' (Iso.op (isoMk _ _) : _ ≅ op (unop P))
no goals
case i.refine'_1
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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ P.unop.left ≅ (mk q).left
exact (Subobject.underlyingIso f.unop.left.op).unop
case i.refine'_2
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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ S.map f.unop.left ≫ S.map (Iso.unop (Subobject.underlyingIso f.unop.left.op)).hom ≫ (mk q).hom =
    S.map f.unop.left ≫ P.unop.hom
case i.refine'_2
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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ S.map (Iso.unop (Subobject.underlyingIso f.unop.left.op)).hom ≫ (mk q).hom = P.unop.hom
refine' (cancel_epi (S.map f.unop.left)).1 _
no goals
case i.refine'_2
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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ S.map f.unop.left ≫ S.map (Iso.unop (Subobject.underlyingIso f.unop.left.op)).hom ≫ (mk q).hom =
    S.map f.unop.left ≫ P.unop.hom
simpa [← Category.assoc, ← S.map_comp] using hq
no goals
case w
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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ (Iso.op (isoMk (Iso.unop (Subobject.underlyingIso f.unop.left.op)))).hom ≫ f =
    (homMk (Subobject.arrow (projectQuotient (Subobject.mk f))).unop).op
exact Quiver.Hom.unop_inj (by aesop_cat)
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
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ ((Iso.op (isoMk (Iso.unop (Subobject.underlyingIso f.unop.left.op)))).hom ≫ f).unop =
    (homMk (Subobject.arrow (projectQuotient (Subobject.mk f))).unop).op.unop
aesop_cat