-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf.{w, v, u} J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection x).arrows i
this :
  Eq.{w + 1} (α := F.obj (op V))
    ((fun (f : G.toFunctor ⟶ G'.toFunctor) ↦
        ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op V)) :
                  (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op V))) →
                    (fun (X : Type w) ↦ X) (G'.toFunctor.obj (op V)))
                (Subtype.mk (p := fun (x : F.obj (op V)) ↦ Membership.mem (γ := Set (F.obj (op V))) (G.obj (op V)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
                      (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
                    x)
                  hi)) :
            F.obj (op V)) :
          F.obj (op V)))
      (homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG'))
    ((fun (f : G.toFunctor ⟶ G'.toFunctor) ↦
        ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op V)) :
                  (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op V))) →
                    (fun (X : Type w) ↦ X) (G'.toFunctor.obj (op V)))
                (Subtype.mk (p := fun (x : F.obj (op V)) ↦ Membership.mem (γ := Set (F.obj (op V))) (G.obj (op V)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
                      (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
                    x)
                  hi)) :
            F.obj (op V)) :
          F.obj (op V)))
      (homOfLe h))
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
        (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.sheafifyLift (homOfLe h) hG').app U) :
                (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) →
                  (fun (X : Type w) ↦ X) (G'.toFunctor.obj U))
              (Subtype.mk (p := fun (x : F.obj U) ↦ x ∈ (sheafify J G).obj U) x hx)) :
          F.obj U) :
      (fun (X : Type w) ↦ X) (F.obj (op V)))
    ((fun (f : G.toFunctor ⟶ G'.toFunctor) ↦
          ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op V)) :
                    (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op V))) →
                      (fun (X : Type w) ↦ X) (G'.toFunctor.obj (op V)))
                  (Subtype.mk (p := fun (x : F.obj (op V)) ↦ Membership.mem (γ := Set (F.obj (op V))) (G.obj (op V)) x)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
                        (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
                      x)
                    hi)) :
              F.obj (op V)) :
            F.obj (op V)))
        (homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG') :
      F.obj (op V))
have h₁ : Eq.{w + 1} (α := (fun (X : Type w) ↦ X) (F.obj (op V)))
  (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.sheafifyLift (homOfLe h) hG').app (op V)) :
          (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj (op V))) →
            (fun (X : Type w) ↦ X) (G'.toFunctor.obj (op V)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((sheafify J G).toFunctor.map i.op) :
            (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj (op (unop U)))) →
              (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj (op V)))
          (Subtype.mk (p := fun (x : F.obj U) ↦ x ∈ (sheafify J G).obj U) x hx))) :
    F.obj (op V))
  ((fun (f : G.toFunctor ⟶ G'.toFunctor) ↦
      ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op V)) :
                (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op V))) →
                  (fun (X : Type w) ↦ X) (G'.toFunctor.obj (op V)))
              (Subtype.mk (p := fun (x : F.obj (op V)) ↦ Membership.mem (γ := Set (F.obj (op V))) (G.obj (op V)) x)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
                    (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
                  x)
                hi)) :
          F.obj (op V)) :
        F.obj (op V)))
    (homOfLe sorry ≫ G.sheafifyLift (homOfLe h) hG'))
Tactic: rw [← Subfunctor.nat_trans_naturality]