-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
P : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
a : S.functor ⟶ P
b : Functor.obj yoneda X ⟶ P
a_1 : Cᵒᵖ
⊢ (∀ (x : (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) (shrinkFunctor.{v₁, v₁, u₁} S)).obj a_1),
      Eq (α := P.obj a_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫
                    Iso.hom (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯) ≫ b)
                  a_1) :
              (a : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.obj a_1) → P.obj a_1)
            x :
          P.obj a_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((S.shrinkFunctorIsoFunctor.hom ≫ a).app a_1) :
              (a : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.obj a_1) → P.obj a_1)
            x :
          P.obj a_1)) ↔
    ∀ (x : S.functor.obj a_1),
      Eq (α := P.obj a_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((S.functorInclusion ≫ b).app a_1) :
              (a : S.functor.obj a_1) → P.obj a_1)
            x :
          P.obj a_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (a.app a_1) : (a : S.functor.obj a_1) → P.obj a_1) x : P.obj a_1)
have a₁ : (∀
    (x :
      { x : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) a_1 //
        S.arrows (Y := unop a_1)
          ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj a_1) → unop a_1 ⟶ X) x) }),
    Eq (α := P.obj a_1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (b.app a_1) : (a : unop a_1 ⟶ X) → P.obj a_1)
          ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj a_1) → unop a_1 ⟶ X)
              (↑x : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj a_1) :
            unop a_1 ⟶ X) :
        P.obj a_1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (a.app a_1) : (a : { g : unop a_1 ⟶ X // S.arrows g }) → P.obj a_1)
          ((Equiv.subtypeEquiv (p :=
                  Membership.mem (γ := Set (Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) a_1))
                    {f : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) a_1 |
                      S.arrows (Y := unop a_1)
                        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj a_1) → unop a_1 ⟶ X) f)})
                  (q := S.arrows) shrinkYonedaObjObjEquiv sorry :
                (a :
                    { x : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj a_1 //
                      S.arrows
                        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj a_1) → unop a_1 ⟶ X)
                          x) }) →
                  { g : unop a_1 ⟶ X // S.arrows g })
              x :
            { g : unop a_1 ⟶ X // S.arrows g }) :
        P.obj a_1)) ↔
  ∀ (x : { g : unop a_1 ⟶ X // S.arrows g }),
    Eq (α := P.obj a_1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (b.app a_1) : (a : unop a_1 ⟶ X) → P.obj a_1) (↑x : unop a_1 ⟶ X) :
        P.obj a_1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (a.app a_1) : (a : { g : unop a_1 ⟶ X // S.arrows g }) → P.obj a_1) x :
        P.obj a_1)
Tactic: dsimp [functor]