awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve X
⊢ 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
have 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
Tactic: rw [overGrothendieckTopology_eq_toGrothendieck_overPretopology]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
inst_2 : P.RespectsIso
X : Over S
R : Sieve 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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
⊢ 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))))
have 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))))
Tactic: rw [mem_overGrothendieckTopology] at hT ⊢
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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
⊢ ∃ (𝒰 : 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))))
have 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))))
Tactic: obtain ⟨𝒰, h, hle⟩ := hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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
⊢ ∃ (𝒰 : 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))))
have 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))))
Tactic: use 𝒰, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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)
have rw : Q (𝒰.f i ≫ (Functor.obj (MorphismProperty.Over.forget Q ⊤ S) X).left ↘ S)
Tactic: rw [← comp_over (𝒰.f i) S]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (hypothesis)
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₀
⊢ 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)
have p : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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.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)
have 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) sorry 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) sorry True.intro))
Tactic: use (𝒰.X i).asOverProp S p, MorphismProperty.Over.homMk (𝒰.f i) (comp_over (𝒰.f i) S), 𝟙 _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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))
have refine_1 : ∀ (j : (Cover.pullbackCoverOverProp' (P := P) S 𝒰 f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (Q := Q) sorry sorry p).I₀),
  Q
    ((Cover.pullbackCoverOverProp' (P := P) S 𝒰 f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (Q := Q) sorry sorry p).X j ↘
      S)
Tactic: refine ⟨𝒰.pullbackCoverOverProp' S f.left (Q := Q) Y.prop X.prop p, inferInstance, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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)
⊢ 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))
have 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) sorry sorry
        p).toPresieveOverProp
    (P := P) (Q := Q) sorry
Tactic: refine ⟨𝒰.pullbackCoverOverProp' S f.left (Q := Q) Y.prop X.prop p, inferInstance, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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)
⊢ 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)
have 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) sorry),
  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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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)
have refine : (𝒰.toPresieveOverProp (P := P) (Q := Q) p).bind T =
  Cover.toPresieveOverProp (P := P) (Q := Q) (Precoverage.ZeroHypercover.bind 𝒰 fun (j : 𝒰.I₀) ↦ 𝒱j j) sorry
Tactic: refine ⟨𝒰.bind (fun j ↦ 𝒱j j), inferInstance, fun j ↦ pV _ _ _, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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) ⋯
⊢ (𝒰.toPresieveOverProp (P := P) (Q := Q) p).bind T =
    Cover.toPresieveOverProp (P := P) (Q := Q) (Precoverage.ZeroHypercover.bind 𝒰 fun (j : 𝒰.I₀) ↦ 𝒱j j) ⋯
have h₁ : Presieve X = Presieve (C := Q.Over ⊤ S) (X.toComma (P := Q) (Q := ⊤) (W := ⊤).left.asOverProp (P := Q) S sorry) →
  X = X.toComma (P := Q) (Q := ⊤) (W := ⊤).left.asOverProp (P := Q) S sorry →
    HEq (𝒰.toPresieveOverProp (P := P) (Q := Q) p) (β :=
        Presieve (C := Q.Over ⊤ S) (X.toComma (P := Q) (Q := ⊤) (W := ⊤).left.asOverProp (P := Q) S sorry))
        (Presieve.ofArrows (fun (j : 𝒰.I₀) ↦ (𝒰.X j).asOverProp (P := Q) S sorry) 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 sorry)
            fun (j : (V x_1 x_2).I₀) ↦ Hom.asOverProp (P := Q) ((V x_1 x_2).f j) S
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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Small (goal)
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
⊢ S.smallGrothendieckTopologyOfLE (P := P) (Q := Q) hPQ =
    Pretopology.toGrothendieck (smallPretopology P Q : Pretopology (Q.Over ⊤ S))
have 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
Tactic: ext X R