-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible (R := R)
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
rwa :
  Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : P.obj (op W)) → Q.obj (op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) : (a : P.obj (op Z₁)) → P.obj (op W)) (x f₁ h₁) :
          P.obj (op W)) :
      Q.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Q.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (Q.obj (op Z₂))) → (fun (X : Type w) ↦ X) (Q.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Z₂)) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op Z₂))) → (fun (X : Type w) ↦ X) (Q.obj (op Z₂)))
            (x f₂ h₂) :
          (fun (X : Type w) ↦ X) (Q.obj (op Z₂))) :
      (fun (X : Type w) ↦ X) (Q.obj (op W)))
rwa₁ :
  Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : P.obj (op W)) → Q.obj (op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) : (a : P.obj (op Z₁)) → P.obj (op W)) (x f₁ h₁) :
          P.obj (op W)) :
      Q.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : P.obj (op W)) → Q.obj (op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) : (a : P.obj (op Z₂)) → P.obj (op W)) (x f₂ h₂) :
          P.obj (op W)) :
      Q.obj (op W))
rwa₂ :
  Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : P.obj (op W)) → Q.obj (op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op Z₂))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
            (x f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op W))) :
      Q.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : P.obj (op W)) → Q.obj (op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) : (a : P.obj (op Z₂)) → P.obj (op W)) (x f₂ h₂) :
          P.obj (op W)) :
      Q.obj (op W))
Y₂ : C
g₃ : W ⟶ Z₂
f₃ : Z₂ ⟶ X
h₃ : R f₂
a : g₁ ≫ f₁ = g₂ ≫ f₂
rwa₃ :
  Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : P.obj (op W)) → Q.obj (op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op Z₂))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
            (x f₂ h₂) :
          (fun (X : Type w) ↦ X) (P.obj (op W))) :
      Q.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : P.obj (op W)) → Q.obj (op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) : (a : P.obj (op Z₂)) → P.obj (op W)) (x f₂ h₂) :
          P.obj (op W)) :
      Q.obj (op W))
Y₃ : C
g₄ : W ⟶ Z₂
f₄ : Z₂ ⟶ X
h₄ : R f₂
a₁ a₂ a₃ : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq (α := (fun (X : Type w) ↦ X) (Q.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Q.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (Q.obj (op Z₁))) → (fun (X : Type w) ↦ X) (Q.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Z₁)) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op Z₁))) → (fun (X : Type w) ↦ X) (Q.obj (op Z₁)))
            (x f₁ h₁) :
          (fun (X : Type w) ↦ X) (Q.obj (op Z₁))) :
      (fun (X : Type w) ↦ X) (Q.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Q.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (Q.obj (op Z₂))) → (fun (X : Type w) ↦ X) (Q.obj (op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Z₂)) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op Z₂))) → (fun (X : Type w) ↦ X) (Q.obj (op Z₂)))
            (x f₂ h₂) :
          (fun (X : Type w) ↦ X) (Q.obj (op Z₂))) :
      (fun (X : Type w) ↦ X) (Q.obj (op W)))

Tactic:
rwa [← NatTrans.naturality_apply, ← NatTrans.naturality_apply, h]

Premises used: CategoryTheory.NatTrans.naturality_apply