Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
inst✝ : 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 ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj 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' ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))).obj F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
X : C
S : Sieve X
hS : S ∈ J X
hWS : J.W (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι
this : K.W (H.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι)
e : H ⋙
    (whiskeringRight Dᵒᵖ (Type (max u₁ v₁ u₂ v₂)) (Type (max (max (max (max u₁ u₂) v₁) v₂) w))).obj
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} ≅
  (whiskeringRight Cᵒᵖ (Type (max u₁ v₁ u₂ v₂)) (Type (max (max (max (max u₁ u₂) v₁) v₂) w))).obj
      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 (H'.map (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S).ι) ≅
  Arrow.mk
    (whiskerRight (H.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι)
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂}) :=
  Arrow.isoMk' (H'.map (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S).ι)
    (whiskerRight (H.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι)
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂})
    (H'.mapIso S.shrinkFunctorUliftFunctorIso.symm ≪≫
      (e.app (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).toFunctor).symm)
    (H'.mapIso (shrinkYonedaUliftFunctorIso.app X).symm ≪≫ (e.app (shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁}.obj X)).symm)
    ⋯
⊢ K.W
    (whiskerRight (H.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι)
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂})

Tactic:
apply GrothendieckTopology.W_of_preservesSheafification

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
inst✝ : 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₂) := ⋯
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op := ⋯
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := ⋯
adj' : H' ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))).obj F.op := ⋯
X : C
S : Sieve X
hS : S ∈ J X
hWS : J.W (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι
this : K.W (H.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι)
e : H ⋙
    (whiskeringRight Dᵒᵖ (Type (max u₁ v₁ u₂ v₂)) (Type (max (max (max (max u₁ u₂) v₁) v₂) w))).obj
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} ≅
  (whiskeringRight Cᵒᵖ (Type (max u₁ v₁ u₂ v₂)) (Type (max (max (max (max u₁ u₂) v₁) v₂) w))).obj
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} ⋙
    H' := ⋯
iso : Arrow.mk (H'.map (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S).ι) ≅
  Arrow.mk
    (whiskerRight (H.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι)
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂}) := ⋯
⊢ K.W (H.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι)