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
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left
h_1 : 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
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 : ⦃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) ⋯
𝒱j : (j : 𝒰.I₀) → Cover (precoverage P) ((𝒰.X j).asOverProp (P := Q) S ⋯).toComma (P := Q) (Q := ⊤) (W := ⊤).left :=
  fun (j : 𝒰.I₀) ↦ V (Hom.asOverProp (P := Q) (𝒰.f 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}
    ((𝒰.toPresieveOverProp (P := P) (Q := Q) p).bind T)

Tactic:
⟨𝒰.bind (fun j ↦ 𝒱j j), inferInstance, fun j ↦ pV _ _ _, ?_⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Presieve.ofArrows.mk, Set.Mem, AlgebraicGeometry.Scheme.Hom.asOverProp, setOf, inferInstance, Sigma.fst, Exists.intro, Sigma.snd, 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
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_1 : 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
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 : ⦃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) ⋯
𝒱j : (j : 𝒰.I₀) → Cover (precoverage P) ((𝒰.X j).asOverProp (P := Q) S ⋯).toComma (P := Q) (Q := ⊤) (W := ⊤).left :=
  fun (j : 𝒰.I₀) ↦ V (Hom.asOverProp (P := Q) (𝒰.f j) S) ⋯
refine :
  (𝒰.toPresieveOverProp (P := P) (Q := Q) p).bind T =
    Cover.toPresieveOverProp (P := P) (Q := Q) (Precoverage.ZeroHypercover.bind 𝒰 fun (j : 𝒰.I₀) ↦ 𝒱j j) ⋯
⊢ 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:
refine ⟨𝒰.bind (fun j ↦ 𝒱j j), inferInstance, fun j ↦ pV _ _ _, ?_⟩
-- 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_1 : 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
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 : ⦃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) ⋯
𝒱j : (j : 𝒰.I₀) → Cover (precoverage P) ((𝒰.X j).asOverProp (P := Q) S ⋯).toComma (P := Q) (Q := ⊤) (W := ⊤).left :=
  fun (j : 𝒰.I₀) ↦ V (Hom.asOverProp (P := Q) (𝒰.f j) S) ⋯
h₁ :
  Presieve X = Presieve (C := Q.Over ⊤ S) (X.toComma (P := Q) (Q := ⊤) (W := ⊤).left.asOverProp (P := Q) S ⋯) →
    X = X.toComma (P := Q) (Q := ⊤) (W := ⊤).left.asOverProp (P := Q) S ⋯ →
      HEq (𝒰.toPresieveOverProp (P := P) (Q := Q) p) (β :=
          Presieve (C := Q.Over ⊤ S) (X.toComma (P := Q) (Q := ⊤) (W := ⊤).left.asOverProp (P := Q) S ⋯))
          (Presieve.ofArrows (fun (j : 𝒰.I₀) ↦ (𝒰.X j).asOverProp (P := Q) S ⋯) fun (j : 𝒰.I₀) ↦
            Hom.asOverProp (P := Q) (𝒰.f j) S) →
        ∀ (x : Q.Over ⊤ S) (x_1 : x ⟶ X) (x_2 : 𝒰.toPresieveOverProp (P := P) (Q := Q) 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).asOverProp (P := Q) S ⋯)
              fun (j : (V x_1 x_2).I₀) ↦ Hom.asOverProp (P := Q) ((V x_1 x_2).f j) S
⊢ (𝒰.toPresieveOverProp (P := P) (Q := Q) p).bind T =
    Cover.toPresieveOverProp (P := P) (Q := Q) (Precoverage.ZeroHypercover.bind 𝒰 fun (j : 𝒰.I₀) ↦ 𝒱j j) ⋯

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

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.asOverProp, CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.Scheme.asOverProp, 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
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_1 : 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
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 : ⦃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) ⋯
𝒱j : (j : 𝒰.I₀) → Cover (precoverage P) ((𝒰.X j).asOverProp (P := Q) S ⋯).toComma (P := Q) (Q := ⊤) (W := ⊤).left :=
  fun (j : 𝒰.I₀) ↦ V (Hom.asOverProp (P := Q) (𝒰.f j) S) ⋯
e_1 : Presieve X = Presieve (C := Q.Over ⊤ S) (X.toComma (P := Q) (Q := ⊤) (W := ⊤).left.asOverProp (P := Q) S ⋯)
e_3 : X = X.toComma (P := Q) (Q := ⊤) (W := ⊤).left.asOverProp (P := Q) S ⋯
e_4 :
  HEq (𝒰.toPresieveOverProp (P := P) (Q := Q) p) (β :=
    Presieve (C := Q.Over ⊤ S) (X.toComma (P := Q) (Q := ⊤) (W := ⊤).left.asOverProp (P := Q) S ⋯))
    (Presieve.ofArrows (fun (j : 𝒰.I₀) ↦ (𝒰.X j).asOverProp (P := Q) S ⋯) fun (j : 𝒰.I₀) ↦
      Hom.asOverProp (P := Q) (𝒰.f j) S)
x : Q.Over ⊤ S
x_1 : x ⟶ X
h_2 : 𝒰.toPresieveOverProp (P := P) (Q := Q) 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).asOverProp (P := Q) S ⋯) fun (j : (V x_1 h_2).I₀) ↦
      Hom.asOverProp (P := Q) ((V x_1 h_2).f j) S

Tactic:
apply hV
-- 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
hPQ : P ≤ Q
h :
  ∀ (X : Q.Over ⊤ S) (R : Sieve X),
    R ∈ (S.smallGrothendieckTopologyOfLE (P := P) (Q := Q) hPQ : (a : Q.Over ⊤ S) → Set (Sieve a)) X ↔
      R ∈
        (Pretopology.toGrothendieck (smallPretopology P Q : Pretopology (Q.Over ⊤ S)) :
            (a : Q.Over ⊤ S) → Set (Sieve a))
          X
⊢ S.smallGrothendieckTopologyOfLE (P := P) (Q := Q) hPQ =
    Pretopology.toGrothendieck (smallPretopology P Q : Pretopology (Q.Over ⊤ S))

Tactic:
ext X R
-- 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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
h :
  (∃ (𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))) (x : Cover.Over S (P := P) 𝒰),
      𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)) ↔
    ∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
      R_1 ≤ R.arrows
⊢ R ∈ (S.smallGrothendieckTopologyOfLE (P := P) (Q := Q) hPQ : (a : Q.Over ⊤ S) → Set (Sieve a)) X ↔
    R ∈
      (Pretopology.toGrothendieck (smallPretopology P Q : Pretopology (Q.Over ⊤ S)) : (a : Q.Over ⊤ S) → Set (Sieve a))
        X

Tactic:
simp only [Pretopology.mem_toGrothendieck, Functor.mem_inducedTopology_sieves_iff,
    MorphismProperty.Comma.forget_obj, mem_overGrothendieckTopology]

Premises used: CategoryTheory.Pretopology.mem_toGrothendieck, AlgebraicGeometry.Scheme.mem_overGrothendieckTopology, CategoryTheory.MorphismProperty.Comma.forget_obj, CategoryTheory.Functor.mem_inducedTopology_sieves_iff
-- 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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
h :
  (∃ (𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))) (x : Cover.Over S (P := P) 𝒰),
      𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)) →
    ∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
      R_1 ≤ R.arrows
h₁ :
  (∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
      R_1 ≤ R.arrows) →
    ∃ (𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))) (x : Cover.Over S (P := P) 𝒰),
      𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
⊢ (∃ (𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))) (x : Cover.Over S (P := P) 𝒰),
      𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)) ↔
    ∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
      R_1 ≤ R.arrows

Tactic:
constructor
-- 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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))
h : Cover.Over S (P := P) 𝒰
le : 𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
j : 𝒰.I₀
rw : Q (𝒰.f j ≫ Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)) ↘ S)
⊢ Q (𝒰.X j ↘ S)

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

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
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))
h : Cover.Over S (P := P) 𝒰
le : 𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
j : 𝒰.I₀
⊢ Q (𝒰.f j ≫ Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)) ↘ S)

Tactic:
Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop _) 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
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))
h : Cover.Over S (P := P) 𝒰
le : 𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
j : 𝒰.I₀
⊢ Q (𝒰.f j ≫ Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)) ↘ S)

Tactic:
exact Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop _) 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
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))
h : Cover.Over S (P := P) 𝒰
le : 𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
⊢ ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)

Tactic:
have hj (j : 𝒰.I₀) : Q (𝒰.X j ↘ S) := by
      rw [← comp_over (𝒰.f j)]
      exact Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop _) 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
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))
h : Cover.Over S (P := P) 𝒰
le : 𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
hj : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ ∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
    R_1 ≤ R.arrows

Tactic:
⟨𝒰.toPresieveOverProp hj, ?_, ?_⟩

Premises used: And.intro, Exists.intro, AlgebraicGeometry.Scheme.Cover.toPresieveOverProp
-- 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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))
h : Cover.Over S (P := P) 𝒰
le : 𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
hj : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
h₁ :
  𝒰.toPresieveOverProp (P := P) (Q := Q) hj ∈
    Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X
h₂ : 𝒰.toPresieveOverProp (P := P) (Q := Q) hj ≤ R.arrows
⊢ ∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
    R_1 ≤ R.arrows

Tactic:
refine ⟨𝒰.toPresieveOverProp hj, ?_, ?_⟩
-- 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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))
h : Cover.Over S (P := P) 𝒰
le : 𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
hj : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
w : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left
w₁ : Cover.Over S (P := P) 𝒰
w₂ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
h₁ : 𝒰.toPresieveOverProp (P := P) (Q := Q) hj = 𝒰.toPresieveOverProp (P := P) (Q := Q) hj
⊢ 𝒰.toPresieveOverProp (P := P) (Q := Q) hj ∈
    Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X

Tactic:
use 𝒰, h, hj
-- 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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))
h : Cover.Over S (P := P) 𝒰
le : 𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
hj : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
Y : Q.Over ⊤ S
i : 𝒰.I₀
fi : (𝒰.X i).asOverProp (P := Q) S ⋯ ⟶ X := Hom.asOverProp (P := Q) (𝒰.f i) S
⊢ Sieve.arrows (X := Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X)
    (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
    (CategoryTheory.Functor.map (MorphismProperty.Over.forget Q ⊤ S) fi)

Tactic:
have : R.functorPushforward _ ((MorphismProperty.Over.forget Q ⊤ S).map fi) := le _ _ ⟨i⟩
-- 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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))
h : Cover.Over S (P := P) 𝒰
le : 𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
hj : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
Y : Q.Over ⊤ S
i : 𝒰.I₀
fi : (𝒰.X i).asOverProp (P := Q) S ⋯ ⟶ X := Hom.asOverProp (P := Q) (𝒰.f i) S
this :
  Sieve.arrows (X := Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X)
    (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
    (CategoryTheory.Functor.map (MorphismProperty.Over.forget Q ⊤ S) fi)
h₁ :
  ∀
    (this :
      Presieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R.arrows
        (CategoryTheory.Functor.map (MorphismProperty.Over.forget Q ⊤ S) fi)),
    R.arrows (Y := (𝒰.X i).asOverProp (P := Q) S ⋯) (Hom.asOverProp (P := Q) (𝒰.f i) S)
h₂ h₃ h₄ h₅ :
  ∀ (this : R.arrows fi), R.arrows (Y := (𝒰.X i).asOverProp (P := Q) S ⋯) (Hom.asOverProp (P := Q) (𝒰.f i) S)
⊢ R.arrows (Y := (𝒰.X i).asOverProp (P := Q) S ⋯) (Hom.asOverProp (P := Q) (𝒰.f i) S)

Tactic:
rwa [Sieve.functorPushforward_apply,
        Sieve.mem_functorPushforward_iff_of_full_of_faithful] at this

Premises used: CategoryTheory.Sieve.functorPushforward_apply, CategoryTheory.Sieve.mem_functorPushforward_iff_of_full_of_faithful
-- 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
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left
h : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
le : 𝒰.toPresieveOverProp (P := P) (Q := Q) p ≤ R.arrows
h₁ : 𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)
⊢ ∃ (𝒰 : Cover (precoverage P) (Over.left (X.toComma (P := Q) (Q := ⊤) (W := ⊤)))) (x : Cover.Over S (P := P) 𝒰),
    𝒰.toPresieveOver (P := P) ≤ Sieve.arrows (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R)

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
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left
h : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
le : 𝒰.toPresieveOverProp (P := P) (Q := Q) p ≤ R.arrows
Y : Over S
i : 𝒰.I₀
⊢ Sieve.arrows (X := X.toComma (P := Q) (Q := ⊤) (W := ⊤))
    (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R :
      Sieve (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X))
    (Y := (𝒰.X i).asOver S) (Hom.asOver (𝒰.f i) S)

Tactic:
⟨(𝒰.X i).asOverProp S (p i), (𝒰.f i).asOverProp S, 𝟙 _, le _ _ ⟨i⟩, rfl⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Presieve.ofArrows.mk, AlgebraicGeometry.Scheme.Hom.asOverProp, CategoryTheory.CategoryStruct.id, CategoryTheory.PreZeroHypercover.X, And.intro, Exists.intro, AlgebraicGeometry.Scheme.asOverProp, CategoryTheory.Presieve.functorPushforward, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, 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
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left
h : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
le : 𝒰.toPresieveOverProp (P := P) (Q := Q) p ≤ R.arrows
Y : Over S
i : 𝒰.I₀
⊢ Sieve.arrows (X := X.toComma (P := Q) (Q := ⊤) (W := ⊤))
    (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R :
      Sieve (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X))
    (Y := (𝒰.X i).asOver S) (Hom.asOver (𝒰.f i) S)

Tactic:
exact ⟨(𝒰.X i).asOverProp S (p i), (𝒰.f i).asOverProp S, 𝟙 _, le _ _ ⟨i⟩, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.Small
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
inst_3 : P.HasOfPostcompProperty P
⊢ Eq (α := GrothendieckTopology (P.Over ⊤ S)) (smallGrothendieckTopology P)
    (Pretopology.toGrothendieck (smallPretopology P P : Pretopology (P.Over ⊤ S)))

Tactic:
S.smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology le_rfl

Premises used: le_rfl, AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology