-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₂
⊢ 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))
have a : (g₁ ≫
      sorry.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₁)) ≫
    sorry.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 ∧
        sorry.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₂ ≫
      sorry.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₂)) ≫
    sorry.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 ∧
        sorry.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₂)
Tactic: apply hx