-- 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
W₁ : C
g₁ : unop (G.op.obj (op W₁)) ⟶ unop (op (G.obj U))
W₂ : C
g₂ : unop (G.op.obj (op W₂)) ⟶ unop (op (G.obj U))
i : Quiver.Hom (V := StructuredArrow (op (G.obj U)) G.op) (StructuredArrow.mk (op g₁)) (StructuredArrow.mk (op g₂))
refine_2 :
  ∀
    (i :
      Quiver.Hom.{v_1, u_1} (V := C)
        (unop
          (StructuredArrow.right.{v_1, v_2, u_1, u_2} (D := Dᵒᵖ) (S := op (G.obj U)) (T := G.op)
            (StructuredArrow.mk (op g₂))))
        (unop
          (StructuredArrow.right.{v_1, v_2, u_1, u_2} (D := Dᵒᵖ) (S := op (G.obj U)) (T := G.op)
            (StructuredArrow.mk (op g₁)))))
    (hi :
      StructuredArrow.hom (StructuredArrow.mk (op g₁)) ≫ G.op.map (op i) =
        StructuredArrow.hom (StructuredArrow.mk (op g₂))),
    Eq (α :=
      obj (C := StructuredArrow (op (G.obj U)) G.op) (obj (const (StructuredArrow (op (G.obj U)) G.op)) X)
          (StructuredArrow.mk (op g₁)) ⟶
        (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj (P := Presheaf.IsSheaf J)).obj (StructuredArrow.mk (op g₂)))
      (map (obj (const (StructuredArrow (op (G.obj U)) G.op)) X) (StructuredArrow.homMk (op i) hi) ≫
        (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)
                ⋯ :
              obj (obj (const (StructuredArrow (op (G.obj U)) G.op)) X) g ⟶
                Y.obj (P := Presheaf.IsSheaf J).obj (op (unop g.2))))
          (StructuredArrow.mk (op g₂)))
      ((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)
                ⋯ :
              obj (obj (const (StructuredArrow (op (G.obj U)) G.op)) X) g ⟶
                Y.obj (P := Presheaf.IsSheaf J).obj (op (unop g.2))))
          (StructuredArrow.mk (op g₁)) ≫
        (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj (P := Presheaf.IsSheaf J)).map
          (StructuredArrow.homMk (op i) hi))
⊢ Eq (α :=
    obj (C := StructuredArrow (op (G.obj U)) G.op) (obj (const (StructuredArrow (op (G.obj U)) G.op)) X)
        (StructuredArrow.mk (op g₁)) ⟶
      (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj (P := Presheaf.IsSheaf J)).obj (StructuredArrow.mk (op g₂)))
    (map (obj (const (StructuredArrow (op (G.obj U)) G.op)) X) i ≫
      (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)
              ⋯ :
            obj (obj (const (StructuredArrow (op (G.obj U)) G.op)) X) g ⟶
              Y.obj (P := Presheaf.IsSheaf J).obj (op (unop g.2))))
        (StructuredArrow.mk (op g₂)))
    ((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)
              ⋯ :
            obj (obj (const (StructuredArrow (op (G.obj U)) G.op)) X) g ⟶
              Y.obj (P := Presheaf.IsSheaf J).obj (op (unop g.2))))
        (StructuredArrow.mk (op g₁)) ≫
      (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj (P := Presheaf.IsSheaf J)).map i)

Tactic:
obtain ⟨⟨i⟩, hi, rfl⟩ := StructuredArrow.homMk_surjective i

Premises used: rfl, CategoryTheory.StructuredArrow.homMk_surjective