-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
ℱ : Functor.{v_2, v, u_2, v + 1} Dᵒᵖ (Type v)
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
inst_2 : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
x : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))
this :
  ∀ {X Y : C} (i : X ⟶ Y) (x : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))),
    Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (G.map i).op) :
            (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y)))) →
              (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj X))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
                (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))) →
                  (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op Y)))
              x :
            (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y))) :
        (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op X)) :
            (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op X))) → (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op X)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map (G.map i).op) :
                (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y)))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X))))
              x :
            (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X)))) :
        (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op X)))
refine :
  ∀ (V : C) (iVX : V ⟶ X) (iVY : V ⟶ Y) (e : G.map iVY = G.map iVX ≫ i),
    Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (G.map iVX).op) :
            (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj X)))) →
              (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj V))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map i.op) :
                (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y)))) →
                  (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj X))))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
                    (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))) →
                      (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op Y)))
                  x :
                (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y))) :
            (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X)))) :
        (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (G.map iVX).op) :
            (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj X)))) →
              (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj V))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op X)) :
                (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op X))) →
                  (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op X)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map i.op) :
                    (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y)))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X))))
                  x :
                (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X)))) :
            (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op X))) :
        (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V))))
⊢ Eq (α := (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map i.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj Y)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj X))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op Y)) :
              (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op Y))) →
                (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op Y)))
            x :
          (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op Y))) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op X)) :
          (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op X))) → (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op X)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map i.op) :
              (a : (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj Y)))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X))))
            x :
          (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj X)))) :
      (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op X)))

Tactic:
refine IsLocallyFull.ext G _ i fun V iVX iVY e ↦ ?_

Premises used: CategoryTheory.Functor.IsLocallyFull.ext