-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
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
⊢ Eq (α := P₁ ⟶ Q.obj (P := Presheaf.IsSheaf K))
    ((sheafifyHomEquivOfIsEquivalence J K G : (a : (sheafifyOfIsEquivalence J K G A).obj P₁ ⟶ Q) → P₁ ⟶ Q.obj)
        (map (sheafifyOfIsEquivalence J K G A) f ≫ g) :
      P₁ ⟶ Q.obj (P := Presheaf.IsSheaf K))
    (f ≫ (sheafifyHomEquivOfIsEquivalence J K G : (a : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q) → P₂ ⟶ Q.obj) g :
      P₁ ⟶ Q.obj (P := Presheaf.IsSheaf K))
have change : 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: change IsCoverDense.restrictHomEquivHom (adj₂.homEquiv _ _ (adj₁.homEquiv _ _
    ((sheafifyOfIsEquivalence J K G A).map f ≫ g))) =
      f ≫ IsCoverDense.restrictHomEquivHom (adj₂.homEquiv _ _ (adj₁.homEquiv _ _ g))