awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
Y X : Over S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S (P := P) 𝒰
⊢ Presieve.pullbackArrows f (𝒰.toPresieveOver (P := P)) =
    (Cover.pullbackCoverOver' (P := P) S 𝒰 (Over.Hom.left f)).toPresieveOver (P := P)

Tactic:
simpa [Cover.toPresieveOver] using
      (Presieve.ofArrows_pullback f (fun i ↦ (𝒰.X i).asOver S) (fun i ↦ (𝒰.f i).asOver S)).symm

Premises used: AlgebraicGeometry.Scheme.Hom.asOver, CategoryTheory.PreZeroHypercover.f, CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.Scheme.asOver, CategoryTheory.Presieve.ofArrows_pullback, Eq.symm, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, AlgebraicGeometry.Scheme.Cover.toPresieveOver
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S (P := P) 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver (P := P) f → Presieve Y
H :
  ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver (P := P) f),
    Membership.mem (γ := Set (Presieve Y))
      {R : Presieve Y |
        ∃ (𝒰 : Cover (precoverage P) Y.left) (x : Cover.Over S (P := P) 𝒰), R = 𝒰.toPresieveOver (P := P)}
      (T f H)
choose :
  ∀ (V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover (precoverage P) Y.left)
    (h_1 : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover.Over S (P := P) (V f H))
    (hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver (P := P) f), T f H = (V f H).toPresieveOver (P := P)),
    Membership.mem (γ := Set (Presieve X))
      {R : Presieve X |
        ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), R = 𝒰.toPresieveOver (P := P)}
      (𝒰.toPresieveOver (P := P).bind T)
⊢ Membership.mem (γ := Set (Presieve X))
    {R : Presieve X | ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), R = 𝒰.toPresieveOver (P := P)}
    (𝒰.toPresieveOver (P := P).bind T)

Tactic:
choose V h hV using H
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h_1 : Cover.Over S (P := P) 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver (P := P) f → Presieve Y
V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover (precoverage P) Y.left
h : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover.Over S (P := P) (V f H)
hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver (P := P) f), T f H = (V f H).toPresieveOver (P := P)
⊢ Membership.mem (γ := Set (Presieve X))
    {R : Presieve X | ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), R = 𝒰.toPresieveOver (P := P)}
    (𝒰.toPresieveOver (P := P).bind T)

Tactic:
⟨𝒰.bind (fun j => V ((𝒰.f j).asOver S) ⟨j⟩), inferInstance, ?_⟩

Premises used: AlgebraicGeometry.Scheme.Hom.asOver, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Presieve.ofArrows.mk, Set.Mem, setOf, inferInstance, Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.bind, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h_1 : Cover.Over S (P := P) 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver (P := P) f → Presieve Y
V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover (precoverage P) Y.left
h : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover.Over S (P := P) (V f H)
hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver (P := P) f), T f H = (V f H).toPresieveOver (P := P)
refine :
  𝒰.toPresieveOver (P := P).bind T =
    Cover.toPresieveOver (P := P) (Precoverage.ZeroHypercover.bind 𝒰 fun (j : 𝒰.I₀) ↦ V (Hom.asOver (𝒰.f j) S) ⋯)
⊢ Membership.mem (γ := Set (Presieve X))
    {R : Presieve X | ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), R = 𝒰.toPresieveOver (P := P)}
    (𝒰.toPresieveOver (P := P).bind T)

Tactic:
refine ⟨𝒰.bind (fun j => V ((𝒰.f j).asOver S) ⟨j⟩), inferInstance, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h_1 : Cover.Over S (P := P) 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver (P := P) f → Presieve Y
V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover (precoverage P) Y.left
h : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover.Over S (P := P) (V f H)
hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver (P := P) f), T f H = (V f H).toPresieveOver (P := P)
⊢ Eq.{u + 2} (α := Presieve (C := Over S) (OverClass.asOver X.left S))
    (Presieve.bind
      (Presieve.ofArrows (fun (j : 𝒰.I₀) ↦ OverClass.asOver (𝒰.X j) S) fun (j : 𝒰.I₀) ↦ Hom.asOver (𝒰.f j) S)
      fun (x : Over S) (f : x ⟶ OverClass.asOver X.left S)
        (H :
          Presieve.ofArrows (fun (j : 𝒰.I₀) ↦ OverClass.asOver (𝒰.X j) S) (fun (j : 𝒰.I₀) ↦ Hom.asOver (𝒰.f j) S) f) ↦
      Presieve.ofArrows (fun (j : (V f H).I₀) ↦ ((V f H).X j).asOver S) fun (j : (V f H).I₀) ↦
        Hom.asOver ((V f H).f j) S)
    (Presieve.ofArrows
      (fun (i : (i : 𝒰.I₀) × (V (Hom.asOver (𝒰.f i) S) ⋯).I₀) ↦
        ((V (Hom.asOver (𝒰.f (i.fst (β := fun (i : 𝒰.I₀) ↦ (V (Hom.asOver (𝒰.f i) S) ⋯).I₀))) S) ⋯).X
              (i.snd (β := fun (i : 𝒰.I₀) ↦ (V (Hom.asOver (𝒰.f i) S) ⋯).I₀))).asOver
          S)
      fun (ij : (i : 𝒰.I₀) × (V (Hom.asOver (𝒰.f i) S) ⋯).I₀) ↦
      CategoryStruct.comp (Y :=
        OverClass.asOver (𝒰.X (ij.fst (β := fun (i : 𝒰.I₀) ↦ (V (Hom.asOver (𝒰.f i) S) ⋯).I₀))) S)
        (Hom.asOver
          ((V (Hom.asOver (𝒰.f (ij.fst (β := fun (i : 𝒰.I₀) ↦ (V (Hom.asOver (𝒰.f i) S) ⋯).I₀))) S) ⋯).f
            (ij.snd (β := fun (i : 𝒰.I₀) ↦ (V (Hom.asOver (𝒰.f i) S) ⋯).I₀)))
          S)
        (Hom.asOver (𝒰.f (ij.fst (β := fun (i : 𝒰.I₀) ↦ (V (Hom.asOver (𝒰.f i) S) ⋯).I₀))) S))

Tactic:
Presieve.ofArrows_bind _ (fun j ↦ (𝒰.f j).asOver S) _ (fun Y f H j ↦ ((V f H).X j).asOver S)
        (fun Y f H j ↦ ((V f H).f j).asOver S)

Premises used: AlgebraicGeometry.Scheme.Hom.asOver, CategoryTheory.PreZeroHypercover.f, CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.Scheme.asOver, CategoryTheory.Presieve.ofArrows_bind, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h_1 : Cover.Over S (P := P) 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver (P := P) f → Presieve Y
V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover (precoverage P) Y.left
h : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover.Over S (P := P) (V f H)
hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver (P := P) f), T f H = (V f H).toPresieveOver (P := P)
h₁ :
  Presieve X = Presieve (C := Over S) (OverClass.asOver X.left S) →
    X = OverClass.asOver X.left S →
      HEq (𝒰.toPresieveOver (P := P)) (β := Presieve (C := Over S) (OverClass.asOver X.left S))
          (Presieve.ofArrows (fun (j : 𝒰.I₀) ↦ OverClass.asOver (𝒰.X j) S) fun (j : 𝒰.I₀) ↦ Hom.asOver (𝒰.f j) S) →
        ∀ (x : Over S) (x_1 : x ⟶ X) (x_2 : 𝒰.toPresieveOver (P := P) x_1),
          T x_1 x_2 =
            Presieve.ofArrows (fun (j : (V x_1 x_2).I₀) ↦ ((V x_1 x_2).X j).asOver S) fun (j : (V x_1 x_2).I₀) ↦
              Hom.asOver ((V x_1 x_2).f j) S
⊢ 𝒰.toPresieveOver (P := P).bind T =
    Cover.toPresieveOver (P := P) (Precoverage.ZeroHypercover.bind 𝒰 fun (j : 𝒰.I₀) ↦ V (Hom.asOver (𝒰.f j) S) ⋯)

Tactic:
convert!
      Presieve.ofArrows_bind _ (fun j ↦ (𝒰.f j).asOver S) _ (fun Y f H j ↦ ((V f H).X j).asOver S)
        (fun Y f H j ↦ ((V f H).f j).asOver S)

Premises used: AlgebraicGeometry.Scheme.Hom.asOver, CategoryTheory.PreZeroHypercover.f, CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.Scheme.asOver, CategoryTheory.Presieve.ofArrows_bind, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
𝒰 : Cover (precoverage P) X.left
h_1 : Cover.Over S (P := P) 𝒰
T : ⦃Y : Over S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOver (P := P) f → Presieve Y
V : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover (precoverage P) Y.left
h : ⦃Y : Over S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOver (P := P) f) → Cover.Over S (P := P) (V f H)
hV : ∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOver (P := P) f), T f H = (V f H).toPresieveOver (P := P)
e_1 : Presieve X = Presieve (C := Over S) (OverClass.asOver X.left S)
e_3 : X = OverClass.asOver X.left S
e_4 :
  HEq (𝒰.toPresieveOver (P := P)) (β := Presieve (C := Over S) (OverClass.asOver X.left S))
    (Presieve.ofArrows (fun (j : 𝒰.I₀) ↦ OverClass.asOver (𝒰.X j) S) fun (j : 𝒰.I₀) ↦ Hom.asOver (𝒰.f j) S)
x : Over S
x_1 : x ⟶ X
h_2 : 𝒰.toPresieveOver (P := P) x_1
⊢ T x_1 h_2 =
    Presieve.ofArrows (fun (j : (V x_1 h_2).I₀) ↦ ((V x_1 h_2).X j).asOver S) fun (j : (V x_1 h_2).I₀) ↦
      Hom.asOver ((V x_1 h_2).f j) S

Tactic:
apply hV
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
h :
  ∀ (X : Over S) (R : Sieve X),
    R ∈ (overGrothendieckTopology P S : (a : Over S) → Set (Sieve a)) X ↔
      R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
⊢ overGrothendieckTopology P S = (overPretopology P S).toGrothendieck

Tactic:
ext X R
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
h :
  Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
      ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
      ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left) →
    R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
h₁ :
  R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X →
    Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
      ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
      ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left)
⊢ Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
      ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
      ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left) ↔
    R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
hR :
  Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
    ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
    ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left)
h :
  ∀ (𝒰 : Cover (precoverage P) X.left)
    (hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)),
    R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
⊢ R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X

Tactic:
obtain ⟨𝒰, hle⟩ := exists_cover_of_mem_grothendieckTopology hR

Premises used: AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
hR :
  Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
    ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
    ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left)
𝒰 : Cover (precoverage P) X.left
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
h :
  ∀
    (hR :
      ∃ (𝒰 : Cover (precoverage P) X.left),
        Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R))
    (𝒰 : Cover (precoverage P) X.left)
    (hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)),
    R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
⊢ R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X

Tactic:
rw [mem_grothendieckTopology_iff] at hR

Premises used: AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
hR :
  ∃ (𝒰 : Cover (precoverage P) X.left),
    Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
𝒰 : Cover (precoverage P) X.left
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
this_1 : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun (i : 𝒰.I₀) ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) inferInstance ⋯
right : 𝒰.toPresieveOver (P := P) ≤ R.arrows
⊢ R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X

Tactic:
use 𝒰.toPresieveOver, ⟨𝒰, inferInstance, rfl⟩

Premises used: AlgebraicGeometry.Scheme.Cover.toPresieveOver
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
hR :
  ∃ (𝒰 : Cover (precoverage P) X.left),
    Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
𝒰 : Cover (precoverage P) X.left
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
this_1 : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun (i : 𝒰.I₀) ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) inferInstance ⋯
right right₁ right₂ right₃ :
  Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
⊢ 𝒰.toPresieveOver (P := P) ≤ R.arrows

Tactic:
rwa [Cover.toPresieveOver_le_arrows_iff]

Premises used: AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S (P := P) 𝒰
hT : 𝒰.toPresieveOver (P := P) ≤ R.arrows
h₁ :
  ∃ (𝒰 : Cover (precoverage P) X.left),
    Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
⊢ Membership.mem (α := Sieve X.left) (γ := Set (Sieve X.left))
    ((grothendieckTopology P : (a : Scheme) → Set (Sieve a)) X.left)
    ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R : Sieve X.left)

Tactic:
rw [mem_grothendieckTopology_iff]

Premises used: AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S (P := P) 𝒰
hT : 𝒰.toPresieveOver (P := P) ≤ R.arrows
h₁ : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
⊢ ∃ (𝒰 : Cover (precoverage P) X.left),
    Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)

Tactic:
use 𝒰
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S (P := P) 𝒰
hT : 𝒰.toPresieveOver (P := P) ≤ R.arrows
h₁ h₂ h₃ h₄ :
  ∀ (hT : Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)),
    Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)
⊢ Presieve.ofArrows 𝒰.X 𝒰.f ≤ Sieve.arrows ((Sieve.overEquiv X : (a : Sieve X) → Sieve X.left) R)

Tactic:
rwa [Cover.toPresieveOver_le_arrows_iff] at hT

Premises used: AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
rw :
  R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X ↔
    ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), 𝒰.toPresieveOver (P := P) ≤ R.arrows
⊢ R ∈ (overGrothendieckTopology P S : (a : Over S) → Set (Sieve a)) X ↔
    ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), 𝒰.toPresieveOver (P := P) ≤ R.arrows

Tactic:
rw [overGrothendieckTopology_eq_toGrothendieck_overPretopology]

Premises used: AlgebraicGeometry.Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopology
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
mp :
  R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X →
    ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), 𝒰.toPresieveOver (P := P) ≤ R.arrows
mpr :
  (∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), 𝒰.toPresieveOver (P := P) ≤ R.arrows) →
    R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X
⊢ R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X ↔
    ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), 𝒰.toPresieveOver (P := P) ≤ R.arrows

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S (P := P) 𝒰
hle : 𝒰.toPresieveOver (P := P) ≤ R.arrows
w : Cover (precoverage P) X.left
w₁ : Cover.Over S (P := P) 𝒰
h₁ : 𝒰.toPresieveOver (P := P) ≤ R.arrows
⊢ ∃ (𝒰 : Cover (precoverage P) X.left) (x : Cover.Over S (P := P) 𝒰), 𝒰.toPresieveOver (P := P) ≤ R.arrows

Tactic:
use 𝒰, h
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h𝒰 : Cover.Over S (P := P) 𝒰
hle : 𝒰.toPresieveOver (P := P) ≤ R.arrows
⊢ R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X

Tactic:
⟨𝒰.toPresieveOver, ⟨𝒰, h𝒰, rfl⟩, hle⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, rfl, AlgebraicGeometry.Scheme.Cover.toPresieveOver
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h𝒰 : Cover.Over S (P := P) 𝒰
hle : 𝒰.toPresieveOver (P := P) ≤ R.arrows
⊢ R ∈ ((overPretopology P S).toGrothendieck : (a : Over S) → Set (Sieve a)) X

Tactic:
exact ⟨𝒰.toPresieveOver, ⟨𝒰, h𝒰, rfl⟩, hle⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P Q : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
inst_3 : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X)
hT :
  Membership.mem (γ := Set (Sieve (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X)))
    ((overGrothendieckTopology P S : (a : Over S) → Set (Sieve a)) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X))
    T
rw :
  ∀
    (hT_1 :
      ∃ (𝒰 : Cover (precoverage P) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left) (x :
        Cover.Over S (P := P) 𝒰), 𝒰.toPresieveOver (P := P) ≤ T.arrows),
    ∃ (𝒰 : Cover (precoverage P) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left) (x :
      Cover.Over S (P := P) 𝒰),
      𝒰.toPresieveOver (P := P) ≤
        Sieve.arrows
          (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
            (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S)
              (↑(Subtype.mk (p := fun (x : Sieve (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X)) ↦
                    Membership.mem (γ := Set (Sieve (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X)))
                      ((overGrothendieckTopology P S : (a : Over S) → Set (Sieve a))
                        (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X))
                      x)
                    T hT) :
                Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X))))
⊢ Membership.mem (γ := Set (Sieve (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X)))
    ((overGrothendieckTopology P S : (a : Over S) → Set (Sieve a)) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X))
    (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S)
      (Sieve.functorPullback (MorphismProperty.Over.forget Q ⊤ S)
        (↑(Subtype.mk (p := fun (x : Sieve (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X)) ↦
              Membership.mem (γ := Set (Sieve (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X)))
                ((overGrothendieckTopology P S : (a : Over S) → Set (Sieve a))
                  (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X))
                x)
              T hT) :
          Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X))))

Tactic:
rw [mem_overGrothendieckTopology] at hT ⊢

Premises used: AlgebraicGeometry.Scheme.mem_overGrothendieckTopology