-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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 })
        ⊤)
⊢ 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 })
have 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 })
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
Cleared hypotheses: s, hR