C : Type u₁
inst✝³ : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
⊢ ∀ (f₁ : Subobject Y), (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map 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 : Y ⟶ X
inst✝ : Mono g
f₁ f₂ : Subobject Y
⊢ (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map 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 : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
⊢ ∀ (a : MonoOver Y), (map g).obj (Quotient.mk'' a ⊓ f₂) = (map g).obj (Quotient.mk'' a) ⊓ (map 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 : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
⊢ ∀ (f₁ : Subobject Y), (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map 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 : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj (Quotient.mk'' f₁ ⊓ f₂) = (map g).obj (Quotient.mk'' f₁) ⊓ (map 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 : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
⊢ ∀ (a : MonoOver Y), (map g).obj (Quotient.mk'' a ⊓ f₂) = (map g).obj (Quotient.mk'' a) ⊓ (map 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 : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (MonoOver.arrow f₁ ≫ g)).obj ((pullback (MonoOver.arrow f₁)).obj f₂) =
    (map (MonoOver.arrow ((MonoOver.map g).obj f₁))).obj
      ((pullback (MonoOver.arrow ((MonoOver.map g).obj f₁))).obj ((map 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 : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj (Quotient.mk'' f₁ ⊓ f₂) = (map g).obj (Quotient.mk'' f₁) ⊓ (map g).obj f₂
erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← map_comp]
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 : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (MonoOver.arrow f₁ ≫ g)).obj ((pullback (MonoOver.arrow f₁)).obj f₂) =
    (map (MonoOver.arrow f₁ ≫ g)).obj ((pullback (MonoOver.arrow f₁ ≫ g)).obj ((map 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 : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (MonoOver.arrow f₁ ≫ g)).obj ((pullback (MonoOver.arrow f₁)).obj f₂) =
    (map (MonoOver.arrow ((MonoOver.map g).obj f₁))).obj
      ((pullback (MonoOver.arrow ((MonoOver.map g).obj f₁))).obj ((map g).obj f₂))
dsimp
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 : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (MonoOver.arrow f₁ ≫ g)).obj ((pullback (MonoOver.arrow f₁)).obj f₂) =
    (map (MonoOver.arrow f₁ ≫ g)).obj ((pullback (MonoOver.arrow f₁ ≫ g)).obj ((map g).obj f₂))
rw [pullback_comp, pullback_map_self]