-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.CoverLifting (goal)
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
F : Sheaf.{v_2, w', u_2, w} K A
H : Sheaf.{v_1, w', u_1, w} J A
f : obj (G.sheafPushforwardContinuous A J K) F ⟶ H
erw :
  Eq (α :=
    F.obj (P := Presheaf.IsSheaf K) ⟶ (obj (G.sheafPushforwardCocontinuous A J K) H).obj (P := Presheaf.IsSheaf K))
    (CategoryStruct.comp (Y := obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K)))
      (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)) :
        obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) (F.obj (P := Presheaf.IsSheaf K)) ⟶
          obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ G.op.ran) (F.obj (P := Presheaf.IsSheaf K)))
      (𝟙 (obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K))) ≫
        map G.op.ran f.hom ≫ 𝟙 ((obj (G.sheafPushforwardCocontinuous A J K) H).obj (P := Presheaf.IsSheaf K))))
    ((Adjunction.homEquiv (G.op.ranAdjunction A) (F.obj (P := Presheaf.IsSheaf K)) (H.obj (P := Presheaf.IsSheaf J)) :
        (a : G.op ⋙ F.obj ⟶ H.obj) → F.obj ⟶ G.op.ran.obj H.obj)
      f.hom)
erw₁ :
  NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)) ≫
      𝟙 (obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K))) ≫ map G.op.ran f.hom =
    (Adjunction.homEquiv (G.op.ranAdjunction A) (F.obj (P := Presheaf.IsSheaf K)) (H.obj (P := Presheaf.IsSheaf J)) :
        (a : G.op ⋙ F.obj ⟶ H.obj) → F.obj ⟶ G.op.ran.obj H.obj)
      f.hom
⊢ Eq (α :=
    F.obj (P := Presheaf.IsSheaf K) ⟶ (obj (G.sheafPushforwardCocontinuous A J K) H).obj (P := Presheaf.IsSheaf K))
    (CategoryStruct.comp (Y := obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K)))
      (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)) :
        obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) (F.obj (P := Presheaf.IsSheaf K)) ⟶
          obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ G.op.ran) (F.obj (P := Presheaf.IsSheaf K)))
      (CategoryStruct.comp (Y :=
        obj G.op.ran ((obj (G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J)))
        (map G.op.ran (NatTrans.app (Iso.inv (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K)) F) :
          obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K)) ⟶
            obj G.op.ran ((obj (G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J)))
        (map G.op.ran f.hom ≫ 𝟙 ((obj (G.sheafPushforwardCocontinuous A J K) H).obj (P := Presheaf.IsSheaf K)) :
          obj G.op.ran ((obj (G.sheafPushforwardContinuous A J K) F).obj (P := Presheaf.IsSheaf J)) ⟶
            (obj (G.sheafPushforwardCocontinuous A J K) H).obj (P := Presheaf.IsSheaf K))))
    ((Adjunction.homEquiv (G.op.ranAdjunction A) (F.obj (P := Presheaf.IsSheaf K)) (H.obj (P := Presheaf.IsSheaf J)) :
        (a : G.op ⋙ F.obj ⟶ H.obj) → F.obj ⟶ G.op.ran.obj H.obj)
      f.hom)
have erw₂ : Eq (α := F.obj (P := Presheaf.IsSheaf K) ⟶ (obj (G.sheafPushforwardCocontinuous A J K) H).obj (P := Presheaf.IsSheaf K))
  (CategoryStruct.comp (Y := obj G.op.ran (G.op ⋙ F.obj (P := Presheaf.IsSheaf K)))
    (NatTrans.app (Adjunction.unit (G.op.ranAdjunction A)) (F.obj (P := Presheaf.IsSheaf K)) :
      obj (𝟭 (Functor.{v_2, w', u_2, w} Dᵒᵖ A)) (F.obj (P := Presheaf.IsSheaf K)) ⟶
        obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op ⋙ G.op.ran) (F.obj (P := Presheaf.IsSheaf K)))
    (map G.op.ran f.hom))
  ((Adjunction.homEquiv (G.op.ranAdjunction A) (F.obj (P := Presheaf.IsSheaf K)) (H.obj (P := Presheaf.IsSheaf J)) :
      (a : G.op ⋙ F.obj ⟶ H.obj) → F.obj ⟶ G.op.ran.obj H.obj)
    f.hom)
Tactic: erw [Functor.map_id, Category.comp_id, Category.id_comp,
          Adjunction.homEquiv_unit]