case intro
C : Type u₁
inst✝¹ : Category C
X Y Z : C
D : Type u₂
inst✝ : Category D
P : Subobject X
Q : MonoOver X
e : Quotient.out' (Quotient.mk'' Q) ≅ Q
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q
C : Type u₁
inst✝¹ : Category C
X Y Z : C
D : Type u₂
inst✝ : Category D
P : Subobject X
Q : MonoOver X
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q
obtain ⟨e⟩ := @Quotient.mk_out' _ (isIsomorphicSetoid _) Q
no goals
case intro
C : Type u₁
inst✝¹ : Category C
X Y Z : C
D : Type u₂
inst✝ : Category D
P : Subobject X
Q : MonoOver X
e : Quotient.out' (Quotient.mk'' Q) ≅ Q
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q
exact Quotient.sound' ⟨MonoOver.isoMk (Iso.refl _)  ≪≫ e⟩