case intro.intro
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A : C
h✝ f✝ g✝ : Subobject A
f g h : MonoOver A
k : f ⟶ g
l : f ⟶ h
⊢ Quotient.mk'' f ≤ (inf.obj (Quotient.mk'' g)).obj (Quotient.mk'' h)
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A : C
h f g : Subobject A
⊢ ∀ (a₁ a₂ a₃ : MonoOver A),
    Quotient.mk'' a₁ ≤ Quotient.mk'' a₂ →
      Quotient.mk'' a₁ ≤ Quotient.mk'' a₃ → Quotient.mk'' a₁ ≤ (inf.obj (Quotient.mk'' a₂)).obj (Quotient.mk'' a₃)
rintro f g h ⟨k⟩ ⟨l⟩
no goals
case intro.intro
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A : C
h✝ f✝ g✝ : Subobject A
f g h : MonoOver A
k : f ⟶ g
l : f ⟶ h
⊢ Quotient.mk'' f ≤ (inf.obj (Quotient.mk'' g)).obj (Quotient.mk'' h)
exact ⟨MonoOver.leInf _ _ _ k l⟩