-- 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)))
        x :
      (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)))
have 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 sorry ≫ G.sheafifyLift (homOfLe h) hG') :
    F.obj (op V))
Tactic: convert! this.symm