C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasPullbacks C
f : X ⟶ Y
inst✝ : Mono f
⊢ ∀ (g : Subobject X), (pullback f).obj ((map f).obj g) = g
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasPullbacks C
f : X ⟶ Y
inst✝ : Mono f
g : Subobject X
⊢ (pullback f).obj ((map f).obj g) = g
revert g
no goals
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasPullbacks C
f : X ⟶ Y
inst✝ : Mono f
⊢ ∀ (g : Subobject X), (pullback f).obj ((map f).obj g) = g
exact Quotient.ind (fun g' => Quotient.sound ⟨(MonoOver.pullbackMapSelf f).app _⟩)