-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
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)))
E :
  Eq (α := (fun (X : Type w) ↦ X) ((Sheaf.image f).obj (P := Presheaf.IsSheaf J).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Sheaf.toImage f).hom.app (op V)) :
          (a : (fun (X : Type w) ↦ X) (F.obj.obj (op V))) → (fun (X : Type w) ↦ X) ((Sheaf.image f).obj.obj (op V)))
        y :
      (fun (X : Type w) ↦ X) ((Sheaf.image f).obj (P := Presheaf.IsSheaf J).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Sheaf.image f).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) ((Sheaf.image f).obj.obj (op V)))
        (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj (op (unop U))) ↦
          Membership.mem (γ := Set (F'.obj (P := Presheaf.IsSheaf J).obj (op (unop U))))
            ((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op (unop U))) x)
          s hx) :
      (fun (X : Type w) ↦ X) ((Sheaf.image f).obj (P := Presheaf.IsSheaf J).obj (op V)))
this :
  Eq.{w + 1} (α := (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op V)))
    ((fun (f : F ⟶ G') ↦
        ((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) (G'.obj.obj (op V)))
            y :
          (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op V))))
      (Sheaf.toImage f ≫ g₁))
    ((fun (f : F ⟶ G') ↦
        ((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) (G'.obj.obj (op V)))
            y :
          (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op V))))
      (Sheaf.toImage f ≫ g₂))
h :
  ∀
    (this :
      Eq (α := G'.obj (P := Presheaf.IsSheaf J).obj (op V))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (g₁.hom.app (op V)) :
              (a : (↑((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) : Type w)) → G'.obj.obj (op V))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subfunctor.toRangeSheafify J f.hom).app (op V)) :
                  (a : F.obj.obj (op V)) → (↑((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) : Type w))
                y :
              (↑((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) : Type w)) :
          G'.obj (P := Presheaf.IsSheaf J).obj (op V))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (g₂.hom.app (op V)) :
              (a : (↑((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) : Type w)) → G'.obj.obj (op V))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subfunctor.toRangeSheafify J f.hom).app (op V)) :
                  (a : F.obj.obj (op V)) → (↑((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) : Type w))
                y :
              (↑((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) : Type w)) :
          G'.obj (P := Presheaf.IsSheaf J).obj (op V)))
    (E :
      Eq (α := F'.obj (P := Presheaf.IsSheaf J).obj (op V))
        ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subfunctor.toRangeSheafify J f.hom).app (op V)) :
                  (a : F.obj.obj (op V)) → (↑((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) : Type w))
                y) :
            F'.obj (P := Presheaf.IsSheaf J).obj (op V)) :
          F'.obj (P := Presheaf.IsSheaf J).obj (op V))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.obj (P := Presheaf.IsSheaf J).map i.op) :
              (a : F'.obj.obj U) → F'.obj.obj (op V))
            s :
          F'.obj (P := Presheaf.IsSheaf J).obj (op V))),
    Eq (α := G'.obj (P := Presheaf.IsSheaf J).obj (op V))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (g₁.hom.app (op V)) :
            (a : (↑((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) : Type w)) → G'.obj.obj (op V))
          (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj (op V)) ↦
              Membership.mem (γ := Set (F'.obj (P := Presheaf.IsSheaf J).obj (op V)))
                ((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) x)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.obj (P := Presheaf.IsSheaf J).map i.op) :
                  (a : F'.obj.obj U) → F'.obj.obj (op V))
                s)
              ⋯ :
            { x : F'.obj (P := Presheaf.IsSheaf J).obj (op V) //
              Membership.mem (γ := Set (F'.obj (P := Presheaf.IsSheaf J).obj (op V)))
                ((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) x }) :
        G'.obj (P := Presheaf.IsSheaf J).obj (op V))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (g₂.hom.app (op V)) :
            (a : (↑((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) : Type w)) → G'.obj.obj (op V))
          (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj (op V)) ↦
              Membership.mem (γ := Set (F'.obj (P := Presheaf.IsSheaf J).obj (op V)))
                ((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) x)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.obj (P := Presheaf.IsSheaf J).map i.op) :
                  (a : F'.obj.obj U) → F'.obj.obj (op V))
                s)
              ⋯ :
            { x : F'.obj (P := Presheaf.IsSheaf J).obj (op V) //
              Membership.mem (γ := Set (F'.obj (P := Presheaf.IsSheaf J).obj (op V)))
                ((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op V)) x }) :
        G'.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)
            ((Sheaf.image f).obj (P := Presheaf.IsSheaf J).map i.op ≫ g₁.hom.app (op V)) :
          (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)
            ((Sheaf.image f).obj (P := Presheaf.IsSheaf J).map i.op ≫ g₂.hom.app (op V)) :
          (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:
simp only [ObjectProperty.FullSubcategory.comp_hom, Sheaf.image_obj, Sheaf.toImage_hom,
    NatTrans.comp_app, Subfunctor.toFunctor_obj, comp_apply, op_unop, Subfunctor.toFunctor_map,
    ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, Subtype.ext_iff] at this E ⊢

Premises used: CategoryTheory.Subfunctor.toFunctor_obj, Opposite.op_unop, TypeCat.Fun.coe_mk, CategoryTheory.Sheaf.toImage_hom, CategoryTheory.Sheaf.image_obj, CategoryTheory.Subfunctor.toFunctor_map, Subtype.ext_iff, CategoryTheory.comp_apply, CategoryTheory.ObjectProperty.FullSubcategory.comp_hom, CategoryTheory.NatTrans.comp_app, CategoryTheory.ConcreteCategory.hom_ofHom