-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv (goal)
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₁ f₂ :
  obj (obj yoneda ((obj (G.op.ran ⋙ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U)))
    (op X)
e :
  Eq (α :=
    (fun (X : Type w') ↦ X)
      (obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U)))
        (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (map yoneda (NatTrans.app (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J))) (op U)))
              (op X)) :
          (a :
              (fun (X : Type w') ↦ X)
                ((yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X))) →
            (fun (X : Type w') ↦ X) ((yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)))
        f₁ :
      (fun (X : Type w') ↦ X)
        (obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U)))
          (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (map yoneda (NatTrans.app (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J))) (op U)))
              (op X)) :
          (a :
              (fun (X : Type w') ↦ X)
                ((yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X))) →
            (fun (X : Type w') ↦ X) ((yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)))
        f₂ :
      (fun (X : Type w') ↦ X)
        (obj (obj yoneda ((obj (𝟭 (Functor.{v_1, w', u_1, w} Cᵒᵖ A)) (Y.obj (P := Presheaf.IsSheaf J))).obj (op U)))
          (op X)))
W : C
g : G.obj W ⟶ G.obj U
V : C
iVW : V ⟶ W
h_1 : (G.imageSieve g).arrows iVW
iVU : V ⟶ U
h : G.map iVU = G.map iVW ≫ g
this :
  Eq (α := unop (op X) ⟶ Y.obj (P := Presheaf.IsSheaf J).obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (map yoneda (NatTrans.app (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J))) (op U)))
                (op X)) :
            (a :
                (fun (X : Type w') ↦ X)
                  ((yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X))) →
              (fun (X : Type w') ↦ X) ((yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)))
          f₁ ≫
        Y.obj (P := Presheaf.IsSheaf J).map iVU.op :
      unop (op X) ⟶ Y.obj (P := Presheaf.IsSheaf J).obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (map yoneda (NatTrans.app (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J))) (op U)))
                (op X)) :
            (a :
                (fun (X : Type w') ↦ X)
                  ((yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X))) →
              (fun (X : Type w') ↦ X) ((yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)))
          f₂ ≫
        Y.obj (P := Presheaf.IsSheaf J).map iVU.op :
      unop (op X) ⟶ Y.obj (P := Presheaf.IsSheaf J).obj (op V))
⊢ 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 iVW.op) :
          (a : (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op W))) →
            (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op V)))
        (f₁ ≫
          NatTrans.app
            (Limits.Cone.π
              ((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))))
            (StructuredArrow.mk (op g))) :
      (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 iVW.op) :
          (a : (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op W))) →
            (fun (X : Type w') ↦ X) ((Y.obj ⋙ coyoneda.obj (op X)).obj (op V)))
        (f₂ ≫
          NatTrans.app
            (Limits.Cone.π
              ((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))))
            (StructuredArrow.mk (op g))) :
      (fun (X : Type w') ↦ X) ((Y.obj (P := Presheaf.IsSheaf J) ⋙ obj coyoneda (op X)).obj (op V)))
have left : (f₁ ≫
      (obj G.op.ran (Y.obj (P := Presheaf.IsSheaf J))).map (op g) ≫
        NatTrans.app (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J))) (op W)) ≫
    Y.obj (P := Presheaf.IsSheaf J).map iVW.op =
  (f₂ ≫
      (obj G.op.ran (Y.obj (P := Presheaf.IsSheaf J))).map (op g) ≫
        NatTrans.app (NatTrans.app G.op.ranCounit (Y.obj (P := Presheaf.IsSheaf J))) (op W)) ≫
    Y.obj (P := Presheaf.IsSheaf J).map iVW.op
Tactic: dsimp at this ⊢