-- Module: Mathlib.CategoryTheory.Sites.CoverLifting
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type w
inst_2 : Category.{w', w} A
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
inst_3 : G.IsCocontinuous J K
inst_4 : ∀ (F : Functor.{v_1, w', u_1, w} Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F
inst_5 : G.IsContinuous J K
inst_6 : HasWeakSheafify.{v_1, w', u_1, w} J A
inst_7 : HasWeakSheafify.{v_2, w', u_2, w} K A
F : Functor.{v_2, w', u_2, w} Dᵒᵖ A
adj₁ : Adjunction (C := Functor.{v_2, w', u_2, w} Dᵒᵖ A) (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) G.op.ran :=
  G.op.ranAdjunction A
adj₂ : Adjunction (C := Functor.{v_1, w', u_1, w} Cᵒᵖ A) (presheafToSheaf J A) (sheafToPresheaf J A) :=
  sheafificationAdjunction J A
adj₃ : Adjunction (C := Functor.{v_2, w', u_2, w} Dᵒᵖ A) (presheafToSheaf K A) (sheafToPresheaf K A) :=
  sheafificationAdjunction K A
adj₄ : Adjunction (C := Sheaf.{v_2, w', u_2, w} K A) (G.sheafPushforwardContinuous A J K)
  (G.sheafPushforwardCocontinuous A J K) :=
  G.sheafAdjunctionCocontinuous A J K
eq :
  Eq (α :=
    obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) F ⟶
      obj (sheafToPresheaf J A ⋙ G.op.ran) (obj (presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K) F))
    (adj₁.unit.app F ≫
      CategoryStruct.comp (Y :=
        obj ((obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ presheafToSheaf J A) ⋙ sheafToPresheaf J A ⋙ G.op.ran) F)
        (map G.op.ran (adj₂.unit.app (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) F)))
        (map G.op.ran (map (sheafToPresheaf J A) (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F))))
    (adj₃.unit.app F ≫ map (sheafToPresheaf K A) (adj₄.unit.app (obj (presheafToSheaf K A) F)))
a :
  Eq (α :=
    obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) F) ⟶
      obj (sheafToPresheaf J A) (obj (G.sheafPushforwardContinuous A J K) (obj (presheafToSheaf K A) F)))
    (map (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (adj₃.unit.app F) ≫
      map (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op)
          (map (sheafToPresheaf K A) (adj₄.unit.app (obj (presheafToSheaf K A) F))) ≫
        adj₁.counit.app
          (obj (sheafToPresheaf J A) (obj (G.sheafPushforwardContinuous A J K) (obj (presheafToSheaf K A) F))))
    (map (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (adj₃.unit.app F) ≫
      map (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (adj₁.unit.app (obj (presheafToSheaf K A ⋙ sheafToPresheaf K A) F)) ≫
        adj₁.counit.app
          (obj (sheafToPresheaf J A) (obj (G.sheafPushforwardContinuous A J K) (obj (presheafToSheaf K A) F))))
⊢ Eq (α :=
    obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) F) ⟶
      obj (sheafToPresheaf J A) (obj (G.sheafPushforwardContinuous A J K) (obj (presheafToSheaf K A) F)))
    ((Equiv.symm
            (adj₁.homEquiv (obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) F)
              (obj (sheafToPresheaf J A) (obj (G.sheafPushforwardContinuous A J K) (obj (presheafToSheaf K A) F)))) :
          (a :
              (𝟭 (Dᵒᵖ ⥤ A)).obj F ⟶
                G.op.ran.obj
                  ((sheafToPresheaf J A).obj
                    ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)))) →
            ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj ((𝟭 (Dᵒᵖ ⥤ A)).obj F) ⟶
              (sheafToPresheaf J A).obj ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)))
        (adj₃.unit.app F ≫ map (sheafToPresheaf K A) (adj₄.unit.app (obj (presheafToSheaf K A) F))) :
      obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) F) ⟶
        obj (sheafToPresheaf J A) (obj (G.sheafPushforwardContinuous A J K) (obj (presheafToSheaf K A) F)))
    ((Equiv.symm
            (adj₁.homEquiv (obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) F)
              (obj (sheafToPresheaf J A) (obj (G.sheafPushforwardContinuous A J K) (obj (presheafToSheaf K A) F)))) :
          (a :
              (𝟭 (Dᵒᵖ ⥤ A)).obj F ⟶
                G.op.ran.obj
                  ((sheafToPresheaf J A).obj
                    ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)))) →
            ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj ((𝟭 (Dᵒᵖ ⥤ A)).obj F) ⟶
              (sheafToPresheaf J A).obj ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)))
        ((adj₁.homEquiv F
              (obj (sheafToPresheaf J A) (obj (presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K) F)) :
            (a :
                ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F ⟶
                  (sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)) →
              F ⟶
                G.op.ran.obj
                  ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
          (map (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (adj₃.unit.app F))) :
      obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) (obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) F) ⟶
        obj (sheafToPresheaf J A) (obj (G.sheafPushforwardContinuous A J K) (obj (presheafToSheaf K A) F)))

Tactic:
simp only [Adjunction.homEquiv_counit, map_comp, Category.assoc,
    Adjunction.homEquiv_unit, Adjunction.unit_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Adjunction.unit_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.homEquiv_counit