-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Continuous (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))) F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
X : C
S : Sieve.{v₁, u₁} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
hWS :
  J.W (X :=
    Subfunctor.toFunctor (F := obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X)
      (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S))
    (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S))
this :
  K.W (X :=
    H.obj
      (Subfunctor.toFunctor (F := obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X)
        (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))
    (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))
e : H ⋙
    obj (whiskeringRight Dᵒᵖ (Type (max u₁ v₁ u₂ v₂)) (Type (max (max (max (max u₁ u₂) v₁) v₂) w)))
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} ≅
  obj (whiskeringRight Cᵒᵖ (Type (max u₁ v₁ u₂ v₂)) (Type (max (max (max (max u₁ u₂) v₁) v₂) w)))
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} ⋙
    H' :=
  uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂}.lanCompIsoOfPreserves F.op
⊢ Eq (α :=
    H'.obj
        (Subfunctor.toFunctor (F := obj shrinkYoneda.{max w u₁ v₁ u₂ v₂, v₁, u₁} X)
          (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S)) ⟶
      H.obj (obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X) ⋙ uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂})
    (Iso.hom
        (H'.mapIso (Iso.symm S.shrinkFunctorUliftFunctorIso) ≪≫
          Iso.symm
            (e.app
              (Subfunctor.toFunctor (F := obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X)
                (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))) ≫
      whiskerRight (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))
        uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂})
    (H'.map (Subfunctor.ι (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S)) ≫
      Iso.hom
        (H'.mapIso (Iso.symm (Iso.app shrinkYonedaUliftFunctorIso X)) ≪≫
          Iso.symm (e.app (obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X))))
have simp : Eq (α :=
  H'.obj
      (Subfunctor.toFunctor (F := obj shrinkYoneda.{max w u₁ v₁ u₂ v₂, v₁, u₁} X)
        (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S)) ⟶
    H.obj (obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X) ⋙ uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂})
  (H'.map (Iso.inv S.shrinkFunctorUliftFunctorIso) ≫
    e.inv.app
        (Subfunctor.toFunctor (F := obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X)
          (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)) ≫
      whiskerRight (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))
        uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂})
  (H'.map (Subfunctor.ι (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S)) ≫
    H'.map (NatTrans.app (Iso.inv shrinkYonedaUliftFunctorIso) X) ≫
      e.inv.app (obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X))
Tactic: simp only [Functor.mapIso_symm, Functor.comp_obj, Functor.whiskeringRight_obj_obj,
          Iso.trans_hom, Iso.symm_hom, Functor.mapIso_inv, Iso.app_inv, Category.assoc]