no goals
C : Type u
inst✝ : Category C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
hS : Covers J S f
hR : Covers J R f
⊢ Covers J (S ⊓ R) f
simpa [covers_iff] using And.intro hS hR