C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
⊢ Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T) ∈
    GrothendieckTopology.sieves J ((Over.forget X).obj Y)
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
⊢ LocallyCoverDense J (Over.forget X)
intro Y T
case h.e'_4
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
⊢ Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T) = ↑T
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
⊢ Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T) ∈
    GrothendieckTopology.sieves J ((Over.forget X).obj Y)
convert T.property
case h.e'_4.h
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
⊢ ∀ (f : Z ⟶ (Over.forget X).obj Y),
    (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f ↔ (↑T).arrows f
case h.e'_4
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
⊢ Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T) = ↑T
ext Z
case h.e'_4.h
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f ↔ (↑T).arrows f
case h.e'_4.h
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
⊢ ∀ (f : Z ⟶ (Over.forget X).obj Y),
    (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f ↔ (↑T).arrows f
intro f
case h.e'_4.h.mp
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f → (↑T).arrows f

case h.e'_4.h.mpr
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (↑T).arrows f → (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f
case h.e'_4.h
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f ↔ (↑T).arrows f
constructor
case h.e'_4.h.mp.intro.intro.intro.intro
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
w✝¹ : Over X
w✝ : w✝¹ ⟶ Y
g' : Z ⟶ (Over.forget X).obj w✝¹
hg : (Sieve.functorPullback (Over.forget X) ↑T).arrows w✝
⊢ (↑T).arrows (g' ≫ (Over.forget X).map w✝)
case h.e'_4.h.mp
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f → (↑T).arrows f
rintro ⟨_, _, g', hg, rfl⟩
no goals
case h.e'_4.h.mp.intro.intro.intro.intro
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
w✝¹ : Over X
w✝ : w✝¹ ⟶ Y
g' : Z ⟶ (Over.forget X).obj w✝¹
hg : (Sieve.functorPullback (Over.forget X) ↑T).arrows w✝
⊢ (↑T).arrows (g' ≫ (Over.forget X).map w✝)
exact T.val.downward_closed hg g'
case h.e'_4.h.mpr
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
hf : (↑T).arrows f
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f
case h.e'_4.h.mpr
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (↑T).arrows f → (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f
intro hf
no goals
case h.e'_4.h.mpr
C : Type u_1
inst✝² : Category C
D : Type ?u.13308
inst✝¹ : Category D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝ : Category A
X : C
Y : Over X
T : ↑(GrothendieckTopology.sieves J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
hf : (↑T).arrows f
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f
exact ⟨Over.mk (f ≫ Y.hom), Over.homMk f, 𝟙 _, hf, (Category.id_comp _).symm⟩