-- 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 : C
right : Discrete PUnit.{1}
s : Y ⟶ X
R : Sieve.{v, u} Y
hR : K.toCoverage.Saturate Y R
refine_1 :
  ∀ (Z : C) (S : Presieve.{v, u} Z) (hS : S ∈ K.toCoverage.coverings Z) (s : Z ⟶ X),
    Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }) (γ :=
      Set (Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s }))
      (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
        { left := Z, right := right, hom := s })
      ((Equiv.symm (Sieve.overEquiv { left := Z, right := right, hom := s }) :
            (a : Sieve (Over.left { left := Z, right := right, hom := s })) →
              Sieve { left := Z, right := right, hom := s })
          (Sieve.generate S) :
        Sieve (C := Over.{v, u} X) { left := Z, right := right, hom := s })
refine_1₁ :
  ∀ (X_1 : C) (s : X_1 ⟶ X),
    Membership.mem (γ := Set (Sieve (C := Over.{v, u} X) { left := X_1, right := right, hom := s }))
      (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
        { left := X_1, right := right, hom := s })
      ((Equiv.symm (Sieve.overEquiv { left := X_1, right := right, hom := s }) :
          (a : Sieve (Over.left { left := X_1, right := right, hom := s })) →
            Sieve { left := X_1, right := right, hom := s })
        ⊤)
refine_1₂ :
  ∀ (Y : C) (R S : Sieve.{v, u} Y) (hR : K.toCoverage.Saturate Y R)
    (H : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_1 (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_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
        R.arrows f →
          ∀ (s : Y_1 ⟶ X),
            Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y_1, right := right, hom := s }) (γ :=
              Set (Sieve (C := Over.{v, u} X) { left := Y_1, right := right, hom := s }))
              (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
                { left := Y_1, right := right, hom := s })
              ((Equiv.symm (Sieve.overEquiv { left := Y_1, right := right, hom := s }) :
                    (a : Sieve (Over.left { left := Y_1, right := right, hom := s })) →
                      Sieve { left := Y_1, right := right, hom := s })
                  (Sieve.pullback f S) :
                Sieve (C := Over.{v, u} X) { left := Y_1, right := right, hom := s }))
    (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 })
          S :
        Sieve (C := Over.{v, u} X) { left := Y, right := right, hom := s })
⊢ 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 })

Tactic:
induction hR with
    | of Z S hS =>
      rw [Sieve.overEquiv_symm_generate]
      exact .of _ _ (by simpa)
    | top =>
      rw [Sieve.overEquiv_symm_top]
      simp
    | transitive Y R S hR H ih ih' =>
      refine GrothendieckTopology.transitive _ (ih s) _ fun Z g hg ↦ ?_
      obtain rfl : right = Z.right := Subsingleton.elim _ _
      rw [← Sieve.overEquiv_symm_pullback]
      exact ih' hg Z.hom

Premises used: CategoryTheory.Sieve.overEquiv_symm_pullback, CategoryTheory.Sieve.overEquiv_symm_generate, CategoryTheory.Sieve.overEquiv_symm_top, Subsingleton.elim, rfl