case h
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A : C
f₁ f₂ : MonoOver A
⊢ (inf.obj (Quotient.mk'' f₁)).obj (Quotient.mk'' f₂) =
    (map (MonoOver.arrow f₁)).obj ((pullback (MonoOver.arrow f₁)).obj (Quotient.mk'' f₂))
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A : C
f₁ : MonoOver A
f₂ : Subobject A
⊢ (inf.obj (Quotient.mk'' f₁)).obj f₂ = (map (MonoOver.arrow f₁)).obj ((pullback (MonoOver.arrow f₁)).obj f₂)
induction' f₂ using Quotient.inductionOn' with f₂
no goals
case h
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A : C
f₁ f₂ : MonoOver A
⊢ (inf.obj (Quotient.mk'' f₁)).obj (Quotient.mk'' f₂) =
    (map (MonoOver.arrow f₁)).obj ((pullback (MonoOver.arrow f₁)).obj (Quotient.mk'' f₂))
rfl