-- 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
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
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
⊢ 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

Tactic:
obtain rfl : right = Z.right := Subsingleton.elim _ _

Premises used: CategoryTheory.Comma.right, Subsingleton.elim, rfl