C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
⊢ ∀ {X Y : Subobject B}, Factors X f ∧ Factors Y f → Factors (X ⊓ Y) f
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A B : C
X Y : Subobject B
f : A ⟶ B
⊢ Factors X f ∧ Factors Y f → Factors (X ⊓ Y) f
revert X Y
case h
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
⊢ ∀ (a₁ a₂ : MonoOver B),
    Factors (Quotient.mk'' a₁) f ∧ Factors (Quotient.mk'' a₂) f → Factors (Quotient.mk'' a₁ ⊓ Quotient.mk'' a₂) f
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
⊢ ∀ {X Y : Subobject B}, Factors X f ∧ Factors Y f → Factors (X ⊓ Y) f
apply Quotient.ind₂'
case h.intro.intro.intro
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A B : C
X Y : MonoOver B
g₁ : A ⟶ X.obj.left
g₂ : A ⟶ Y.obj.left
hg₂ : g₂ ≫ MonoOver.arrow Y = g₁ ≫ MonoOver.arrow X
⊢ Factors (Quotient.mk'' X ⊓ Quotient.mk'' Y) (g₁ ≫ MonoOver.arrow X)
case h
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
⊢ ∀ (a₁ a₂ : MonoOver B),
    Factors (Quotient.mk'' a₁) f ∧ Factors (Quotient.mk'' a₂) f → Factors (Quotient.mk'' a₁ ⊓ Quotient.mk'' a₂) f
rintro X Y ⟨⟨g₁, rfl⟩, ⟨g₂, hg₂⟩⟩
no goals
case h.intro.intro.intro
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
A B : C
X Y : MonoOver B
g₁ : A ⟶ X.obj.left
g₂ : A ⟶ Y.obj.left
hg₂ : g₂ ≫ MonoOver.arrow Y = g₁ ≫ MonoOver.arrow X
⊢ Factors (Quotient.mk'' X ⊓ Quotient.mk'' Y) (g₁ ≫ MonoOver.arrow X)
exact ⟨_, pullback.lift_snd_assoc _ _ hg₂ _⟩