-- 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₁ P₂ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
f : P₁ ⟶ P₂
Q : Sheaf.{v_2, v_4, u_2, u_4} K A
g : obj (sheafifyOfIsEquivalence J K G A) P₂ ⟶ 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
rw :
  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)
            (map (sheafifyOfIsEquivalence J K G A) f ≫ g))) :
      P₁ ⟶ Q.obj (P := Presheaf.IsSheaf K))
    ((IsCoverDense.restrictHomEquivHom : (a : G.op ⋙ P₁ ⟶ G.op ⋙ Q.obj) → P₁ ⟶ Q.obj)
        (G.op.whiskerLeft f ≫
          (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)
              g)) :
      P₁ ⟶ Q.obj (P := Presheaf.IsSheaf K))
⊢ 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)
            (map (sheafifyOfIsEquivalence J K G A) f ≫ g))) :
      P₁ ⟶ Q.obj (P := Presheaf.IsSheaf K))
    (f ≫
        (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)
              g)) :
      P₁ ⟶ Q.obj (P := Presheaf.IsSheaf K))

Tactic:
rw [← IsCoverDense.restrictHomEquivHom_naturality_left]

Premises used: CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left