-- Module: Mathlib.CategoryTheory.Sites.Continuous
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
iso : Arrow.mk (X :=
    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'.map (Subfunctor.ι (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S))) ≅
  Arrow.mk (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)) ⋙
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂})
    (whiskerRight (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂}) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
rw :
  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)) ⋙
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂})
    (whiskerRight (H.map (Subfunctor.ι (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S)))
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂})
⊢ K.W (X :=
    H'.obj
      (Subfunctor.toFunctor (F := obj shrinkYoneda.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} X)
        (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S)))
    (H'.map (Subfunctor.ι (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S)))

Tactic:
rw [K.W.arrow_mk_iso_iff iso]

Premises used: CategoryTheory.GrothendieckTopology.W, CategoryTheory.MorphismProperty.arrow_mk_iso_iff