case h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
⊢ ∀ (f_1 : W ⟶ Y), (generate (Presieve.pullbackArrows f R)).arrows f_1 ↔ (pullback f (generate R)).arrows f_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
⊢ generate (Presieve.pullbackArrows f R) = pullback f (generate R)
ext W
case h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g ↔ (pullback f (generate R)).arrows 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✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
⊢ ∀ (f_1 : W ⟶ Y), (generate (Presieve.pullbackArrows f R)).arrows f_1 ↔ (pullback f (generate R)).arrows f_1
intro g
case h.mp
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g → (pullback f (generate R)).arrows g

case h.mpr
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (pullback f (generate R)).arrows g → (generate (Presieve.pullbackArrows f R)).arrows 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✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g ↔ (pullback f (generate R)).arrows g
constructor
case h.mp.intro.intro.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W w✝ : C
h : W ⟶ w✝
k : w✝ ⟶ Y
hk : Presieve.pullbackArrows f R k
⊢ (pullback f (generate R)).arrows (h ≫ k)
case h.mp
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g → (pullback f (generate R)).arrows g
rintro ⟨_, h, k, hk, rfl⟩
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd)
case h.mp.intro.intro.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W w✝ : C
h : W ⟶ w✝
k : w✝ ⟶ Y
hk : Presieve.pullbackArrows f R k
⊢ (pullback f (generate R)).arrows (h ≫ k)
cases' hk with W g hg
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd)
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd)
change (Sieve.generate R).pullback f (h ≫ pullback.snd)
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (generate R).arrows ((h ≫ pullback.fst) ≫ g)
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd)
rw [Sieve.pullback_apply, assoc, ← pullback.condition, ← assoc]
no goals
case h.mp.intro.intro.intro.intro.mk
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (generate R).arrows ((h ≫ pullback.fst) ≫ g)
exact Sieve.downward_closed _ (by exact Sieve.le_generate R W hg) (h ≫ pullback.fst)
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
⊢ (generate R).arrows g
exact Sieve.le_generate R W hg
case h.mpr.intro.intro.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ : C
g : W✝ ⟶ Y
W : C
h : W✝ ⟶ W
k : W ⟶ X
hk : R k
comm : h ≫ k = g ≫ f
⊢ (generate (Presieve.pullbackArrows f R)).arrows g
case h.mpr
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W : C
g : W ⟶ Y
⊢ (pullback f (generate R)).arrows g → (generate (Presieve.pullbackArrows f R)).arrows g
rintro ⟨W, h, k, hk, comm⟩
no goals
case h.mpr.intro.intro.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X✝ Y✝ Z : C
f✝ : Y✝ ⟶ X✝
S R✝ : Sieve X✝
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
R : Presieve X
W✝ : C
g : W✝ ⟶ Y
W : C
h : W✝ ⟶ W
k : W ⟶ X
hk : R k
comm : h ≫ k = g ≫ f
⊢ (generate (Presieve.pullbackArrows f R)).arrows g
exact ⟨_, _, _, Presieve.pullbackArrows.mk _ _ hk, pullback.lift_snd _ _ comm⟩