-- 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 : 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))
    ((sheafifyHomEquivOfIsEquivalence J K G : (a : (sheafifyOfIsEquivalence J K G A).obj P ⟶ Q₂) → P ⟶ Q₂.obj) (f ≫ g) :
      P ⟶ Q₂.obj (P := Presheaf.IsSheaf K))
    ((sheafifyHomEquivOfIsEquivalence J K G : (a : (sheafifyOfIsEquivalence J K G A).obj P ⟶ Q₁) → P ⟶ Q₁.obj) f ≫
        g.hom :
      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₂)
          (f ≫ 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: change IsCoverDense.restrictHomEquivHom (adj₂.homEquiv _ _ (adj₁.homEquiv _ _ (f ≫ g))) =
    IsCoverDense.restrictHomEquivHom (adj₂.homEquiv _ _ (adj₁.homEquiv _ _ f)) ≫ g.hom