-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : PullbackCompatible P π x
i j : I
Z : C
gi : Z ⟶ X i
gj : Z ⟶ X j
comm : gi ≫ π i = gj ≫ π j
refine_2 :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (P.map
              (CategoryStruct.comp (Y := Limits.pullback (π i) (π j)) (pullback.lift gi gj comm)
                  (pullback.fst (π i) (π j))).op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X i)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x i) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
refine_2₁ :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (P.map
              (CategoryStruct.comp (Y := op (Limits.pullback (π i) (π j))) (Quiver.Hom.op (pullback.fst (π i) (π j)))
                (Quiver.Hom.op (pullback.lift gi gj comm)))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X i)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x i) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
refine_2₂ :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := P.obj (op (Limits.pullback (π i) (π j))))
              (P.map (Quiver.Hom.op (pullback.fst (π i) (π j)))) (P.map (Quiver.Hom.op (pullback.lift gi gj comm)))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X i)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x i) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
refine_2₃ :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.lift gi gj comm))) :
          (a : P.obj (op (Limits.pullback (π i) (π j)))) → P.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst (π i) (π j)))) :
              (a : P.obj (op (X i))) → P.obj (op (Limits.pullback (π i) (π j))))
            (x i) :
          P.obj (op (Limits.pullback (π i) (π j)))) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
refine_2₄ :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.lift gi gj comm))) :
          (a : P.obj (op (Limits.pullback (π i) (π j)))) → P.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd (π i) (π j)))) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) →
                (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
            (x j) :
          (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j))))) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
refine_2₅ :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := P.obj (op (Limits.pullback (π i) (π j))))
              (P.map (Quiver.Hom.op (pullback.snd (π i) (π j)))) (P.map (Quiver.Hom.op (pullback.lift gi gj comm)))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → P.obj (op Z))
        (x j) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
refine_2₆ :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (P.map
              (CategoryStruct.comp (Y := op (Limits.pullback (π i) (π j))) (Quiver.Hom.op (pullback.snd (π i) (π j)))
                (Quiver.Hom.op (pullback.lift gi gj comm)))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → P.obj (op Z))
        (x j) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
refine_2₇ :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (P.map
              (CategoryStruct.comp (Y := Limits.pullback (π i) (π j)) (pullback.lift gi gj comm)
                  (pullback.snd (π i) (π j))).op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → P.obj (op Z))
        (x j) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
refine_2₈ refine_2₉ :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → P.obj (op Z))
        (x j) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gi.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X i)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x i) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map gj.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x j) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
rw [← pullback.lift_fst _ _ comm, op_comp, Functor.map_comp, comp_apply, t i j,
      ← comp_apply, ← Functor.map_comp, ← op_comp, pullback.lift_snd]

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pullback.lift_fst