case h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
⊢ pullbackArrows f (singleton g) = singleton pullback.snd
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
⊢ pullbackArrows f (singleton g) = singleton pullback.snd
funext W
case h.h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ pullbackArrows f (singleton g) ↔ h ∈ singleton pullback.snd
case h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
⊢ pullbackArrows f (singleton g) = singleton pullback.snd
ext h
case h.h.mp
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ pullbackArrows f (singleton g) → h ∈ singleton pullback.snd

case h.h.mpr
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ singleton pullback.snd → h ∈ pullbackArrows f (singleton g)
case h.h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ pullbackArrows f (singleton g) ↔ h ∈ singleton pullback.snd
constructor
case h.h.mp.mk.mk
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y✝¹ Z : C
f : Y✝¹ ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
Y✝ Y : C
⊢ pullback.snd ∈ singleton pullback.snd
case h.h.mp
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ pullbackArrows f (singleton g) → h ∈ singleton pullback.snd
rintro ⟨W, _, _, _⟩
no goals
case h.h.mp.mk.mk
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y✝¹ Z : C
f : Y✝¹ ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
Y✝ Y : C
⊢ pullback.snd ∈ singleton pullback.snd
exact singleton.mk
case h.h.mpr.mk
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
Y : C
⊢ pullback.snd ∈ pullbackArrows f (singleton g)
case h.h.mpr
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
W : C
h : W ⟶ Y
⊢ h ∈ singleton pullback.snd → h ∈ pullbackArrows f (singleton g)
rintro ⟨_⟩
no goals
case h.h.mpr.mk
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
inst✝ : HasPullbacks C
g : Z ⟶ X
Y : C
⊢ pullback.snd ∈ pullbackArrows f (singleton g)
exact pullbackArrows.mk Z g singleton.mk