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
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : F.IsContinuous J K
G : Sheaf K (Type t)
rw : Presieve.IsSheaf J (F.op ⋙ G.obj (P := Presheaf.IsSheaf K) ⋙ uliftFunctor.{max u₁ v₁ u₂ v₂, t})
⊢ Presieve.IsSheaf.{t, v₁, u₁} J (F.op ⋙ G.obj (P := Presheaf.IsSheaf K))

Tactic:
rw [← Presieve.isSheaf_comp_uliftFunctor_iff.{t, max u₁ v₁ u₂ v₂}, ← isSheaf_iff_isSheaf_of_type,
    Presheaf.isSheaf_of_iso_iff (Functor.associator _ _ _), isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.Presheaf.isSheaf_of_iso_iff, CategoryTheory.Functor.associator, 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
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : F.IsContinuous J K
G : Sheaf K (Type t)
hG : Presieve.IsSheaf K (G.obj (P := Presheaf.IsSheaf K) ⋙ uliftFunctor.{max u₁ v₁ u₂ v₂, t})
⊢ Presieve.IsSheaf J (F.op ⋙ G.obj (P := Presheaf.IsSheaf K) ⋙ uliftFunctor.{max u₁ v₁ u₂ v₂, t})

Tactic:
apply isSheaf_of_isContinuous_aux.{t} J K
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : F.IsContinuous J K
G : Sheaf K (Type t)
hG : Presheaf.IsSheaf K (G.obj (P := Presheaf.IsSheaf K))
⊢ Presieve.IsSheaf K (G.obj (P := Presheaf.IsSheaf K) ⋙ uliftFunctor.{max u₁ v₁ u₂ v₂, t})

Tactic:
rw [Presieve.isSheaf_comp_uliftFunctor_iff, ← isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type, CategoryTheory.Presieve.isSheaf_comp_uliftFunctor_iff
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : F.IsContinuous J K
G : Sheaf K (Type t)
⊢ Presheaf.IsSheaf K (G.obj (P := Presheaf.IsSheaf K))

Tactic:
G.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : F.IsContinuous J K
G : Sheaf K (Type t)
⊢ Presheaf.IsSheaf K (G.obj (P := Presheaf.IsSheaf K))

Tactic:
exact G.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u
inst_2 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_3 : F.IsContinuous J K
G : Sheaf.{v₂, t, u₂, u} K A
⊢ Presheaf.IsSheaf J (F.op ⋙ G.obj (P := Presheaf.IsSheaf K))

Tactic:
fun T => F.op_comp_isSheaf_of_types J K ⟨_, (isSheaf_iff_isSheaf_of_type _ _).2 (G.property T)⟩

Premises used: Iff.mpr, CategoryTheory.Functor.op, CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.coyoneda, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.op_comp_isSheaf_of_types, CategoryTheory.isSheaf_iff_isSheaf_of_type, Opposite.op, CategoryTheory.Presheaf.IsSheaf, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u
inst_2 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_3 : F.IsContinuous J K
P : Functor.{v₂, t, u₂, u} Dᵒᵖ A
h : Presheaf.IsSheaf K P
⊢ Presheaf.IsSheaf J (F.op ⋙ P)

Tactic:
F.op_comp_isSheaf J K ⟨P, h⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Functor.op_comp_isSheaf
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : Type u
inst_2 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
H : Functor.{v₁, t, u₁, u} Cᵒᵖ A ⥤ Functor.{v₂, t, u₂, u} Dᵒᵖ A
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) F.op
inst_3 : F.IsContinuous J K
G G' : Functor.{v₁, t, u₁, u} Cᵒᵖ A
f : G ⟶ G'
hf : J.W f
U : Functor.{v₂, t, u₂, u} Dᵒᵖ A
hU : Presheaf.IsSheaf K U
rw :
  Function.Bijective (β := G ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) F.op) U)
    fun (g : G' ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) 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
A : Type u
inst_2 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
H : Functor.{v₁, t, u₁, u} Cᵒᵖ A ⥤ Functor.{v₂, t, u₂, u} Dᵒᵖ A
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) F.op
inst_3 : F.IsContinuous J K
G G' : Functor.{v₁, t, u₁, u} Cᵒᵖ A
f : G ⟶ G'
hf : J.W f
U : Functor.{v₂, t, u₂, u} Dᵒᵖ A
hU : Presheaf.IsSheaf K U
⊢ Function.Bijective (β := G ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) F.op) U)
    fun (g : G' ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) F.op) U) ↦ f ≫ g

Tactic:
hf _ (F.op_comp_isSheaf_of_isSheaf _ _ _ hU)

Premises used: CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : Type u
inst_2 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
H : Functor.{v₁, t, u₁, u} Cᵒᵖ A ⥤ Functor.{v₂, t, u₂, u} Dᵒᵖ A
adj : H ⊣ obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) F.op
inst_3 : F.IsContinuous J K
G G' : Functor.{v₁, t, u₁, u} Cᵒᵖ A
f : G ⟶ G'
hf : J.W f
U : Functor.{v₂, t, u₂, u} Dᵒᵖ A
hU : Presheaf.IsSheaf K U
⊢ Function.Bijective (β := G ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) F.op) U)
    fun (g : G' ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) F.op) U) ↦ f ≫ g

Tactic:
exact hf _ (F.op_comp_isSheaf_of_isSheaf _ _ _ hU)

Premises used: CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F₁ : Functor.{v₁, v₂, u₁, u₂} C D
F₂ : Functor.{v₂, v₃, u₂, u₃} D E
F₁₂ : Functor.{v₁, v₃, u₁, u₃} C E
e : F₁ ⋙ F₂ ≅ F₁₂
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
L : GrothendieckTopology.{v₃, u₃} E
inst_3 : F₁.IsContinuous J K
inst_4 : F₂.IsContinuous K L
⊢ (F₁ ⋙ F₂).IsContinuous J L

Tactic:
have := Functor.isContinuous_comp F₁ F₂ J K L
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F₁ : Functor.{v₁, v₂, u₁, u₂} C D
F₂ : Functor.{v₂, v₃, u₂, u₃} D E
F₁₂ : Functor.{v₁, v₃, u₁, u₃} C E
e : F₁ ⋙ F₂ ≅ F₁₂
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
L : GrothendieckTopology.{v₃, u₃} E
inst_3 : F₁.IsContinuous J K
inst_4 : F₂.IsContinuous K L
this : (F₁ ⋙ F₂).IsContinuous J L
⊢ F₁₂.IsContinuous J L

Tactic:
apply Functor.isContinuous_of_iso e

Premises used: CategoryTheory.Functor.isContinuous_of_iso
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
τ : F ⟶ F'
e : F ≅ F'
G : Functor.{v₂, v₃, u₂, u₃} D E
F'' : Functor.{v₁, v₁, u₁, u₁} C C
eF'' : F'' ≅ 𝟭 C
FG : Functor.{v₁, v₃, u₁, u₃} C E
eFG : F ⋙ G ≅ FG
A : Type u
inst_3 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
L : GrothendieckTopology.{v₃, u₃} E
inst_4 : F.IsContinuous J K
⊢ (F ⋙ 𝟭 D).IsContinuous J K

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
τ : F ⟶ F'
e : F ≅ F'
G : Functor.{v₂, v₃, u₂, u₃} D E
F'' : Functor.{v₁, v₁, u₁, u₁} C C
eF'' : F'' ≅ 𝟭 C
FG : Functor.{v₁, v₃, u₁, u₃} C E
eFG : F ⋙ G ≅ FG
A : Type u
inst_3 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
L : GrothendieckTopology.{v₃, u₃} E
inst_4 : F.IsContinuous J K
⊢ (𝟭 C ⋙ F).IsContinuous J K

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : Precoverage.{v₁, u₁} C
K : Precoverage.{v₂, u₂} D
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : K.IsStableUnderBaseChange
inst_5 : K.HasPullbacks
inst_6 : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H : Presheaf.IsSheaf K.toGrothendieck G
⊢ Presieve.IsSheaf K.toGrothendieck G

Tactic:
rw [isSheaf_iff_isSheaf_of_type] at H

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
F : Functor.{v₁, v₂, u₁, u₂} C D
J : Precoverage.{v₁, u₁} C
K : Precoverage.{v₂, u₂} D
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : K.IsStableUnderBaseChange
inst_5 : K.HasPullbacks
inst_6 : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H_1 : Presheaf.IsSheaf K.toGrothendieck G
H : Presieve.IsSheaf K.toGrothendieck G
rw :
  ∀ (H : ∀ {X : D}, ∀ R ∈ K.toCoverage.coverings X, Presieve.IsSheafFor G R) {X : C},
    ∀ R ∈ J.toCoverage.coverings X,
      Presieve.IsSheafFor
        (F.op ⋙
          ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf K.toGrothendieck)
            (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf K.toGrothendieck) G H_1))
        R
⊢ Presieve.IsSheaf J.toGrothendieck
    (F.op ⋙
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf K.toGrothendieck)
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf K.toGrothendieck) G H_1))

Tactic:
rw [← Precoverage.toGrothendieck_toCoverage, Presieve.isSheaf_coverage] at H ⊢

Premises used: CategoryTheory.Presieve.isSheaf_coverage, CategoryTheory.Precoverage.toGrothendieck_toCoverage
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : Precoverage.{v₁, u₁} C
K : Precoverage.{v₂, u₂} D
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : K.IsStableUnderBaseChange
inst_5 : K.HasPullbacks
inst_6 : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H_1 : Presheaf.IsSheaf K.toGrothendieck G
H : ∀ {X : D}, ∀ R ∈ K.toCoverage.coverings X, Presieve.IsSheafFor G R
X : C
R : Presieve.{v₁, u₁} X
hR : R ∈ J.toCoverage.coverings X
⊢ F.PreservesPairwisePullbacks R

Tactic:
have : F.PreservesPairwisePullbacks R := J.preservesPairwisePullbacks_of_mem hR
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : Precoverage.{v₁, u₁} C
K : Precoverage.{v₂, u₂} D
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : K.IsStableUnderBaseChange
inst_5 : K.HasPullbacks
inst_6 : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H_1 : Presheaf.IsSheaf K.toGrothendieck G
H : ∀ {X : D}, ∀ R ∈ K.toCoverage.coverings X, Presieve.IsSheafFor G R
X : C
R : Presieve.{v₁, u₁} X
hR : R ∈ J.toCoverage.coverings X
this : F.PreservesPairwisePullbacks R
⊢ R.HasPairwisePullbacks

Tactic:
have : R.HasPairwisePullbacks := J.hasPairwisePullbacks_of_mem hR
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : Precoverage.{v₁, u₁} C
K : Precoverage.{v₂, u₂} D
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : K.IsStableUnderBaseChange
inst_5 : K.HasPullbacks
inst_6 : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H_1 : Presheaf.IsSheaf K.toGrothendieck G
H : ∀ {X : D}, ∀ R ∈ K.toCoverage.coverings X, Presieve.IsSheafFor G R
X : C
R : Presieve.{v₁, u₁} X
hR : R ∈ J.toCoverage.coverings X
this_1 : F.PreservesPairwisePullbacks R
this : R.HasPairwisePullbacks
rw :
  Presieve.IsSheafFor
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf K.toGrothendieck)
      (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf K.toGrothendieck) G H_1))
    (Presieve.map F R)
⊢ Presieve.IsSheafFor
    (F.op ⋙
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf K.toGrothendieck)
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf K.toGrothendieck) G H_1))
    R

Tactic:
rw [Presieve.IsSheafFor.comp_iff_of_preservesPairwisePullbacks]

Premises used: CategoryTheory.Presieve.IsSheafFor.comp_iff_of_preservesPairwisePullbacks
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : Precoverage.{v₁, u₁} C
K : Precoverage.{v₂, u₂} D
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : K.IsStableUnderBaseChange
inst_5 : K.HasPullbacks
inst_6 : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H_1 : Presheaf.IsSheaf K.toGrothendieck G
H : ∀ {X : D}, ∀ R ∈ K.toCoverage.coverings X, Presieve.IsSheafFor G R
X : C
R : Presieve.{v₁, u₁} X
hR : R ∈ J.toCoverage.coverings X
this_1 : F.PreservesPairwisePullbacks R
this : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf K.toGrothendieck)
      (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf K.toGrothendieck) G H_1))
    (Presieve.map F R)

Tactic:
H _ (h _ hR)
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : Precoverage.{v₁, u₁} C
K : Precoverage.{v₂, u₂} D
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : K.IsStableUnderBaseChange
inst_5 : K.HasPullbacks
inst_6 : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H_1 : Presheaf.IsSheaf K.toGrothendieck G
H : ∀ {X : D}, ∀ R ∈ K.toCoverage.coverings X, Presieve.IsSheafFor G R
X : C
R : Presieve.{v₁, u₁} X
hR : R ∈ J.toCoverage.coverings X
this_1 : F.PreservesPairwisePullbacks R
this : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf K.toGrothendieck)
      (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf K.toGrothendieck) G H_1))
    (Presieve.map F R)

Tactic:
exact H _ (h _ hR)
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u
inst_2 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_3 : F.PreservesOneHypercovers J K
inst_4 : J.IsGeneratedByOneHypercovers
P : Functor.{v₂, t, u₂, u} Dᵒᵖ A
hP : Presheaf.IsSheaf K P
rw : ∀ ⦃X : C⦄ (E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J X), Nonempty (IsLimit (E.multifork (F.op ⋙ P)))
⊢ Presheaf.IsSheaf J (F.op ⋙ P)

Tactic:
rw [Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers.{w}]
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u
inst_2 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_3 : F.PreservesOneHypercovers J K
inst_4 : J.IsGeneratedByOneHypercovers
P : Functor.{v₂, t, u₂, u} Dᵒᵖ A
hP : Presheaf.IsSheaf K P
X : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J X
⊢ Nonempty (IsLimit (E.multifork (F.op ⋙ P)))

Tactic:
⟨(E.toPreOneHypercover.isLimitMapMultiforkEquiv F P)
    ((E.map F K).isLimitMultifork ⟨P, hP⟩)⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.GrothendieckTopology.OneHypercover.map, CategoryTheory.GrothendieckTopology.OneHypercover.toPreOneHypercover, Nonempty.intro, CategoryTheory.GrothendieckTopology.OneHypercover.isLimitMultifork, DFunLike.coe, CategoryTheory.PreOneHypercover.isLimitMapMultiforkEquiv
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
A : Type u
inst_2 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_3 : F.PreservesOneHypercovers J K
inst_4 : J.IsGeneratedByOneHypercovers
P : Functor.{v₂, t, u₂, u} Dᵒᵖ A
hP : Presheaf.IsSheaf K P
X : C
E : GrothendieckTopology.OneHypercover.{w, v₁, u₁} J X
⊢ Nonempty (IsLimit (E.multifork (F.op ⋙ P)))

Tactic:
exact ⟨(E.toPreOneHypercover.isLimitMapMultiforkEquiv F P)
    ((E.map F K).isLimitMultifork ⟨P, hP⟩)⟩
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : F.PreservesOneHypercovers J K
inst_3 : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hP : Presheaf.IsSheaf K P
rw :
  Presheaf.IsSheaf J
    (F.op ⋙
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf K)
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf K) P hP))
⊢ Presieve.IsSheaf J
    (F.op ⋙
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf K)
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf K) P hP))

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
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : F.PreservesOneHypercovers J K
inst_3 : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hP : Presheaf.IsSheaf K P
⊢ Presheaf.IsSheaf J
    (F.op ⋙
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf K)
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf K) P hP))

Tactic:
F.op_comp_isSheaf_of_preservesOneHypercovers J K P hP

Premises used: CategoryTheory.Functor.op_comp_isSheaf_of_preservesOneHypercovers
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
inst_2 : F.PreservesOneHypercovers J K
inst_3 : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hP : Presheaf.IsSheaf K P
⊢ Presheaf.IsSheaf J
    (F.op ⋙
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf K)
        (ObjectProperty.FullSubcategory.mk (P := Presheaf.IsSheaf K) P hP))

Tactic:
exact F.op_comp_isSheaf_of_preservesOneHypercovers J K P hP

Premises used: CategoryTheory.Functor.op_comp_isSheaf_of_preservesOneHypercovers
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
τ : F ⟶ F'
e : F ≅ F'
G : Functor.{v₂, v₃, u₂, u₃} D E
F'' : Functor.{v₁, v₁, u₁, u₁} C C
eF'' : F'' ≅ 𝟭 C
FG : Functor.{v₁, v₃, u₁, u₃} C E
eFG : F ⋙ G ≅ FG
A : Type u
inst_3 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
L : GrothendieckTopology.{v₃, u₃} E
inst_4 : F.PreservesOneHypercovers J K
⊢ F.IsContinuous J K

Tactic:
isContinuous_of_preservesOneHypercovers.{max u₁ v₁} F J K

Premises used: CategoryTheory.Functor.isContinuous_of_preservesOneHypercovers
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
τ : F ⟶ F'
e : F ≅ F'
G : Functor.{v₂, v₃, u₂, u₃} D E
F'' : Functor.{v₁, v₁, u₁, u₁} C C
eF'' : F'' ≅ 𝟭 C
FG : Functor.{v₁, v₃, u₁, u₃} C E
eFG : F ⋙ G ≅ FG
A : Type u
inst_3 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
L : GrothendieckTopology.{v₃, u₃} E
inst_4 : F.IsContinuous J K
inst_5 : F'.IsContinuous J K
w :
  ∀ (x : Sheaf.{v₂, t, u₂, u} K A) (x_1 : Cᵒᵖ),
    Eq (α :=
      (obj (F.sheafPushforwardContinuous A J K) x).obj (P := Presheaf.IsSheaf J).obj x_1 ⟶
        (obj (F.sheafPushforwardContinuous A J K) x).obj (P := Presheaf.IsSheaf J).obj x_1)
      (NatTrans.app
        (InducedCategory.Hom.hom
          (NatTrans.app
            (CategoryStruct.comp (Y := F'.sheafPushforwardContinuous A J K)
              (sheafPushforwardContinuousNatTrans e.inv A J K) (sheafPushforwardContinuousNatTrans e.hom A J K))
            x))
        x_1)
      (NatTrans.app (InducedCategory.Hom.hom (NatTrans.app (𝟙 (F.sheafPushforwardContinuous A J K)) x)) x_1)
⊢ Eq (α :=
    Quiver.Hom (V := Sheaf.{v₂, t, u₂, u} K A ⥤ Sheaf.{v₁, t, u₁, u} J A) (F.sheafPushforwardContinuous A J K)
      (F.sheafPushforwardContinuous A J K))
    (CategoryStruct.comp (Y := F'.sheafPushforwardContinuous A J K) (sheafPushforwardContinuousNatTrans e.inv A J K)
      (sheafPushforwardContinuousNatTrans e.hom A J K))
    (𝟙 (F.sheafPushforwardContinuous A J K))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Continuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
τ : F ⟶ F'
e : F ≅ F'
G : Functor.{v₂, v₃, u₂, u₃} D E
F'' : Functor.{v₁, v₁, u₁, u₁} C C
eF'' : F'' ≅ 𝟭 C
FG : Functor.{v₁, v₃, u₁, u₃} C E
eFG : F ⋙ G ≅ FG
A : Type u
inst_3 : Category.{t, u} A
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
L : GrothendieckTopology.{v₃, u₃} E
inst_4 : F.IsContinuous J K
inst_5 : F'.IsContinuous J K
x : Sheaf.{v₂, t, u₂, u} K A
x_1 : Cᵒᵖ
⊢ Eq (α :=
    (obj (F.sheafPushforwardContinuous A J K) x).obj (P := Presheaf.IsSheaf J).obj x_1 ⟶
      (obj (F.sheafPushforwardContinuous A J K) x).obj (P := Presheaf.IsSheaf J).obj x_1)
    (NatTrans.app
      (InducedCategory.Hom.hom
        (NatTrans.app
          (CategoryStruct.comp (Y := F'.sheafPushforwardContinuous A J K)
            (sheafPushforwardContinuousNatTrans e.inv A J K) (sheafPushforwardContinuousNatTrans e.hom A J K))
          x))
      x_1)
    (NatTrans.app (InducedCategory.Hom.hom (NatTrans.app (𝟙 (F.sheafPushforwardContinuous A J K)) x)) x_1)

Tactic:
simp [← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp