C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
⊢ ∀ (f₁ : Subobject Y), (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₁ f₂ : Subobject Y
⊢ (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂
revert f₁
case h
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
⊢ ∀ (a : MonoOver Y), (pullback g).obj (Quotient.mk'' a ⊓ f₂) = (pullback g).obj (Quotient.mk'' a) ⊓ (pullback g).obj f₂
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
⊢ ∀ (f₁ : Subobject Y), (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂
apply Quotient.ind'
case h
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj (Quotient.mk'' f₁ ⊓ f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂
case h
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
⊢ ∀ (a : MonoOver Y), (pullback g).obj (Quotient.mk'' a ⊓ f₂) = (pullback g).obj (Quotient.mk'' a) ⊓ (pullback g).obj f₂
intro f₁
case h
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map pullback.snd).obj ((pullback (pullback.snd ≫ g)).obj f₂) =
    (map (MonoOver.arrow ((MonoOver.pullback g).obj f₁))).obj
      ((pullback (MonoOver.arrow ((MonoOver.pullback g).obj f₁) ≫ g)).obj f₂)
case h
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj (Quotient.mk'' f₁ ⊓ f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂
erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← pullback_comp, ←
  map_pullback pullback.condition (pullbackIsPullback f₁.arrow g), ← pullback_comp,
  pullback.condition]
no goals
case h
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map pullback.snd).obj ((pullback (pullback.snd ≫ g)).obj f₂) =
    (map (MonoOver.arrow ((MonoOver.pullback g).obj f₁))).obj
      ((pullback (MonoOver.arrow ((MonoOver.pullback g).obj f₁) ≫ g)).obj f₂)
rfl