-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
hx : x.Compatible (R := R)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : (generate R).arrows f₁
h₂ : (generate R).arrows f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
a :
  (g₁ ≫
        ⋯.choose (p :=
          fun (h : Y₁ ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁) ↦
          ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁ ⟶ X),
            R g ∧ h ≫ g = f₁)) ≫
      ⋯.choose (p := fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁ ⟶ X) ↦
        R g ∧
          ⋯.choose (p :=
                fun (h : Y₁ ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁) ↦
                ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁ ⟶ X),
                  R g ∧ h ≫ g = f₁) ≫
              g =
            f₁) =
    (g₂ ≫
        ⋯.choose (p :=
          fun (h : Y₂ ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂) ↦
          ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂ ⟶ X),
            R g ∧ h ≫ g = f₂)) ≫
      ⋯.choose (p := fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂ ⟶ X) ↦
        R g ∧
          ⋯.choose (p :=
                fun (h : Y₂ ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂) ↦
                ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂ ⟶ X),
                  R g ∧ h ≫ g = f₂) ≫
              g =
            f₂)
⊢ Eq (α := P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (P.map
              (g₁ ≫
                  ⋯.choose (p :=
                    fun (h : Y₁ ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁) ↦
                    ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁ ⟶ X),
                      R g ∧ h ≫ g = f₁)).op) :
          (a : P.obj (op (Exists.choose h₁))) → P.obj (op Z))
        (x
          (⋯.choose (p :=
            fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁ ⟶ X) ↦
            R g ∧
              ⋯.choose (p :=
                    fun (h : Y₁ ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁) ↦
                    ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁ ⟶ X),
                      R g ∧ h ≫ g = f₁) ≫
                  g =
                f₁))
          ⋯) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (P.map
              (g₂ ≫
                  ⋯.choose (p :=
                    fun (h : Y₂ ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂) ↦
                    ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂ ⟶ X),
                      R g ∧ h ≫ g = f₂)).op) :
          (a : P.obj (op (Exists.choose h₂))) → P.obj (op Z))
        (x
          (⋯.choose (p :=
            fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂ ⟶ X) ↦
            R g ∧
              ⋯.choose (p :=
                    fun (h : Y₂ ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂) ↦
                    ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂ ⟶ X),
                      R g ∧ h ≫ g = f₂) ≫
                  g =
                f₂))
          ⋯) :
      P.obj (op Z))

Tactic:
apply hx