∀ {C : Type u_6} [inst : CategoryTheory.Category.{u_5, u_6} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_1}
  [inst_2 : CategoryTheory.Category.{u_2, u_1} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val) (U V : Dᵒᵖ) (i : U ⟶ V),
  CategoryTheory.CategoryStruct.comp ((ℱ.comp CategoryTheory.yoneda).map i)
      (let α_1 := CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom α;
      { app := fun X => (α_1.app X).app V, naturality := ⋯ }) =
    CategoryTheory.CategoryStruct.comp
      (let α_1 := CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom α;
      { app := fun X => (α_1.app X).app U, naturality := ⋯ })
      ((ℱ'.val.comp CategoryTheory.yoneda).map i)