-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
inst_3 : IsDenseSubsite J K G
inst_4 : IsEquivalence (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)
inst_5 : HasWeakSheafify.{v_1, v_4, u_1, u_4} J A
P : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
Q₁ Q₂ : Sheaf.{v_2, v_4, u_2, u_4} K A
f : obj (sheafifyOfIsEquivalence J K G A) P ⟶ Q₁
g : Q₁ ⟶ Q₂
this_1 : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : Adjunction (C := Sheaf.{v_1, v_4, u_1, u_4} J A)
  (Equivalence.functor (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K))))
  (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) :=
  Equivalence.toAdjunction (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))
adj₂ : Adjunction (C := Functor.{v_1, v_4, u_1, u_4} Cᵒᵖ A) (presheafToSheaf J A) (sheafToPresheaf J A) :=
  sheafificationAdjunction J A
⊢ Eq (α := P ⟶ Q₂.obj (P := Presheaf.IsSheaf K))
    ((IsCoverDense.restrictHomEquivHom : (a : G.op ⋙ P ⟶ G.op ⋙ Q₂.obj) → P ⟶ Q₂.obj)
        ((adj₂.homEquiv (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P)
                (obj (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) Q₁) :
              (a :
                  (presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P) ⟶
                    (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q₁) →
                ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P ⟶
                  (sheafToPresheaf J A).obj ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q₁))
            ((adj₁.homEquiv (obj (presheafToSheaf J A) (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P)) Q₁ :
                (a :
                    (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor.obj
                        ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P)) ⟶
                      Q₁) →
                  (presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P) ⟶
                    (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q₁)
              f) ≫
          map (sheafToPresheaf J A)
            (map (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) g)) :
      P ⟶ Q₂.obj (P := Presheaf.IsSheaf K))
    ((IsCoverDense.restrictHomEquivHom : (a : G.op ⋙ P ⟶ G.op ⋙ Q₁.obj) → P ⟶ Q₁.obj)
          ((adj₂.homEquiv (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P)
                (obj (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) Q₁) :
              (a :
                  (presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P) ⟶
                    (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q₁) →
                ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P ⟶
                  (sheafToPresheaf J A).obj ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q₁))
            ((adj₁.homEquiv (obj (presheafToSheaf J A) (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P)) Q₁ :
                (a :
                    (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor.obj
                        ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P)) ⟶
                      Q₁) →
                  (presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P) ⟶
                    (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q₁)
              f)) ≫
        g.hom :
      P ⟶ Q₂.obj (P := Presheaf.IsSheaf K))

Tactic:
apply IsCoverDense.restrictHomEquivHom_naturality_right

Premises used: CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_right