awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
hG : IsSheaf J G
inst_4 : HasFunctorEnrichedHom A F G
M : A
rw : IsSheaf J (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G)
⊢ Presieve.IsSheaf J (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G)

Tactic:
rw [← isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
hG : IsSheaf J G
inst_4 : HasFunctorEnrichedHom A F G
M : A
⊢ IsSheaf J (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G)

Tactic:
Presheaf.IsSheaf.hom (F ⊗ (Functor.const _).obj M) G hG

Premises used: CategoryTheory.Presheaf.IsSheaf.hom, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.Functor.const, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
hG : IsSheaf J G
inst_4 : HasFunctorEnrichedHom A F G
M : A
⊢ IsSheaf J (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G)

Tactic:
exact Presheaf.IsSheaf.hom (F ⊗ (Functor.const _).obj M) G hG

Premises used: CategoryTheory.Presheaf.IsSheaf.hom, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.Functor.const, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : Functor.EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_8 : MorphismProperty.IsMonoidal (C := Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) K.W
rw :
  MorphismProperty.IsMonoidal (C := Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A)
    (MorphismProperty.inverseImage K.W (Functor.obj (Functor.whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))
⊢ MorphismProperty.IsMonoidal (C := Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A) J.W

Tactic:
rw [← J.W_inverseImage_whiskeringLeft K G]

Premises used: CategoryTheory.GrothendieckTopology.W_inverseImage_whiskeringLeft
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : Functor.EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_8 : MorphismProperty.IsMonoidal (C := Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) K.W
⊢ MorphismProperty.IsMonoidal (C := Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A)
    (MorphismProperty.inverseImage K.W (Functor.obj (Functor.whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
⊢ Function.Bijective (β := G₁ ⟶ functorEnrichedHom A F H) fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1

Tactic:
have := hg _ (Presheaf.isSheaf_functorEnrichedHom F H h)
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
this : Function.Bijective (β := G₁ ⟶ functorEnrichedHom A F H) fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1
rw :
  Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ F ⟹ H)
    (curry ∘ fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1)
⊢ Function.Bijective (β := tensorObj (𝒞 := Functor.category) F G₁ ⟶ H)
    fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1

Tactic:
rw [← Function.Bijective.of_comp_iff' (f := MonoidalClosed.curry)
    ((ihom.adjunction _).homEquiv _ _).bijective]

Premises used: Equiv.bijective, Function.Bijective.of_comp_iff', CategoryTheory.ihom.adjunction, CategoryTheory.Adjunction.homEquiv
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
this : Function.Bijective (β := G₁ ⟶ functorEnrichedHom A F H) fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1
⊢ Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ functorEnrichedHom A F H)
    ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry)

Tactic:
rw [← Function.Bijective.of_comp_iff (g := MonoidalClosed.curry) _
    ((ihom.adjunction _).homEquiv _ _).bijective] at this

Premises used: Equiv.bijective, Function.Bijective.of_comp_iff, CategoryTheory.ihom.adjunction, CategoryTheory.Adjunction.homEquiv
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
this :
  Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ functorEnrichedHom A F H)
    ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry)
⊢ Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ functorEnrichedHom A F H)
    ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry)

Tactic:
this
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
this :
  Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ functorEnrichedHom A F H)
    ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry)
h₁ :
  (G₁ ⟶ F ⟹ H) = (G₁ ⟶ functorEnrichedHom A F H) →
    Eq (α := (tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) → (G₁ ⟶ F ⟹ H))
      (curry ∘ fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1 :
        (tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) → (G₁ ⟶ F ⟹ H))
      ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry :
        (tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) → (G₁ ⟶ functorEnrichedHom A F H))
⊢ Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ F ⟹ H)
    (curry ∘ fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1)

Tactic:
convert! this using 1
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
this :
  Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ functorEnrichedHom A F H)
    ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry)
e_2 : (G₁ ⟶ F ⟹ H) = (G₁ ⟶ functorEnrichedHom A F H)
h₁ :
  ∀ (α : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H),
    Eq (α := G₁ ⟶ F ⟹ H) ((curry ∘ fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1) α)
      (((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry) α)
⊢ Eq (α := (tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) → (G₁ ⟶ F ⟹ H))
    (curry ∘ fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1 :
      (tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) → (G₁ ⟶ F ⟹ H))
    ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry :
      (tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) → (G₁ ⟶ functorEnrichedHom A F H))

Tactic:
ext α : 1
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
this :
  Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ functorEnrichedHom A F H)
    ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry)
e_2 : (G₁ ⟶ F ⟹ H) = (G₁ ⟶ functorEnrichedHom A F H)
α : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H
h₁ h₂ : Eq (α := G₁ ⟶ F ⟹ H) (g ≫ curry α) (g ≫ curry α)
⊢ Eq (α := G₁ ⟶ F ⟹ H) (curry (F ◁ g ≫ α)) (g ≫ curry α)

Tactic:
rw [curry_natural_left]

Premises used: CategoryTheory.MonoidalClosed.curry_natural_left
-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
inst_6 : BraidedCategory.{v₃, u₃} A
F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
f : F₁ ⟶ F₂
hf : J.W f
G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
⊢ J.W (X := tensorObj (𝒞 := Functor.category) F₁ G) (f ▷ G)

Tactic:
(J.W.arrow_mk_iso_iff (Arrow.isoMk (β_ F₁ G) (β_ F₂ G))).2 (hf.whiskerLeft G)

Premises used: Iff.mpr, CategoryTheory.GrothendieckTopology.W, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.GrothendieckTopology.W.whiskerLeft, CategoryTheory.BraidedCategory.braiding, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
X : C
ι : Type u_2
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ Presieve.ofArrows Y f ∈ P.precoverage.coverings X ↔ ∀ (i : ι), P (f i)

Tactic:
⟨fun h i ↦ h ⟨i⟩, fun h _ g ⟨i⟩ ↦ h i⟩

Premises used: _private.0.CategoryTheory.MorphismProperty.ofArrows_mem_precoverage.match_1, CategoryTheory.Presieve.ofArrows.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
T : C
g_1 : T ⟶ S
W : ι → C
p₁ : (i : ι) → W i ⟶ T
p₂ : (i : ι) → W i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g_1 (f i)
Z : C
g : Z ⟶ T
hg : Presieve.ofArrows W p₁ g
obtain : ∀ ⦃Y : C⦄ (i : ι), P (p₁ i)
⊢ P g

Tactic:
obtain ⟨i⟩ := hg
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
T : C
g : T ⟶ S
W : ι → C
p₁ : (i : ι) → W i ⟶ T
p₂ : (i : ι) → W i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
Y : C
i : ι
⊢ P (p₁ i)

Tactic:
P.of_isPullback (h i).flip (hf ⟨i⟩)

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.IsPullback.flip
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
T : C
g : T ⟶ S
W : ι → C
p₁ : (i : ι) → W i ⟶ T
p₂ : (i : ι) → W i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
Y : C
i : ι
⊢ P (p₁ i)

Tactic:
exact P.of_isPullback (h i).flip (hf ⟨i⟩)

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.IsPullback.flip
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderComposition
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u_1 v_1)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} (X i))) (P.precoverage.coverings (X i))
      (Presieve.ofArrows (Y i) (g i))
Z : C
p : Z ⟶ S
i : (i : ι) × σ i
⊢ P (g (i.fst (β := fun (i : ι) ↦ σ i)) (i.snd (β := fun (i : ι) ↦ σ i)) ≫ f (i.fst (β := fun (i : ι) ↦ σ i)))

Tactic:
P.comp_mem _ _ (hg _ ⟨i.2⟩) (hf ⟨i.1⟩)

Premises used: CategoryTheory.Presieve.ofArrows.mk, Sigma.fst, CategoryTheory.MorphismProperty.comp_mem, Sigma.snd
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderComposition
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
σ : ι → Type (max u_1 v_1)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg :
  ∀ (i : ι),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} (X i))) (P.precoverage.coverings (X i))
      (Presieve.ofArrows (Y i) (g i))
Z : C
p : Z ⟶ S
i : (i : ι) × σ i
⊢ P (g (i.fst (β := fun (i : ι) ↦ σ i)) (i.snd (β := fun (i : ι) ↦ σ i)) ≫ f (i.fst (β := fun (i : ι) ↦ σ i)))

Tactic:
exact P.comp_mem _ _ (hg _ ⟨i.2⟩) (hf ⟨i.1⟩)

Premises used: CategoryTheory.Presieve.ofArrows.mk, Sigma.fst, CategoryTheory.MorphismProperty.comp_mem, Sigma.snd
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
S : C
E : P.precoverage.ZeroHypercover S
exists_restrictIndex_mem :
  ∃ (ι : Type w) (f : ι → E.I₀),
    PreZeroHypercover.presieve₀.{w, v_1, u_1} (E.restrictIndex f) ∈ P.precoverage.coverings S
⊢ E.Small

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
S : C
E : P.precoverage.ZeroHypercover S
h : PreZeroHypercover.presieve₀.{w, v_1, u_1} (E.restrictIndex PEmpty.elim) ∈ P.precoverage.coverings S
⊢ ∃ (ι : Type w) (f : ι → E.I₀),
    PreZeroHypercover.presieve₀.{w, v_1, u_1} (E.restrictIndex f) ∈ P.precoverage.coverings S

Tactic:
use PEmpty, PEmpty.elim

Premises used: PEmpty, PEmpty.elim
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
S : C
E : P.precoverage.ZeroHypercover S
⊢ PreZeroHypercover.presieve₀.{w, v_1, u_1} (E.restrictIndex PEmpty.elim) ∈ P.precoverage.coverings S

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
hPQ : P ≤ Q
⊢ P.precoverage ≤ Q.precoverage

Tactic:
fun _ _ hR _ _ hg ↦ hPQ _ (hR hg)

Premises used: Set.Mem, setOf, Set.Subset
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
coverings :
  ∀ (X : C) (R : Presieve.{v_1, u_1} X),
    R ∈ (P ⊓ Q).precoverage.coverings X ↔ R ∈ (P.precoverage ⊓ Q.precoverage).coverings X
⊢ (P ⊓ Q).precoverage = P.precoverage ⊓ Q.precoverage

Tactic:
ext X R
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
X : C
R : Presieve.{v_1, u_1} X
⊢ R ∈ (P ⊓ Q).precoverage.coverings X ↔ R ∈ (P.precoverage ⊓ Q.precoverage).coverings X

Tactic:
⟨fun hS ↦ ⟨fun _ _ hf ↦ (hS hf).left, fun _ _ hf ↦ (hS hf).right⟩,
    fun h ↦ fun _ _ hf ↦ ⟨h.left hf, h.right hf⟩⟩

Premises used: And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
X : C
R : Presieve.{v_1, u_1} X
⊢ R ∈ (P ⊓ Q).precoverage.coverings X ↔ R ∈ (P.precoverage ⊓ Q.precoverage).coverings X

Tactic:
exact ⟨fun hS ↦ ⟨fun _ _ hf ↦ (hS hf).left, fun _ _ hf ↦ (hS hf).right⟩,
    fun h ↦ fun _ _ hf ↦ ⟨h.left hf, h.right hf⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
X : C
⊢ ⊥ ∈ P.precoverage.coverings X

Tactic:
fun _ _ h ↦ h.elim

Premises used: Set.Mem, False.elim, setOf
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
P : MorphismProperty.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
coverings :
  ∀ (X : C) (R : Presieve.{v_1, u_1} X),
    R ∈ (Precoverage.comap F P.precoverage).coverings X ↔ R ∈ (P.inverseImage F).precoverage.coverings X
⊢ Precoverage.comap F P.precoverage = (P.inverseImage F).precoverage

Tactic:
ext X R
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
P : MorphismProperty.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X : C
R : Presieve.{v_1, u_1} X
coverings :
  ∀ (ι : Type (max u_1 v_1)) (Y : ι → C) (f : (i : ι) → Y i ⟶ X),
    Presieve.ofArrows Y f ∈ (Precoverage.comap F P.precoverage).coverings X ↔
      Presieve.ofArrows Y f ∈ (P.inverseImage F).precoverage.coverings X
⊢ R ∈ (Precoverage.comap F P.precoverage).coverings X ↔ R ∈ (P.inverseImage F).precoverage.coverings X

Tactic:
obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows

Premises used: CategoryTheory.Presieve.exists_eq_ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
P : MorphismProperty.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X : C
ι : Type (max u_1 v_1)
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ Presieve.ofArrows Y f ∈ (Precoverage.comap F P.precoverage).coverings X ↔
    Presieve.ofArrows Y f ∈ (P.inverseImage F).precoverage.coverings X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ P.precoverage.coverings X
⊢ S.HasPullbacks f

Tactic:
have : S.HasPullbacks f := ⟨fun {W} h hh ↦ P.hasPullback _ (hS hh)⟩
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
⊢ ∃ T ∈ P.precoverage.coverings Y, T.FactorsThruAlong S f

Tactic:
⟨S.pullbackArrows f, ?_, .pullbackArrows f S⟩

Premises used: CategoryTheory.Presieve.pullbackArrows, And.intro, Exists.intro, CategoryTheory.Presieve.FactorsThruAlong.pullbackArrows
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
refine : Presieve.pullbackArrows f S ∈ P.precoverage.coverings Y
⊢ ∃ T ∈ P.precoverage.coverings Y, T.FactorsThruAlong S f

Tactic:
refine ⟨S.pullbackArrows f, ?_, .pullbackArrows f S⟩
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
Z : C
g : Z ⟶ Y
this₁ : ∀ (W : C) (a : W ⟶ X) (h : S a), P (X := pullback a f) (pullback.snd a f)
⊢ Presieve.pullbackArrows f S g → P g

Tactic:
⟨W, a, h⟩
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
Z : C
g : Z ⟶ Y
W : C
a : W ⟶ X
h : S a
⊢ HasPullback a f

Tactic:
have := S.hasPullback f h
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ P.precoverage.coverings X
this_1 : S.HasPullbacks f
Z : C
g : Z ⟶ Y
W : C
a : W ⟶ X
h : S a
this : HasPullback a f
⊢ P (X := pullback a f) (pullback.snd a f)

Tactic:
P.pullback_snd _ _ (hS h)

Premises used: CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ P.precoverage.coverings X
this_1 : S.HasPullbacks f
Z : C
g : Z ⟶ Y
W : C
a : W ⟶ X
h : S a
this : HasPullback a f
⊢ P (X := pullback a f) (pullback.snd a f)

Tactic:
exact P.pullback_snd _ _ (hS h)

Premises used: CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : HasPullbacks.{v_1, u_1} C
inst_3 : P.IsMultiplicative
⊢ P.coverage = Pretopology.toCoverage P.pretopology

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.precoverage, CategoryTheory.MorphismProperty.coverage, CategoryTheory.Pretopology.toCoverage, rfl