-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
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ᵒᵖ
a₁ :
  (∀ (b_1 : unop a_1 ⟶ X) (b_2 : S.arrows b_1),
      Eq (α := P.obj a_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (b.app a_1) : (a : unop a_1 ⟶ X) → P.obj a_1) b_1 : 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 ⋯ :
                  (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 })
                (Subtype.mk (p := fun (a : 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) a))
                  ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop a_1 ⟶ X) → (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj a_1)
                    b_1)
                  ⋯) :
              { g : unop a_1 ⟶ X // S.arrows g }) :
          P.obj a_1)) ↔
    ∀ (a_2 : unop a_1 ⟶ X) (b_1 : S.arrows a_2),
      Eq (α := P.obj a_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (b.app a_1) : (a : unop a_1 ⟶ X) → P.obj a_1) a_2 : 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)
            (Subtype.mk (p := fun (a : unop a_1 ⟶ X) ↦ S.arrows a) a_2 b_1) :
          P.obj a_1)
⊢ (∀
      (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 ⋯ :
                  (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:
simp only [Subtype.forall, shrinkYonedaObjObjEquiv.forall_congr_left, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Equiv.forall_congr_left, Subtype.forall, CategoryTheory.shrinkYonedaObjObjEquiv