case 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
R : Presieve X
S : Sieve X
ss : R ≤ S.arrows
Y Z : C
f : Y ⟶ Z
g : Z ⟶ X
hg : R g
⊢ S.arrows (f ≫ g)
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
R : Presieve X
S : Sieve X
ss : R ≤ S.arrows
Y : C
f : Y ⟶ X
⊢ (generate R).arrows f → S.arrows f
rintro ⟨Z, f, g, hg, rfl⟩
no goals
case 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
R : Presieve X
S : Sieve X
ss : R ≤ S.arrows
Y Z : C
f : Y ⟶ Z
g : Z ⟶ X
hg : R g
⊢ S.arrows (f ≫ g)
exact S.downward_closed (ss Z hg) f