awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{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
inst_2 : F.PreservesPairwisePullbacks R
inst_3 : R.HasPairwisePullbacks
Y Z : D
f : Y ⟶ F.obj X
h : map F R f
g : Z ⟶ F.obj X
h_1 : map F R g
Y_1 : C
u : Y_1 ⟶ X
hf : R u
Y_2 : C
u_1 : Y_2 ⟶ X
hg : R u_1
⊢ HasPullback u u_1

Tactic:
have := Presieve.HasPairwisePullbacks.has_pullbacks hf hg
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{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
inst_2 : F.PreservesPairwisePullbacks R
inst_3 : R.HasPairwisePullbacks
Y Z : D
f : Y ⟶ F.obj X
h : map F R f
g : Z ⟶ F.obj X
h_1 : map F R g
Y_1 : C
u : Y_1 ⟶ X
hf : R u
Y_2 : C
u_1 : Y_2 ⟶ X
hg : R u_1
this : HasPullback u u_1
⊢ PreservesLimit (cospan u u_1) F

Tactic:
have := F.preservesLimit_cospan_of_mem_presieve _ hf hg
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{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
inst_2 : F.PreservesPairwisePullbacks R
inst_3 : R.HasPairwisePullbacks
Y Z : D
f : Y ⟶ F.obj X
h : map F R f
g : Z ⟶ F.obj X
h_1 : map F R g
Y_1 : C
u : Y_1 ⟶ X
hf : R u
Y_2 : C
u_1 : Y_2 ⟶ X
hg : R u_1
this_1 : HasPullback u u_1
this : PreservesLimit (cospan u u_1) F
⊢ HasPullback (F.map u) (F.map u_1)

Tactic:
hasPullback_of_preservesPullback F _ _

Premises used: CategoryTheory.Limits.hasPullback_of_preservesPullback
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{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
inst_2 : F.PreservesPairwisePullbacks R
inst_3 : R.HasPairwisePullbacks
Y Z : D
f : Y ⟶ F.obj X
h : map F R f
g : Z ⟶ F.obj X
h_1 : map F R g
Y_1 : C
u : Y_1 ⟶ X
hf : R u
Y_2 : C
u_1 : Y_2 ⟶ X
hg : R u_1
this_1 : HasPullback u u_1
this : PreservesLimit (cospan u u_1) F
⊢ HasPullback (F.map u) (F.map u_1)

Tactic:
exact hasPullback_of_preservesPullback F _ _

Premises used: CategoryTheory.Limits.hasPullback_of_preservesPullback
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
X : C
S : Sieve.{u_1, u_2} X
⊢ S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X ↔ J.Saturate X S

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
X : C
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
⊢ Sieve.generate R ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X

Tactic:
.of _ _ hR

Premises used: Set.Mem, setOf, CategoryTheory.Precoverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
⊢ J.toGrothendieck =
    sInf
      {K : GrothendieckTopology.{u_1, u_2} C |
        ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
refine_1 :
  J.toGrothendieck ≤
    sInf
      {K : GrothendieckTopology.{u_1, u_2} C |
        ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
refine_2 :
  sInf
      {K : GrothendieckTopology.{u_1, u_2} C |
        ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X} ≤
    J.toGrothendieck
⊢ J.toGrothendieck =
    sInf
      {K : GrothendieckTopology.{u_1, u_2} C |
        ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
refine_1 :
  ∀ (b : GrothendieckTopology.{u_1, u_2} C),
    Membership.mem (γ := Set (GrothendieckTopology.{u_1, u_2} C))
        {K : GrothendieckTopology.{u_1, u_2} C |
          ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
        b →
      J.toGrothendieck ≤ b
⊢ J.toGrothendieck ≤
    sInf
      {K : GrothendieckTopology.{u_1, u_2} C |
        ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}

Tactic:
rw [le_sInf_iff]

Premises used: le_sInf_iff
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
K : GrothendieckTopology.{u_1, u_2} C
hK :
  Membership.mem (γ := Set (GrothendieckTopology.{u_1, u_2} C))
    {K : GrothendieckTopology.{u_1, u_2} C |
      ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
    K
refine_1 : ∀ (i : C), (J.toGrothendieck : (a : C) → Set (Sieve a)) i ≤ (K : (a : C) → Set (Sieve a)) i
⊢ J.toGrothendieck ≤ K

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
K : GrothendieckTopology.{u_1, u_2} C
hK :
  Membership.mem (γ := Set (GrothendieckTopology.{u_1, u_2} C))
    {K : GrothendieckTopology.{u_1, u_2} C |
      ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
    K
i : C
refine_1 :
  ∀ ⦃a : Sieve.{u_1, u_2} i⦄, a ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) i → a ∈ (K : (a : C) → Set (Sieve a)) i
⊢ (J.toGrothendieck : (a : C) → Set (Sieve a)) i ≤ (K : (a : C) → Set (Sieve a)) i

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
K : GrothendieckTopology.{u_1, u_2} C
hK :
  Membership.mem (γ := Set (GrothendieckTopology.{u_1, u_2} C))
    {K : GrothendieckTopology.{u_1, u_2} C |
      ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
    K
i : C
a : Sieve.{u_1, u_2} i
X : C
S : Presieve.{u_1, u_2} X
hS : S ∈ J.coverings X
⊢ Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X

Tactic:
hK _ hS
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
K : GrothendieckTopology.{u_1, u_2} C
hK :
  Membership.mem (γ := Set (GrothendieckTopology.{u_1, u_2} C))
    {K : GrothendieckTopology.{u_1, u_2} C |
      ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
    K
i : C
a : Sieve.{u_1, u_2} i
X : C
S : Presieve.{u_1, u_2} X
hS : S ∈ J.coverings X
⊢ Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X

Tactic:
exact hK _ hS
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
K : GrothendieckTopology.{u_1, u_2} C
hK :
  Membership.mem (γ := Set (GrothendieckTopology.{u_1, u_2} C))
    {K : GrothendieckTopology.{u_1, u_2} C |
      ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
    K
i : C
a : Sieve.{u_1, u_2} i
X : C
⊢ ⊤ ∈ (K : (a : C) → Set (Sieve a)) X

Tactic:
K.top_mem _

Premises used: CategoryTheory.GrothendieckTopology.top_mem
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
K : GrothendieckTopology.{u_1, u_2} C
hK :
  Membership.mem (γ := Set (GrothendieckTopology.{u_1, u_2} C))
    {K : GrothendieckTopology.{u_1, u_2} C |
      ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
    K
i : C
a : Sieve.{u_1, u_2} i
X : C
⊢ ⊤ ∈ (K : (a : C) → Set (Sieve a)) X

Tactic:
exact K.top_mem _

Premises used: CategoryTheory.GrothendieckTopology.top_mem
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
K : GrothendieckTopology.{u_1, u_2} C
hK :
  Membership.mem (γ := Set (GrothendieckTopology.{u_1, u_2} C))
    {K : GrothendieckTopology.{u_1, u_2} C |
      ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
    K
i : C
a : Sieve.{u_1, u_2} i
X : C
S : Sieve.{u_1, u_2} X
h : J.Saturate X S
Y : C
f : Y ⟶ X
ih : S ∈ (K : (a : C) → Set (Sieve a)) X
⊢ Sieve.pullback f S ∈ (K : (a : C) → Set (Sieve a)) Y

Tactic:
K.pullback_stable _ ih

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
K : GrothendieckTopology.{u_1, u_2} C
hK :
  Membership.mem (γ := Set (GrothendieckTopology.{u_1, u_2} C))
    {K : GrothendieckTopology.{u_1, u_2} C |
      ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
    K
i : C
a : Sieve.{u_1, u_2} i
X : C
S : Sieve.{u_1, u_2} X
h : J.Saturate X S
Y : C
f : Y ⟶ X
ih : S ∈ (K : (a : C) → Set (Sieve a)) X
⊢ Sieve.pullback f S ∈ (K : (a : C) → Set (Sieve a)) Y

Tactic:
exact K.pullback_stable _ ih

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
K : GrothendieckTopology.{u_1, u_2} C
hK :
  Membership.mem (γ := Set (GrothendieckTopology.{u_1, u_2} C))
    {K : GrothendieckTopology.{u_1, u_2} C |
      ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
    K
i : C
a : Sieve.{u_1, u_2} i
X : C
S R : Sieve.{u_1, u_2} X
h : J.Saturate X S
h_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f R)
ih1 : S ∈ (K : (a : C) → Set (Sieve a)) X
ih2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (K : (a : C) → Set (Sieve a)) Y
⊢ R ∈ (K : (a : C) → Set (Sieve a)) X

Tactic:
K.transitive ih1 _ ih2

Premises used: CategoryTheory.GrothendieckTopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
K : GrothendieckTopology.{u_1, u_2} C
hK :
  Membership.mem (γ := Set (GrothendieckTopology.{u_1, u_2} C))
    {K : GrothendieckTopology.{u_1, u_2} C |
      ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
    K
i : C
a : Sieve.{u_1, u_2} i
X : C
S R : Sieve.{u_1, u_2} X
h : J.Saturate X S
h_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f R)
ih1 : S ∈ (K : (a : C) → Set (Sieve a)) X
ih2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (K : (a : C) → Set (Sieve a)) Y
⊢ R ∈ (K : (a : C) → Set (Sieve a)) X

Tactic:
exact K.transitive ih1 _ ih2

Premises used: CategoryTheory.GrothendieckTopology.transitive
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
K : GrothendieckTopology.{u_1, u_2} C
hK :
  Membership.mem (γ := Set (GrothendieckTopology.{u_1, u_2} C))
    {K : GrothendieckTopology.{u_1, u_2} C |
      ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X}
    K
i : C
a : Sieve.{u_1, u_2} i
hS : a ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) i
refine_1 :
  ∀ (X : C) (S : Presieve.{u_1, u_2} X) (hS : S ∈ J.coverings X), Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X
refine_1₁ : ∀ (X : C), ⊤ ∈ (K : (a : C) → Set (Sieve a)) X
refine_1₂ :
  ∀ (X : C) (S : Sieve.{u_1, u_2} X),
    J.Saturate X S →
      ∀ (Y : C) (f : Y ⟶ X) (ih : S ∈ (K : (a : C) → Set (Sieve a)) X),
        Sieve.pullback f S ∈ (K : (a : C) → Set (Sieve a)) Y
refine_1₃ :
  ∀ (X : C) (S R : Sieve.{u_1, u_2} X),
    J.Saturate X S →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f R)) →
        ∀ (ih1 : S ∈ (K : (a : C) → Set (Sieve a)) X)
          (ih2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (K : (a : C) → Set (Sieve a)) Y),
          R ∈ (K : (a : C) → Set (Sieve a)) X
⊢ a ∈ (K : (a : C) → Set (Sieve a)) i

Tactic:
induction hS with
    | of _ _ hS => exact hK _ hS
    | top => exact K.top_mem _
    | pullback _ _ _ _ _ ih => exact K.pullback_stable _ ih
    | transitive _ _ _ _ _ ih1 ih2 => exact K.transitive ih1 _ ih2

Premises used: CategoryTheory.GrothendieckTopology.top_mem
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
⊢ sInf
      {K : GrothendieckTopology.{u_1, u_2} C |
        ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X} ≤
    J.toGrothendieck

Tactic:
sInf_le (fun _ _ hS => .of _ _ hS)

Premises used: sInf_le, CategoryTheory.Precoverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
⊢ sInf
      {K : GrothendieckTopology.{u_1, u_2} C |
        ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ (K : (a : C) → Set (Sieve a)) X} ≤
    J.toGrothendieck

Tactic:
exact sInf_le (fun _ _ hS => .of _ _ hS)
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
mp :
  Presieve.IsSheaf J.toGrothendieck P →
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
mpr :
  (∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows) →
    Presieve.IsSheaf J.toGrothendieck P
⊢ Presieve.IsSheaf J.toGrothendieck P ↔
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
⊢ Presieve.IsSheaf J.toGrothendieck P →
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows

Tactic:
fun H _ _ _ _ hR => ?_
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
mp :
  ∀ (H : Presieve.IsSheaf J.toGrothendieck P) (x x_1 : C) (x_2 : x_1 ⟶ x) (x_3 : Presieve.{u_2, u_3} x)
    (hR : x_3 ∈ J.coverings x), Presieve.IsSheafFor P (Sieve.pullback x_2 (Sieve.generate x_3)).arrows
⊢ Presieve.IsSheaf J.toGrothendieck P →
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows

Tactic:
refine fun H _ _ _ _ hR => ?_
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : Presieve.IsSheaf J.toGrothendieck P
x x_1 : C
x_2 : x_1 ⟶ x
x_3 : Presieve.{u_2, u_3} x
hR : x_3 ∈ J.coverings x
mp : Sieve.generate (Sieve.pullback x_2 (Sieve.generate x_3)).arrows ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) x_1
⊢ Presieve.IsSheafFor P (Sieve.pullback x_2 (Sieve.generate x_3)).arrows

Tactic:
apply H.isSheafFor

Premises used: CategoryTheory.Presieve.IsSheaf.isSheafFor
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : Presieve.IsSheaf J.toGrothendieck P
x x_1 : C
x_2 : x_1 ⟶ x
x_3 : Presieve.{u_2, u_3} x
hR : x_3 ∈ J.coverings x
mp : Sieve.pullback x_2 (Sieve.generate x_3) ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) x_1
⊢ Sieve.generate (Sieve.pullback x_2 (Sieve.generate x_3)).arrows ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) x_1

Tactic:
rw [Sieve.generate_sieve]

Premises used: CategoryTheory.Sieve.generate_sieve
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : Presieve.IsSheaf J.toGrothendieck P
x x_1 : C
x_2 : x_1 ⟶ x
x_3 : Presieve.{u_2, u_3} x
hR : x_3 ∈ J.coverings x
⊢ Sieve.pullback x_2 (Sieve.generate x_3) ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) x_1

Tactic:
J.toGrothendieck.pullback_stable _ (Saturate.of _ _ hR)

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Precoverage.toGrothendieck, CategoryTheory.Precoverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : Presieve.IsSheaf J.toGrothendieck P
x x_1 : C
x_2 : x_1 ⟶ x
x_3 : Presieve.{u_2, u_3} x
hR : x_3 ∈ J.coverings x
⊢ Sieve.pullback x_2 (Sieve.generate x_3) ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) x_1

Tactic:
exact J.toGrothendieck.pullback_stable _ (Saturate.of _ _ hR)

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Precoverage.toGrothendieck, CategoryTheory.Precoverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Sieve.{u_2, u_3} X
hS : S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
this : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
simpa using this (f := 𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Sieve.{u_2, u_3} X
hS : S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
mpr : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
suffices ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (S.pullback f).arrows by
      simpa using this (f := 𝟙 _)
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X_1 : C
S_1 : Sieve.{u_2, u_3} X_1
X : C
S : Presieve.{u_2, u_3} X
hS : S ∈ J.coverings X
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows

Tactic:
fun _ _ => H S hS
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X_1 : C
S_1 : Sieve.{u_2, u_3} X_1
X : C
S : Presieve.{u_2, u_3} X
hS : S ∈ J.coverings X
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows

Tactic:
exact fun _ _ => H S hS
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Sieve.{u_2, u_3} X
X_1 : C
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X_1), Presieve.IsSheafFor P (Sieve.pullback f ⊤).arrows

Tactic:
simp [Presieve.isSheafFor_top P]

Premises used: CategoryTheory.Presieve.isSheafFor_top
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X_1 : C
S_1 : Sieve.{u_2, u_3} X_1
X : C
S : Sieve.{u_2, u_3} X
hS : J.Saturate X S
Y_1 : C
f_1 : Y_1 ⟶ X
ih : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
Y : C
f : Y ⟶ Y_1
mpr : Presieve.IsSheafFor P (Sieve.pullback (f ≫ f_1) S).arrows
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback f_1 S)).arrows

Tactic:
rw [← S.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X_1 : C
S_1 : Sieve.{u_2, u_3} X_1
X : C
S : Sieve.{u_2, u_3} X
hS : J.Saturate X S
Y_1 : C
f_1 : Y_1 ⟶ X
ih : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
Y : C
f : Y ⟶ Y_1
⊢ Presieve.IsSheafFor P (Sieve.pullback (f ≫ f_1) S).arrows

Tactic:
ih (f ≫ _)

Premises used: CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X_1 : C
S_1 : Sieve.{u_2, u_3} X_1
X : C
S : Sieve.{u_2, u_3} X
hS : J.Saturate X S
Y_1 : C
f_1 : Y_1 ⟶ X
ih : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
Y : C
f : Y ⟶ Y_1
⊢ Presieve.IsSheafFor P (Sieve.pullback (f ≫ f_1) S).arrows

Tactic:
exact ih (f ≫ _)

Premises used: CategoryTheory.CategoryStruct.comp