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

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

Premises used: rfl