-- 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_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G'_1 : Subfunctor F_1
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : Sheaf.image f ⟶ G'
e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂
U : Cᵒᵖ
s : F'.obj (P := Presheaf.IsSheaf J).obj U
hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U
V : C
i : V ⟶ unop U
y : F.obj (P := Presheaf.IsSheaf J).obj (op V)
e' :
  Eq (α := F'.obj (P := Presheaf.IsSheaf J).obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op V)) :
          (a : (fun (X : Type w) ↦ X) (F.obj.obj (op V))) → (fun (X : Type w) ↦ X) (F'.obj.obj (op V)))
        y :
      (fun (X : Type w) ↦ X) (F'.obj (P := Presheaf.IsSheaf J).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.obj (P := Presheaf.IsSheaf J).map i.op) :
          (a : (fun (X : Type w) ↦ X) (F'.obj.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F'.obj.obj (op V)))
        s :
      (fun (X : Type w) ↦ X) (F'.obj (P := Presheaf.IsSheaf J).obj (op V)))
⊢ Eq (α := (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G'.obj (P := Presheaf.IsSheaf J).map i.op) :
          (a : (fun (X : Type w) ↦ X) (G'.obj.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (G'.obj.obj (op V)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (g₁.hom.app U)).toFun
          (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
            x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx)) :
      (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G'.obj (P := Presheaf.IsSheaf J).map i.op) :
          (a : (fun (X : Type w) ↦ X) (G'.obj.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (G'.obj.obj (op V)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (g₂.hom.app U)).toFun
          (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
            x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx)) :
      (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op V)))
have h : Eq (α := (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op V)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (g₁.hom.app (op (unop U)) ≫ G'.obj (P := Presheaf.IsSheaf J).map i.op) :
        (a : (fun (X : Type w) ↦ X) ((Sheaf.image f).obj.obj (op (unop U)))) →
          (fun (X : Type w) ↦ X) (G'.obj.obj (op V)))
      (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
        x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx) :
    (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op V)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (g₂.hom.app (op (unop U)) ≫ G'.obj (P := Presheaf.IsSheaf J).map i.op) :
        (a : (fun (X : Type w) ↦ X) ((Sheaf.image f).obj.obj (op (unop U)))) →
          (fun (X : Type w) ↦ X) (G'.obj.obj (op V)))
      (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
        x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx) :
    (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op V)))
Tactic: change (g₁.hom.app _ ≫ G'.obj.map _) _ = (g₂.hom.app _ ≫ G'.obj.map _) _