-- 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
g : StructuredArrow (op (G.obj U)) G.op
I₁ 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) ⋯)
r : I₁.Relation I₂
apply : G.map (r.g₁ ≫ l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯) = G.map (r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯)
apply₁ :
  ∀ (V : C) (iUV : V ⟶ r.Z)
    (hiUV : iUV ≫ r.g₁ ≫ l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯ = iUV ≫ r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯),
    Eq (α := (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).map iUV.op) :
            (a : (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op r.Z))) →
              (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op V)))
          ((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)
              I₁ ≫
            Y.obj (P := Presheaf.IsSheaf J).map r.g₁.op) :
        (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).map iUV.op) :
            (a : (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op r.Z))) →
              (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op V)))
          ((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)
              I₂ ≫
            Y.obj (P := Presheaf.IsSheaf J).map r.g₂.op) :
        (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))
⊢ Eq (α := obj (obj (const (StructuredArrow (op (G.obj U)) G.op)) X) g ⟶ Y.obj (P := Presheaf.IsSheaf J).obj (op r.Z))
    ((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)
        I₁ ≫
      Y.obj (P := Presheaf.IsSheaf J).map r.g₁.op)
    ((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)
        I₂ ≫
      Y.obj (P := Presheaf.IsSheaf J).map r.g₂.op)

Tactic:
apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (r.g₁ ≫ l _ _ _ _ _ I₁.hf)
          (r.g₂ ≫ l _ _ _ _ _ I₂.hf) ?_)).isSeparatedFor.ext fun V iUV (hiUV : _ = _) ↦ ?_

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.IsDenseSubsite.equalizer_mem, CategoryTheory.GrothendieckTopology.Cover.Arrow.hf, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₁, CategoryTheory.CategoryStruct.comp, CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₂