-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
U : Sieve.{v₁, u₁} X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve.{v₁, u₁} Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible (R := (Sieve.bind U.arrows B).arrows)
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows :=
  fun (Y : C) (f : Y ⟶ X) (hf : U.arrows f) (Z : C) (g : Z ⟶ Y) (hg : (B hf).arrows g) ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible (R := (B hf).arrows)
t : FamilyOfElements P U.arrows :=
  fun (Y : C) (f : Y ⟶ X) (hf : U.arrows f) ↦ ⋯.amalgamate (R := (B hf).arrows) (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (R := (B hf).arrows) (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
Y : C
l : Y ⟶ W
hl : (B ⋯).arrows l
apply :
  ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (Sieve.pullback (l ≫ h) (B hf)).arrows f_1 →
      Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f_1.op) :
              (a : (fun (X : Type u_1) ↦ X) (P.obj (op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map l.op) :
                  (a : (fun (X : Type u_1) ↦ X) (P.obj (op W))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
                (t (h ≫ f) ⋯) :
              (fun (X : Type u_1) ↦ X) (P.obj (op Y))) :
          (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f_1.op) :
              (a : (fun (X : Type u_1) ↦ X) (P.obj (op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map l.op) :
                  (a : (fun (X : Type u_1) ↦ X) (P.obj (op W))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map h.op) :
                      (a : (fun (X : Type u_1) ↦ X) (P.obj (op Z))) → (fun (X : Type u_1) ↦ X) (P.obj (op W)))
                    (t f hf) :
                  (fun (X : Type u_1) ↦ X) (P.obj (op W))) :
              (fun (X : Type u_1) ↦ X) (P.obj (op Y))) :
          (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map l.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (op W))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
        (t (h ≫ f) ⋯) :
      (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map l.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (op W))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map h.op) :
              (a : (fun (X : Type u_1) ↦ X) (P.obj (op Z))) → (fun (X : Type u_1) ↦ X) (P.obj (op W)))
            (t f hf) :
          (fun (X : Type u_1) ↦ X) (P.obj (op W))) :
      (fun (X : Type u_1) ↦ X) (P.obj (op Y)))

Tactic:
apply (hB' hf (l ≫ h)).ext

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.CategoryStruct.comp