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
inst_3 : Q.IsStableUnderComposition
hPQ : P ≤ Q
X : Q.Over ⊤ S
T : Sieve (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X)
hT_1 :
  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
hT :
  ∃ (𝒰 : Cover (precoverage P) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left) (x : Cover.Over S (P := P) 𝒰),
    𝒰.toPresieveOver (P := P) ≤ T.arrows
obtain :
  ∀ (𝒰 : Cover (precoverage P) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left) (h : Cover.Over S (P := P) 𝒰)
    (hle : 𝒰.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_1) :
                Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X))))
⊢ ∃ (𝒰 : 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_1) :
              Sieve ((MorphismProperty.Over.forget Q ⊤ S).obj X))))

Tactic:
obtain ⟨𝒰, h, hle⟩ := hT
-- 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
𝒰 : Cover (precoverage P) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left
h : Cover.Over S (P := P) 𝒰
hle : 𝒰.toPresieveOver (P := P) ≤ T.arrows
h₁ :
  𝒰.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))))
⊢ ∃ (𝒰 : 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))))

Tactic:
use 𝒰, h
-- 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
𝒰 : Cover (precoverage P) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left
h : Cover.Over S (P := P) 𝒰
hle : 𝒰.toPresieveOver (P := P) ≤ T.arrows
Y : Over S
i : 𝒰.I₀
rw : Q (𝒰.f i ≫ (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left ↘ S)
⊢ Q (𝒰.X i ↘ S)

Tactic:
rw [← comp_over (𝒰.f i) S]

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.comp_over, 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
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
𝒰 : Cover (precoverage P) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left
h : Cover.Over S (P := P) 𝒰
hle : 𝒰.toPresieveOver (P := P) ≤ T.arrows
Y : Over S
i : 𝒰.I₀
⊢ Q (𝒰.f i ≫ (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left ↘ S)

Tactic:
Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop i) X.prop

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.Comma.prop, AlgebraicGeometry.Scheme.Cover.map_prop
-- 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
𝒰 : Cover (precoverage P) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left
h : Cover.Over S (P := P) 𝒰
hle : 𝒰.toPresieveOver (P := P) ≤ T.arrows
Y : Over S
i : 𝒰.I₀
⊢ Q (𝒰.f i ≫ (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left ↘ S)

Tactic:
exact Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop i) X.prop

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.Comma.prop, AlgebraicGeometry.Scheme.Cover.map_prop
-- 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
𝒰 : Cover (precoverage P) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left
h : Cover.Over S (P := P) 𝒰
hle : 𝒰.toPresieveOver (P := P) ≤ T.arrows
Y : Over S
i : 𝒰.I₀
⊢ Q (𝒰.X i ↘ S)

Tactic:
have p : Q (𝒰.X i ↘ S) := by
      rw [← comp_over (𝒰.f i) S]
      exact Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop i) X.prop
-- 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
𝒰 : Cover (precoverage P) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left
h : Cover.Over S (P := P) 𝒰
hle : 𝒰.toPresieveOver (P := P) ≤ T.arrows
Y : Over S
i : 𝒰.I₀
p : Q (𝒰.X i ↘ S)
h₁ :
  (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))).arrows
      (Y := (𝒰.X i).asOverProp (P := Q) S p) (MorphismProperty.Over.homMk (P := Q) (Q := ⊤) (𝒰.f i) ⋯ True.intro) ∧
    Eq (α := (𝒰.X i).asOver S ⟶ Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X) (Hom.asOver (𝒰.f i) S)
      (𝟙 ((𝒰.X i).asOver S) ≫
        CategoryTheory.Functor.map (MorphismProperty.Over.forget Q ⊤ S)
          (MorphismProperty.Over.homMk (P := Q) (Q := ⊤) (𝒰.f i) ⋯ True.intro))
⊢ Sieve.arrows (X := 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))))
    (Y := (𝒰.X i).asOver S) (Hom.asOver (𝒰.f i) S)

Tactic:
use (𝒰.X i).asOverProp S p, MorphismProperty.Over.homMk (𝒰.f i) (comp_over (𝒰.f i) S), 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.PreZeroHypercover.X, CategoryTheory.MorphismProperty.Over.homMk, AlgebraicGeometry.Scheme.asOverProp, 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
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
𝒰 : Cover (precoverage P) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left
h : Cover.Over S (P := P) 𝒰
hle : 𝒰.toPresieveOver (P := P) ≤ T.arrows
Y : Over S
i : 𝒰.I₀
p : Q (𝒰.X i ↘ 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))).arrows
      (Y := (𝒰.X i).asOverProp (P := Q) S p) (MorphismProperty.Over.homMk (P := Q) (Q := ⊤) (𝒰.f i) ⋯ True.intro) ∧
    Eq (α := (𝒰.X i).asOver S ⟶ Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X) (Hom.asOver (𝒰.f i) S)
      (𝟙 ((𝒰.X i).asOver S) ≫
        CategoryTheory.Functor.map (MorphismProperty.Over.forget Q ⊤ S)
          (MorphismProperty.Over.homMk (P := Q) (Q := ⊤) (𝒰.f i) ⋯ True.intro))

Tactic:
⟨hle _ _ ⟨i⟩, rfl⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, And.intro, rfl
-- 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
𝒰 : Cover (precoverage P) (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left
h : Cover.Over S (P := P) 𝒰
hle : 𝒰.toPresieveOver (P := P) ≤ T.arrows
Y : Over S
i : 𝒰.I₀
p : Q (𝒰.X i ↘ 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))).arrows
      (Y := (𝒰.X i).asOverProp (P := Q) S p) (MorphismProperty.Over.homMk (P := Q) (Q := ⊤) (𝒰.f i) ⋯ True.intro) ∧
    Eq (α := (𝒰.X i).asOver S ⟶ Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X) (Hom.asOver (𝒰.f i) S)
      (𝟙 ((𝒰.X i).asOver S) ≫
        CategoryTheory.Functor.map (MorphismProperty.Over.forget Q ⊤ S)
          (MorphismProperty.Over.homMk (P := Q) (Q := ⊤) (𝒰.f i) ⋯ True.intro))

Tactic:
exact ⟨hle _ _ ⟨i⟩, rfl⟩
-- 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
⊢ Functor.LocallyCoverDense (C := P.Over ⊤ S) (MorphismProperty.Over.forget P ⊤ S) (overGrothendieckTopology P S)

Tactic:
locallyCoverDense_of_le S le_rfl

Premises used: le_rfl, AlgebraicGeometry.Scheme.locallyCoverDense_of_le
-- 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
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left
h : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ Membership.mem (γ := Set (Presieve X))
    {R : Presieve X |
      ∃ (𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
        ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp (P := P) (Q := Q) h}
    (Presieve.pullbackArrows f (𝒰.toPresieveOverProp (P := P) (Q := Q) p))

Tactic:
⟨𝒰.pullbackCoverOverProp' S f.left (Q := Q) Y.prop X.prop p, inferInstance, ?_, ?_⟩

Premises used: Set.Mem, setOf, inferInstance, CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.CommaMorphism.left, Exists.intro, CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism, AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'
-- 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
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left
h : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
refine_1 :
  ∀
    (j :
      (Cover.pullbackCoverOverProp' (P := P) S 𝒰 f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (Q := Q) ⋯ ⋯ p).I₀),
    Q
      ((Cover.pullbackCoverOverProp' (P := P) S 𝒰 f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (Q := Q) ⋯ ⋯ p).X
          j ↘
        S)
refine_2 :
  Presieve.pullbackArrows f (𝒰.toPresieveOverProp (P := P) (Q := Q) p) =
    (Cover.pullbackCoverOverProp' (P := P) S 𝒰 f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (Q := Q) ⋯ ⋯
          p).toPresieveOverProp
      (P := P) (Q := Q) ⋯
⊢ Membership.mem (γ := Set (Presieve X))
    {R : Presieve X |
      ∃ (𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
        ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp (P := P) (Q := Q) h}
    (Presieve.pullbackArrows f (𝒰.toPresieveOverProp (P := P) (Q := Q) p))

Tactic:
refine ⟨𝒰.pullbackCoverOverProp' S f.left (Q := Q) Y.prop X.prop p, inferInstance, ?_, ?_⟩
-- 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
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left
h : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j : (Cover.pullbackCoverOverProp' (P := P) S 𝒰 f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (Q := Q) ⋯ ⋯ p).I₀
⊢ Q
    ((Cover.pullbackCoverOverProp' (P := P) S 𝒰 f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (Q := Q) ⋯ ⋯ p).X j ↘
      S)

Tactic:
apply MorphismProperty.Comma.prop

Premises used: CategoryTheory.MorphismProperty.Comma.prop
-- 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
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left
h : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ Presieve.pullbackArrows f (𝒰.toPresieveOverProp (P := P) (Q := Q) p) =
    (Cover.pullbackCoverOverProp' (P := P) S 𝒰 f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (Q := Q) ⋯ ⋯
          p).toPresieveOverProp
      (P := P) (Q := Q) ⋯

Tactic:
(Presieve.ofArrows_pullback f (fun i ↦ ⟨(𝒰.X i).asOver S, p i⟩)
        (fun i ↦ ⟨(𝒰.f i).asOver S, trivial, trivial⟩)).symm

Premises used: CategoryTheory.Limits.limit.π, AlgebraicGeometry.Scheme.Hom.asOver, CategoryTheory.PreZeroHypercover.f, trivial, CategoryTheory.Over.mk, CategoryTheory.over, CategoryTheory.PreZeroHypercover.X, CategoryTheory.CostructuredArrow.homMk, AlgebraicGeometry.Scheme.asOver, CategoryTheory.Over.homMk, CategoryTheory.Presieve.ofArrows_pullback, CategoryTheory.Limits.limit, CategoryTheory.MorphismProperty.Comma.mk, CategoryTheory.OverClass.asOver, CategoryTheory.CostructuredArrow.mk, CategoryTheory.OverClass.asOverHom, AlgebraicGeometry.Scheme.Cover.toPresieveOverProp, CategoryTheory.MorphismProperty.Comma.Hom.mk, Eq.symm, 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
inst_3 : Q.IsStableUnderComposition
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left
h : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ Presieve.pullbackArrows f (𝒰.toPresieveOverProp (P := P) (Q := Q) p) =
    (Cover.pullbackCoverOverProp' (P := P) S 𝒰 f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (Q := Q) ⋯ ⋯
          p).toPresieveOverProp
      (P := P) (Q := Q) ⋯

Tactic:
exact (Presieve.ofArrows_pullback f (fun i ↦ ⟨(𝒰.X i).asOver S, p i⟩)
        (fun i ↦ ⟨(𝒰.f i).asOver S, trivial, trivial⟩)).symm

Premises used: AlgebraicGeometry.Scheme.Hom.asOver, CategoryTheory.PreZeroHypercover.f, trivial, CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.Scheme.asOver, CategoryTheory.Presieve.ofArrows_pullback, CategoryTheory.MorphismProperty.Comma.mk, CategoryTheory.MorphismProperty.Comma.Hom.mk, Eq.symm, 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
inst_3 : Q.IsStableUnderComposition
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left
h : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
T : ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → 𝒰.toPresieveOverProp (P := P) (Q := Q) p f → Presieve Y
H :
  ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp (P := P) (Q := Q) p f),
    Membership.mem (γ := Set (Presieve Y))
      {R : Presieve Y |
        ∃ (𝒰 : Cover (precoverage P) Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
          ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp (P := P) (Q := Q) h}
      (T f H)
choose :
  ∀
    (V :
      ⦃Y : Q.Over ⊤ S⦄ →
        (f : Y ⟶ X) →
          (H : 𝒰.toPresieveOverProp (P := P) (Q := Q) p f) →
            Cover (precoverage P) Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left)
    (h_1 :
      ⦃Y : Q.Over ⊤ S⦄ → (f : Y ⟶ X) → (H : 𝒰.toPresieveOverProp (P := P) (Q := Q) p f) → Cover.Over S (P := P) (V f H))
    (pV :
      ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp (P := P) (Q := Q) p f) (j : (V f H).I₀),
        Q ((V f H).X j ↘ S))
    (hV :
      ∀ ⦃Y : Q.Over ⊤ S⦄ (f : Y ⟶ X) (H : 𝒰.toPresieveOverProp (P := P) (Q := Q) p f),
        T f H = (V f H).toPresieveOverProp (P := P) (Q := Q) ⋯),
    Membership.mem (γ := Set (Presieve X))
      {R : Presieve X |
        ∃ (𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
          ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp (P := P) (Q := Q) h}
      ((𝒰.toPresieveOverProp (P := P) (Q := Q) p).bind T)
⊢ Membership.mem (γ := Set (Presieve X))
    {R : Presieve X |
      ∃ (𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
        ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp (P := P) (Q := Q) h}
    ((𝒰.toPresieveOverProp (P := P) (Q := Q) p).bind T)

Tactic:
choose V h pV hV using H