-- 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.IsCoverDense K
inst_3 : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Z : D
W₁ W₂ : C
iWX₁ : G.obj W₁ ⟶ X
iWX₂ : G.obj W₂ ⟶ X
iZW₁ : Z ⟶ G.obj W₁
iZW₂ : Z ⟶ G.obj W₂
e : iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂
refine :
  ∀ (V : C) (iVZ : G.obj V ⟶ Z),
    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 iVZ.op) :
            (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj V))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map iZW₁.op) :
                (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj W₁)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op W₁)) :
                    (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op W₁))) →
                      (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op W₁)))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map iWX₁.op) :
                        (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₁))))
                      x :
                    (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₁)))) :
                (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op W₁))) :
            (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z))) :
        (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 iVZ.op) :
            (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj V))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map iZW₂.op) :
                (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj W₂)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op W₂)) :
                    (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op W₂))) →
                      (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op W₂)))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map iWX₂.op) :
                        (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₂))))
                      x :
                    (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₂)))) :
                (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op W₂))) :
            (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z))) :
        (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 Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map iZW₁.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj W₁)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op W₁)) :
              (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op W₁))) →
                (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op W₁)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map iWX₁.op) :
                  (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₁))))
                x :
              (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₁)))) :
          (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op W₁))) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map iZW₂.op) :
          (a : (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op (G.obj W₂)))) → (fun (X : Type v) ↦ X) (ℱ'.obj.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op W₂)) :
              (a : (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ).obj (op W₂))) →
                (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj).obj (op W₂)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map iWX₂.op) :
                  (a : (fun (X : Type v) ↦ X) (ℱ.obj (op X))) → (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₂))))
                x :
              (fun (X : Type v) ↦ X) (ℱ.obj (op (G.obj W₂)))) :
          (fun (X : Type v) ↦ X) ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op W₂))) :
      (fun (X : Type v) ↦ X) (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z)))

Tactic:
refine ext G _ _ fun V iVZ ↦ ?_

Premises used: CategoryTheory.Functor.IsCoverDense.ext