C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
A : Type u₃
inst✝ : Category A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
F : C ⥤ D
hF : CoverPreserving J K F
G : D ⥤ A
hG : CoverPreserving K L G
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ GrothendieckTopology.sieves J U✝
⊢ Sieve.functorPushforward G (Sieve.functorPushforward F S✝) ∈ GrothendieckTopology.sieves L ((F ⋙ G).obj U✝)
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
A : Type u₃
inst✝ : Category A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
F : C ⥤ D
hF : CoverPreserving J K F
G : D ⥤ A
hG : CoverPreserving K L G
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ GrothendieckTopology.sieves J U✝
⊢ Sieve.functorPushforward (F ⋙ G) S✝ ∈ GrothendieckTopology.sieves L ((F ⋙ G).obj U✝)
rw [Sieve.functorPushforward_comp]
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
A : Type u₃
inst✝ : Category A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
F : C ⥤ D
hF : CoverPreserving J K F
G : D ⥤ A
hG : CoverPreserving K L G
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ GrothendieckTopology.sieves J U✝
⊢ Sieve.functorPushforward G (Sieve.functorPushforward F S✝) ∈ GrothendieckTopology.sieves L ((F ⋙ G).obj U✝)
exact hG.cover_preserve (hF.cover_preserve hS)