-- 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_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
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
have refine_1 : ∀
  (ih :
    ∀ (s : Y ⟶ X),
      Membership.mem (α := Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s }) (γ :=
        Set (Sieve (C := Over.{v, u} X) { left := Y, right := Z.right, hom := s }))
        (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
          { left := Y, right := Z.right, hom := s })
        ((Equiv.symm (Sieve.overEquiv { left := Y, right := Z.right, hom := s }) :
              (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
                Sieve { left := Y, right := Z.right, hom := s })
            R :
          Sieve (C := Over.{v, u} X) { left := Y, right := Z.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 := Z.right, hom := s }) (γ :=
            Set (Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s }))
            (((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a))
              { left := Y_2, right := Z.right, hom := s })
            ((Equiv.symm (Sieve.overEquiv { left := Y_2, right := Z.right, hom := s }) :
                  (a : Sieve (Over.left { left := Y_2, right := Z.right, hom := s })) →
                    Sieve { left := Y_2, right := Z.right, hom := s })
                (Sieve.pullback f S) :
              Sieve (C := Over.{v, u} X) { left := Y_2, right := Z.right, hom := s }))
  (g : Z ⟶ { left := Y, right := Z.right, hom := s })
  (hg :
    Sieve.arrows
      ((Equiv.symm (Sieve.overEquiv { left := Y, right := Z.right, hom := s }) :
          (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
            Sieve { left := Y, right := Z.right, hom := s })
        R)
      g),
  Sieve.pullback g
      ((Equiv.symm
            (Sieve.overEquiv
              { left := Y, right := Z.right, hom := s : Comma.{v, 0, v, u, 0, u} (𝟭 C) (Functor.fromPUnit X) }) :
          (a : Sieve (Over.left { left := Y, right := Z.right, hom := s })) →
            Sieve { left := Y, right := Z.right, hom := s })
        S) ∈
    ((Precoverage.comap (Over.forget X) K).toGrothendieck : (a : Over X) → Set (Sieve a)) Z
Tactic: obtain rfl : right = Z.right := Subsingleton.elim _ _
Cleared hypotheses: right, ih, ih', g, hg