CoversTop in over-categories

This file contains a transitivity lemma for GrothendieckTopology.CoversTop: if a family X : I → C covers the top for J, and for each i a family Y i covers the top for the induced topology on Over (X i), then the combined family covers the top for J.

theorem CategoryTheory.GrothendieckTopology.CoversTop.over {C : Type u_1} [Category.{v_1, u_1} C] {J : GrothendieckTopology C} {I : Type u_2} {X : I → C} (hX : J.CoversTop X) {I' : I → Type u} {Y : (i : I) → I' i → Over (X i)} (hY : ∀ (i : I), (J.over (X i)).CoversTop (Y i)) : J.CoversTop fun (j : (i : I) × I' i) => (Y j.fst j.snd).left