awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ k) (E.p₂ k) ⋯
refine_2 : Eq (α := pullback l r ⟶ E.X i₁) (pullback.fst l r ≫ p₁) (pullback.snd l r ≫ E.p₁ k)
refine_2₁ : Eq (α := pullback l r ⟶ E.X i₂) (pullback.fst l r ≫ p₂) (pullback.snd l r ≫ E.p₂ k)
⊢ (E.sieve₁ p₁ p₂).arrows (Y := pullback l r) (pullback.fst l r)

Tactic:
refine ⟨k, pullback.snd _ _, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ k) (E.p₂ k) ⋯
⊢ Eq (α := pullback l r ⟶ E.X i₁) (pullback.fst l r ≫ p₁) (pullback.snd l r ≫ E.p₁ k)

Tactic:
simp [← hl₁, ← hl₂, pullback.condition_assoc, r]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ k) (E.p₂ k) ⋯
⊢ Eq (α := pullback l r ⟶ E.X i₂) (pullback.fst l r ≫ p₂) (pullback.snd l r ≫ E.p₂ k)

Tactic:
simp [← hl₁, ← hl₂, pullback.condition_assoc, r]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
E : PreOneHypercover.{u_1, v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst_2 : HasPullbacks.{v₁, u₁} C
inst_3 : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ k) (E.p₂ k) ⋯
⊢ f = CategoryStruct.comp (Y := F.obj (pullback l r)) (IsPullback.lift ⋯ f u ⋯) (F.map (pullback.fst l r))

Tactic:
simp
-- 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
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op
inst_2 : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hU : Presheaf.IsSheaf K U
rw :
  Function.Bijective (β := G ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U)
    fun (g : G' ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U) ↦ f ≫ g
⊢ Function.Bijective (β := H.obj G ⟶ U) fun (g : H.obj G' ⟶ U) ↦ H.map f ≫ g

Tactic:
rw [adj.map_comp_bijective_iff]

Premises used: CategoryTheory.Adjunction.map_comp_bijective_iff
-- 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
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op
inst_2 : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hU : Presheaf.IsSheaf K U
a : Presheaf.IsSheaf J (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U)
⊢ Function.Bijective (β := G ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U)
    fun (g : G' ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U) ↦ f ≫ g

Tactic:
apply hf
-- 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
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op
inst_2 : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hU : Presheaf.IsSheaf K U
a : Presieve.IsSheaf J (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U)
⊢ Presheaf.IsSheaf J (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- 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
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op
inst_2 : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hU : Presheaf.IsSheaf K U
⊢ Presieve.IsSheaf J (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U)

Tactic:
IsContinuous.op_comp_isSheaf_of_types (F := F) ⟨U, hU⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Functor.comp, CategoryTheory.Functor.IsContinuous.op_comp_isSheaf_of_types
-- 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
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op
inst_2 : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hU : Presheaf.IsSheaf K U
⊢ Presieve.IsSheaf J (obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))) F.op) U)

Tactic:
exact IsContinuous.op_comp_isSheaf_of_types (F := F) ⟨U, hU⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Functor.IsContinuous.op_comp_isSheaf_of_types
-- 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₂))
⊢ Presieve.IsSheaf J (F.op ⋙ G)

Tactic:
Presieve.IsSheaf.comp_of_W_map_of_adjunction _ adj' ?_ _ hG

Premises used: CategoryTheory.Presieve.IsSheaf.comp_of_W_map_of_adjunction
-- 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₂))
refine :
  ∀ ⦃X : C⦄ ⦃S : Sieve.{v₁, u₁} X⦄,
    S ∈ (J : (a : C) → Set (Sieve a)) X →
      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)))
⊢ Presieve.IsSheaf J (F.op ⋙ G)

Tactic:
refine Presieve.IsSheaf.comp_of_W_map_of_adjunction _ adj' ?_ _ hG

Premises used: CategoryTheory.Presieve.IsSheaf.comp_of_W_map_of_adjunction
-- 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
⊢ 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))

Tactic:
have hWS : J.W (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂} S).ι :=
    Sieve.W_shrinkFunctor_ι_of_mem.{max u₁ v₁ u₂ v₂} _ S hS
-- 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))
⊢ 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)))

Tactic:
have : K.W _ := Functor.W_map_of_adjunction_of_isContinuous_aux (J := J) K F H adj
    (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂} S).ι hWS
-- 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
⊢ 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
        (Subfunctor.ι (Sieve.shrinkFunctor.{max w (max (max u₁ u₂) v₁) v₂, v₁, u₁} S) ≫
          NatTrans.app (Iso.inv shrinkYonedaUliftFunctorIso) X) ≫
      e.inv.app (obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X))
    (H'.map
        (Subfunctor.ι (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S) ≫
          NatTrans.app (Iso.inv shrinkYonedaUliftFunctorIso) X) ≫
      e.inv.app (obj shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁} X))

Tactic:
rfl
-- 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)
hf :
  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)))
⊢ 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₂})

Tactic:
apply GrothendieckTopology.W_of_preservesSheafification

Premises used: CategoryTheory.GrothendieckTopology.W_of_preservesSheafification
-- 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)
⊢ 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)))

Tactic:
F.W_map_of_adjunction_of_isContinuous_aux J K H adj
    (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂} S).ι hWS

Premises used: _private.0.CategoryTheory.Functor.W_map_of_adjunction_of_isContinuous_aux, CategoryTheory.Sieve.shrinkFunctor, CategoryTheory.Subfunctor.ι
-- 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)
⊢ 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)))

Tactic:
exact F.W_map_of_adjunction_of_isContinuous_aux J K H adj
    (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂} S).ι hWS