-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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))
⊢ 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)))
have 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))
Tactic: rwa [← NatTrans.naturality_apply, ← NatTrans.naturality_apply, h]