-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
K : Precoverage.{v, u} C
inst_1 : K.HasPullbacks
inst_2 : K.IsStableUnderBaseChange
X Y_1 : C
right : Discrete PUnit.{1}
R_1 : Sieve.{v, u} Y_1
Y : C
R S : Sieve.{v, u} Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_2 (Sieve.pullback f S)
ih :
  ∀ (s : Y ⟶ X),
    Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
      Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
      (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
        { left := Y, right := right, hom := s })
      ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
            (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
              Sieve { left := Y, right := right, hom := s })
          R :
        Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })
ih' :
  ∀ ⦃Y_2 : C⦄ ⦃f : Y_2 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_2 ⟶ X),
        Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y_2, right := right, hom := s }) (γ :=
          Set (Sieve (C := Over.{v, u} X) { left := Y_2, right := right, hom := s }))
          (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
            { left := Y_2, right := right, hom := s })
          ((Equiv.symm (Sieve.overEquiv { left := Y_2, right := right, hom := s }) :
                (a : Sieve (Over.left { left := Y_2, right := right, hom := s })) →
                  Sieve { left := Y_2, right := right, hom := s })
              (Sieve.pullback f S) :
            Sieve (C := Over.{v, u} X) { left := Y_2, right := right, hom := s })
s : Y ⟶ X
refine_1 :
  ∀ (Z : Over.{v, u} X) (g : Z ⟶ { left := Y, right := right, hom := s })
    (hg :
      Sieve.arrows
        ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
            (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
              Sieve { left := Y, right := right, hom := s })
          R)
        g),
    Sieve.pullback g
        ((Equiv.symm
              (Sieve.overEquiv
                { left := Y, right := right, hom := s : Comma.{v, 0, v, u, 0, u} (𝟭 C) (Functor.fromPUnit X) }) :
            (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
              Sieve { left := Y, right := right, hom := s })
          S) ∈
      ((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a)) Z
⊢ Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }) (γ :=
    Set (Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s }))
    (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
      { left := Y, right := right, hom := s })
    ((Equiv.symm (Sieve.overEquiv { left := Y, right := right, hom := s }) :
          (a : Sieve (Over.left { left := Y, right := right, hom := s })) →
            Sieve { left := Y, right := right, hom := s })
        S :
      Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })

Tactic:
refine GrothendieckTopology.transitive _ (ih s) _ fun Z g hg ↦ ?_

Premises used: CategoryTheory.GrothendieckTopology.transitive