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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
⊢ (ofArrows (fun i => pullback (g i) f) fun i => pullback.snd) = pullbackArrows f (ofArrows Z g)
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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
⊢ (ofArrows (fun i => pullback (g i) f) fun i => pullback.snd) = pullbackArrows f (ofArrows Z g)
funext T
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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ (h ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd) ↔ h ∈ pullbackArrows f (ofArrows Z g)
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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
⊢ (ofArrows (fun i => pullback (g i) f) fun i => pullback.snd) = pullbackArrows f (ofArrows Z g)
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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ (h ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd) → h ∈ pullbackArrows f (ofArrows Z 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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ h ∈ pullbackArrows f (ofArrows Z g) → h ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd
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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ (h ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd) ↔ h ∈ pullbackArrows f (ofArrows Z g)
constructor
case h.h.mp.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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y : C
hk : ι
⊢ pullback.snd ∈ pullbackArrows f (ofArrows Z g)
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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ (h ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd) → h ∈ pullbackArrows f (ofArrows Z g)
rintro ⟨hk⟩
no goals
case h.h.mp.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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y : C
hk : ι
⊢ pullback.snd ∈ pullbackArrows f (ofArrows Z g)
exact pullbackArrows.mk _ _ (ofArrows.mk hk)
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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y W : C
k : W ⟶ X
hk₁ : ofArrows Z g k
⊢ pullback.snd ∈ ofArrows (fun i => pullback (g i) f) fun i => 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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
T : C
h : T ⟶ Y
⊢ h ∈ pullbackArrows f (ofArrows Z g) → h ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd
rintro ⟨W, k, hk₁⟩
case h.h.mpr.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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y : C
i : ι
⊢ pullback.snd ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd
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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y W : C
k : W ⟶ X
hk₁ : ofArrows Z g k
⊢ pullback.snd ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd
cases' hk₁ with i hi
no goals
case h.h.mpr.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
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
Y : C
i : ι
⊢ pullback.snd ∈ ofArrows (fun i => pullback (g i) f) fun i => pullback.snd
apply ofArrows.mk