-- 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₂
simp :
  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))
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x.sieveExtend (R := R) f₁ h₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x.sieveExtend (R := R) f₂ h₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
simp only [FamilyOfElements.sieveExtend, ← comp_apply, ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Presieve.FamilyOfElements.sieveExtend, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp