-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type w
inst_2 : Category.{w', w} A
inst_3 : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst_4 : IsDenseSubsite J K G
Y : Sheaf.{v_1, w', u_1, w} J A
U : C
X : A
f : obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U))) (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (hf : (G.imageSieve g).arrows f) → X ⟶ Z
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
c : Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj (P := Presheaf.IsSheaf J)) :=
  { pt := X,
    π :=
      {
        app := fun (g : StructuredArrow (op (G.obj U)) G.op) ↦
          ⋯.amalgamate
            (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (C := C) (unop g.2)) ↦
              Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (unop g.2)))
                ((J : (a : C) → Set (Sieve a)) (unop g.2)) S)
              (G.imageSieve g.hom.unop) ⋯)
            (fun
                (I :
                  GrothendieckTopology.Cover.Arrow
                    (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (C := C) (unop g.2)) ↦
                      Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (unop g.2)))
                        ((J : (a : C) → Set (Sieve a)) (unop g.2)) S)
                      (G.imageSieve g.hom.unop) ⋯)) ↦
              f ≫ Y.obj (P := Presheaf.IsSheaf J).map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op)
            ⋯,
        naturality := ⋯ } }
this :
  CategoryStruct.comp (Y := (obj G.op.ran (Y.obj (P := Presheaf.IsSheaf J))).obj (op (G.obj U)))
      (Limits.IsLimit.lift (G.op.isPointwiseRightKanExtensionRanCounit (Y.obj (P := Presheaf.IsSheaf J)) (op (G.obj U)))
          c :
        c.pt ⟶
          Limits.Cone.pt (J := StructuredArrow (op (G.obj U)) G.op)
            ((RightExtension.mk (obj G.op.ran (Y.obj (P := Presheaf.IsSheaf J)))
                  (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J)))).coneAt
              (op (G.obj U))))
      (NatTrans.app (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J))) (op U)) =
    c.π.app (StructuredArrow.mk (𝟙 (op (G.obj U))))
apply :
  ∀
    (I :
      GrothendieckTopology.Cover.Arrow
        (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} U) ↦ S ∈ (J : (a : C) → Set (Sieve a)) U)
          (G.imageSieve (𝟙 (G.obj U))) ⋯)),
    ⋯.amalgamate
          (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (C := C) (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)) ↦
            Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)))
              ((J : (a : C) → Set (Sieve a)) (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)) S)
            (G.imageSieve (V := U) (Quiver.Hom.unop (StructuredArrow.hom (StructuredArrow.mk (𝟙 (op (G.obj U))))))) ⋯)
          (fun
              (I :
                GrothendieckTopology.Cover.Arrow (X := unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)
                  (Subtype.mk (p :=
                    fun (S : Sieve.{v_1, u_1} (C := C) (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)) ↦
                    Membership.mem (γ :=
                      Set (Sieve.{v_1, u_1} (C := C) (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)))
                      ((J : (a : C) → Set (Sieve a)) (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)) S)
                    (G.imageSieve (V := U)
                      (Quiver.Hom.unop (StructuredArrow.hom (StructuredArrow.mk (𝟙 (op (G.obj U)))))))
                    ⋯)) ↦
            f ≫
              Y.obj (P := Presheaf.IsSheaf J).map
                (l I.Y (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2) U I.f
                    (Quiver.Hom.unop (StructuredArrow.hom (StructuredArrow.mk (𝟙 (op (G.obj U)))))) ⋯).op)
          ⋯ ≫
        Y.obj (P := Presheaf.IsSheaf J).map I.f.op =
      f ≫ Y.obj (P := Presheaf.IsSheaf J).map I.f.op
⊢ ⋯.amalgamate
      (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (C := C) (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)) ↦
        Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)))
          ((J : (a : C) → Set (Sieve a)) (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)) S)
        (G.imageSieve (V := U) (Quiver.Hom.unop (StructuredArrow.hom (StructuredArrow.mk (𝟙 (op (G.obj U))))))) ⋯)
      (fun
          (I :
            GrothendieckTopology.Cover.Arrow (X := unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)
              (Subtype.mk (p := fun (S : Sieve.{v_1, u_1} (C := C) (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)) ↦
                Membership.mem (γ := Set (Sieve.{v_1, u_1} (C := C) (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)))
                  ((J : (a : C) → Set (Sieve a)) (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2)) S)
                (G.imageSieve (V := U) (Quiver.Hom.unop (StructuredArrow.hom (StructuredArrow.mk (𝟙 (op (G.obj U)))))))
                ⋯)) ↦
        f ≫
          Y.obj (P := Presheaf.IsSheaf J).map
            (l I.Y (unop (StructuredArrow.mk (𝟙 (op (G.obj U)))).2) U I.f
                (Quiver.Hom.unop (StructuredArrow.hom (StructuredArrow.mk (𝟙 (op (G.obj U)))))) ⋯).op)
      ⋯ =
    f

Tactic:
apply Y.2.hom_ext ⟨_, IsDenseSubsite.imageSieve_mem J K G (𝟙 (G.obj U))⟩ _ _ fun I ↦ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.CategoryStruct.id, Subtype.mk, CategoryTheory.Presheaf.IsSheaf.hom_ext, CategoryTheory.Functor.obj, CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem