-- 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)
this :
  ∀ {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₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      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)))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : coverByImage G X f₁
h₂ : coverByImage G X f₂
e : iZY₁ ≫ f₁ = iZY₂ ≫ f₂
l₁ : CoverByImageStructure G f₁
l₂ : CoverByImageStructure G f₂
obtain :
  ∀ (W₁ : C) (iYW₁ : Y₁ ⟶ G.obj W₁) (iWX₁ : G.obj W₁ ⟶ X) (h₁ : coverByImage G X (iYW₁ ≫ iWX₁))
    (e : iZY₁ ≫ iYW₁ ≫ iWX₁ = iZY₂ ≫ f₂),
    Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (ℱ'.obj (P := Presheaf.IsSheaf K).map
                (iZY₁ ≫
                    { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ :
                        CoverByImageStructure G (iYW₁ ≫ iWX₁) }.lift).op) :
            (a : ℱ'.obj.obj (op (G.obj { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.obj))) → ℱ'.obj.obj (op Z))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (α.app
                    (op { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ : CoverByImageStructure G (iYW₁ ≫ iWX₁) }.1)) :
                (a : (G.op ⋙ ℱ).obj (op { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.1)) →
                  (G.op ⋙ ℱ'.obj).obj (op { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.1))
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (ℱ.map
                        { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ :
                              CoverByImageStructure G (iYW₁ ≫ iWX₁) }.map.op) :
                    (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.obj)))
                  x :
                ℱ.obj
                  (op
                    (G.obj
                      { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ :
                          CoverByImageStructure G (iYW₁ ≫ iWX₁) }.obj))) :
            (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.1)) :
        ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (iZY₂ ≫ l₂.lift).op) :
            (a : ℱ'.obj.obj (op (G.obj l₂.obj))) → ℱ'.obj.obj (op Z))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op l₂.1)) :
                (a : (G.op ⋙ ℱ).obj (op l₂.1)) → (G.op ⋙ ℱ'.obj).obj (op l₂.1))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map l₂.map.op) :
                    (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj l₂.obj)))
                  x :
                ℱ.obj (op (G.obj l₂.obj))) :
            (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op l₂.1)) :
        ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z))
⊢ Eq (α := ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (iZY₁ ≫ l₁.lift).op) :
          (a : ℱ'.obj.obj (op (G.obj l₁.obj))) → ℱ'.obj.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op l₁.1)) :
              (a : (G.op ⋙ ℱ).obj (op l₁.1)) → (G.op ⋙ ℱ'.obj).obj (op l₁.1))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map l₁.map.op) :
                  (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj l₁.obj)))
                x :
              ℱ.obj (op (G.obj l₁.obj))) :
          (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op l₁.1)) :
      ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ'.obj (P := Presheaf.IsSheaf K).map (iZY₂ ≫ l₂.lift).op) :
          (a : ℱ'.obj.obj (op (G.obj l₂.obj))) → ℱ'.obj.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.app (op l₂.1)) :
              (a : (G.op ⋙ ℱ).obj (op l₂.1)) → (G.op ⋙ ℱ'.obj).obj (op l₂.1))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.map l₂.map.op) :
                  (a : ℱ.obj (op X)) → ℱ.obj (op (G.obj l₂.obj)))
                x :
              ℱ.obj (op (G.obj l₂.obj))) :
          (G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj (op l₂.1)) :
      ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Z))

Tactic:
obtain ⟨W₁, iYW₁, iWX₁, rfl⟩ := l₁

Premises used: rfl