-- 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
trans :
  Eq (α :=
    obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P₁ ⟶
      obj (sheafToPresheaf J A)
        (obj (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) Q))
    ((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)) :
      obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P₁ ⟶
        obj (sheafToPresheaf J A)
          (obj (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) Q))
    ((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))
        (map (presheafToSheaf J A) (G.op.whiskerLeft f) ≫
          (adj₁.homEquiv (obj (presheafToSheaf J A) (G.op ⋙ P₂)) Q :
              (a :
                  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor.obj
                      ((presheafToSheaf J A).obj (G.op ⋙ P₂)) ⟶
                    Q) →
                (presheafToSheaf J A).obj (G.op ⋙ P₂) ⟶
                  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q)
            g) :
      obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P₁ ⟶
        obj (sheafToPresheaf J A)
          (obj (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) Q))
trans₁ :
  Eq (α :=
    obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P₁ ⟶
      obj (sheafToPresheaf J A)
        (obj (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) Q))
    ((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))
        (map (presheafToSheaf J A) (G.op.whiskerLeft f) ≫
          (adj₁.homEquiv (obj (presheafToSheaf J A) (G.op ⋙ P₂)) Q :
              (a :
                  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor.obj
                      ((presheafToSheaf J A).obj (G.op ⋙ P₂)) ⟶
                    Q) →
                (presheafToSheaf J A).obj (G.op ⋙ P₂) ⟶
                  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q)
            g) :
      obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P₁ ⟶
        obj (sheafToPresheaf J A)
          (obj (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) Q))
    (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) :
      G.op ⋙ P₁ ⟶ G.op ⋙ Q.obj (P := Presheaf.IsSheaf K))
⊢ Eq (α := G.op ⋙ P₁ ⟶ G.op ⋙ Q.obj (P := Presheaf.IsSheaf K))
    ((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)) :
      obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P₁ ⟶
        obj (sheafToPresheaf J A)
          (obj (Equivalence.inverse (Equivalence.symm (asEquivalence (G.sheafPushforwardContinuous A J K)))) Q))
    (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) :
      G.op ⋙ P₁ ⟶ G.op ⋙ Q.obj (P := Presheaf.IsSheaf K))

Tactic:
trans adj₂.homEquiv _ _ ((presheafToSheaf J A).map (G.op.whiskerLeft f) ≫
    (adj₁.homEquiv _ _) g)

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.whiskerLeft, CategoryTheory.presheafToSheaf, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Adjunction.homEquiv, DFunLike.coe