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
R : Sieve X
⊢ (∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
      R_1 ≤ R.arrows) ↔
    ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
      ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : ↥Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
        R.arrows f ∧
          P f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left ∧ f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left y = x

Tactic:
⟨?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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
R : Sieve X
refine_1 :
  (∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
      R_1 ≤ R.arrows) →
    ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
      ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : ↥Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
        R.arrows f ∧
          P f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left ∧ f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left y = x
refine_2 :
  ∀
    (h :
      ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
        ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : ↥Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
          R.arrows f ∧
            P f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left ∧
              f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left y = x),
    ∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
      R_1 ≤ R.arrows
⊢ (∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
      R_1 ≤ R.arrows) ↔
    ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
      ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : ↥Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
        R.arrows f ∧
          P f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left ∧ f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left y = x

Tactic:
refine ⟨?_, fun 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
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)
hle : 𝒰.toPresieveOverProp (P := P) (Q := Q) p ≤ R.arrows
x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left
refine_1 :
  ∀ (y : ↥(𝒰.X (𝒰.idx x))) (hy : (𝒰.f (𝒰.idx x)) y = x),
    ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : ↥Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
      R.arrows f ∧
        P f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left ∧ f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left y = x
⊢ ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : ↥Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
    R.arrows f ∧
      P f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left ∧ f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left y = x

Tactic:
obtain ⟨y, hy⟩ := 𝒰.covers x

Premises used: AlgebraicGeometry.Scheme.Cover.covers
-- 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
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)
hle : 𝒰.toPresieveOverProp (P := P) (Q := Q) p ≤ R.arrows
x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left
y : ↥(𝒰.X (𝒰.idx x))
hy : (𝒰.f (𝒰.idx x)) y = x
⊢ ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : ↥Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
    R.arrows f ∧
      P f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left ∧ f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left y = x

Tactic:
⟨(𝒰.X (𝒰.idx x)).asOverProp S (p _), (𝒰.f (𝒰.idx x)).asOverProp S, y, hle _ _ ?_,
      𝒰.map_prop _, hy⟩

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.asOverProp, CategoryTheory.PreZeroHypercover.X, And.intro, Exists.intro, AlgebraicGeometry.Scheme.Cover.map_prop, AlgebraicGeometry.Scheme.Cover.idx, 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
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty 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)
hle : 𝒰.toPresieveOverProp (P := P) (Q := Q) p ≤ R.arrows
x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left
y : ↥(𝒰.X (𝒰.idx x))
hy : (𝒰.f (𝒰.idx x)) y = x
refine_1 :
  𝒰.toPresieveOverProp (P := P) (Q := Q) p (Y := (𝒰.X (𝒰.idx x)).asOverProp (P := Q) S ⋯)
    (Hom.asOverProp (P := Q) (𝒰.f (𝒰.idx x)) S)
⊢ ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : ↥Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
    R.arrows f ∧
      P f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left ∧ f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left y = x

Tactic:
refine ⟨(𝒰.X (𝒰.idx x)).asOverProp S (p _), (𝒰.f (𝒰.idx x)).asOverProp S, y, hle _ _ ?_,
      𝒰.map_prop _, hy⟩
-- 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
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)
hle : 𝒰.toPresieveOverProp (P := P) (Q := Q) p ≤ R.arrows
x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left
y : ↥(𝒰.X (𝒰.idx x))
hy : (𝒰.f (𝒰.idx x)) y = x
⊢ 𝒰.toPresieveOverProp (P := P) (Q := Q) p (Y := (𝒰.X (𝒰.idx x)).asOverProp (P := Q) S ⋯)
    (Hom.asOverProp (P := Q) (𝒰.f (𝒰.idx x)) S)

Tactic:
use 𝒰.idx x

Premises used: AlgebraicGeometry.Scheme.Cover.idx
-- 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
R : Sieve X
h :
  ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
    ∃ (Y : Q.Over ⊤ S) (f : Y ⟶ X) (y : ↥Y.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
      R.arrows f ∧
        P f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left ∧ f.toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left y = x
refine_2 :
  ∀ (Y : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Q.Over ⊤ S)
    (f : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Y x ⟶ X)
    (y : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → ↥(Y x).toComma (P := Q) (Q := ⊤) (W := ⊤).left)
    (hf : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), R.arrows (f x))
    (hP : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), P (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left)
    (hy :
      ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left),
        (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (y x) = x),
    ∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
      R_1 ≤ R.arrows
⊢ ∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
    R_1 ≤ R.arrows

Tactic:
choose Y f y hf hP hy 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
inst_3 : Q.IsStableUnderComposition
inst_4 : Q.IsStableUnderBaseChange
inst_5 : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
Y : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Q.Over ⊤ S
f : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Y x ⟶ X
y : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → ↥(Y x).toComma (P := Q) (Q := ⊤) (W := ⊤).left
hf : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), R.arrows (f x)
hP : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), P (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left
hy : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (y x) = x
𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left :=
  { I₀ := ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left,
    X := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (Y i).toComma (P := Q) (Q := ⊤) (W := ⊤).left,
    f := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (f i).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left,
    mem₀ := ⋯ }
this : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) (fun (i : 𝒰.I₀) ↦ inferInstance) ⋯
⊢ ∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
    R_1 ≤ R.arrows

Tactic:
⟨𝒰.toPresieveOverProp fun i ↦ MorphismProperty.Comma.prop _, ?_, ?_⟩

Premises used: CategoryTheory.MorphismProperty.Comma.prop, 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
X : Q.Over ⊤ S
R : Sieve X
Y : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Q.Over ⊤ S
f : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Y x ⟶ X
y : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → ↥(Y x).toComma (P := Q) (Q := ⊤) (W := ⊤).left
hf : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), R.arrows (f x)
hP : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), P (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left
hy : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (y x) = x
𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left :=
  { I₀ := ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left,
    X := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (Y i).toComma (P := Q) (Q := ⊤) (W := ⊤).left,
    f := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (f i).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left,
    mem₀ := ⋯ }
this : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) (fun (i : 𝒰.I₀) ↦ inferInstance) ⋯
refine_2 :
  𝒰.toPresieveOverProp (P := P) (Q := Q) ⋯ ∈
    Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X
refine_2₁ : 𝒰.toPresieveOverProp (P := P) (Q := Q) ⋯ ≤ R.arrows
⊢ ∃ R_1 ∈ Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X,
    R_1 ≤ R.arrows

Tactic:
refine ⟨𝒰.toPresieveOverProp fun i ↦ 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
X : Q.Over ⊤ S
R : Sieve X
Y : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Q.Over ⊤ S
f : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Y x ⟶ X
y : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → ↥(Y x).toComma (P := Q) (Q := ⊤) (W := ⊤).left
hf : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), R.arrows (f x)
hP : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), P (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left
hy : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (y x) = x
𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left :=
  { I₀ := ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left,
    X := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (Y i).toComma (P := Q) (Q := ⊤) (W := ⊤).left,
    f := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (f i).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left,
    mem₀ := ⋯ }
this : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) (fun (i : 𝒰.I₀) ↦ inferInstance) ⋯
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) ⋯ = 𝒰.toPresieveOverProp (P := P) (Q := Q) ⋯
⊢ 𝒰.toPresieveOverProp (P := P) (Q := Q) ⋯ ∈
    Precoverage.coverings (Pretopology.toPrecoverage (smallPretopology P Q : Pretopology (Q.Over ⊤ S))) X

Tactic:
use 𝒰, inferInstance, fun i ↦ 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
X : Q.Over ⊤ S
R : Sieve X
Y_1 : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Q.Over ⊤ S
f : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Y_1 x ⟶ X
y : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → ↥(Y_1 x).toComma (P := Q) (Q := ⊤) (W := ⊤).left
hf : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), R.arrows (f x)
hP : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), P (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left
hy : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (y x) = x
𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left :=
  { I₀ := ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left,
    X := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (Y_1 i).toComma (P := Q) (Q := ⊤) (W := ⊤).left,
    f := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (f i).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left,
    mem₀ := ⋯ }
this : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) (fun (i : 𝒰.I₀) ↦ inferInstance) ⋯
Y : Q.Over ⊤ S
i : 𝒰.I₀
⊢ R.arrows (Y := (𝒰.X i).asOverProp (P := Q) S ⋯) (Hom.asOverProp (P := Q) (𝒰.f i) S)

Tactic:
hf i

Premises used: CategoryTheory.Over.mk, CategoryTheory.over, CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Over.homMk, CategoryTheory.OverClass.asOver, CategoryTheory.CostructuredArrow.mk, CategoryTheory.OverClass.asOverHom
-- 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
R : Sieve X
Y_1 : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Q.Over ⊤ S
f : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → Y_1 x ⟶ X
y : (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) → ↥(Y_1 x).toComma (P := Q) (Q := ⊤) (W := ⊤).left
hf : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), R.arrows (f x)
hP : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), P (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left
hy : ∀ (x : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left), (f x).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left (y x) = x
𝒰 : Cover (precoverage P) X.toComma (P := Q) (Q := ⊤) (W := ⊤).left :=
  { I₀ := ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left,
    X := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (Y_1 i).toComma (P := Q) (Q := ⊤) (W := ⊤).left,
    f := fun (i : ↥X.toComma (P := Q) (Q := ⊤) (W := ⊤).left) ↦ (f i).toCommaMorphism (P := Q) (Q := ⊤) (W := ⊤).left,
    mem₀ := ⋯ }
this : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) (fun (i : 𝒰.I₀) ↦ inferInstance) ⋯
Y : Q.Over ⊤ S
i : 𝒰.I₀
⊢ R.arrows (Y := (𝒰.X i).asOverProp (P := Q) S ⋯) (Hom.asOverProp (P := Q) (𝒰.f i) S)

Tactic:
exact hf i
-- 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
X : P.Over ⊤ S
R : Sieve X
rw :
  R ∈
      (Pretopology.toGrothendieck (smallPretopology P P : Pretopology (P.Over ⊤ S)) : (a : P.Over ⊤ S) → Set (Sieve a))
        X ↔
    ∃ (𝒰 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
      ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp (P := P) (Q := P) h ≤ R.arrows
⊢ R ∈ (smallGrothendieckTopology P : (a : P.Over ⊤ S) → Set (Sieve a)) X ↔
    ∃ (𝒰 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
      ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp (P := P) (Q := P) h ≤ R.arrows

Tactic:
rw [smallGrothendieckTopology_eq_toGrothendieck_smallPretopology]

Premises used: AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology
-- 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
X : P.Over ⊤ S
R : Sieve X
mp :
  R ∈
      (Pretopology.toGrothendieck (smallPretopology P P : Pretopology (P.Over ⊤ S)) : (a : P.Over ⊤ S) → Set (Sieve a))
        X →
    ∃ (𝒰 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
      ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp (P := P) (Q := P) h ≤ R.arrows
mpr :
  (∃ (𝒰 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
      ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp (P := P) (Q := P) h ≤ R.arrows) →
    R ∈
      (Pretopology.toGrothendieck (smallPretopology P P : Pretopology (P.Over ⊤ S)) : (a : P.Over ⊤ S) → Set (Sieve a))
        X
⊢ R ∈
      (Pretopology.toGrothendieck (smallPretopology P P : Pretopology (P.Over ⊤ S)) : (a : P.Over ⊤ S) → Set (Sieve a))
        X ↔
    ∃ (𝒰 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
      ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp (P := P) (Q := P) h ≤ 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
inst_3 : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left
h : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp (P := P) (Q := P) p ≤ R.arrows
w : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left
w₁ : Cover.Over S (P := P) 𝒰
w₂ : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)
h₁ : 𝒰.toPresieveOverProp (P := P) (Q := P) p ≤ R.arrows
⊢ ∃ (𝒰 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
    ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp (P := P) (Q := P) h ≤ R.arrows

Tactic:
use 𝒰, h, p
-- 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
X : P.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left
h𝒰 : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp (P := P) (Q := P) p ≤ R.arrows
⊢ R ∈
    (Pretopology.toGrothendieck (smallPretopology P P : Pretopology (P.Over ⊤ S)) : (a : P.Over ⊤ S) → Set (Sieve a)) X

Tactic:
⟨𝒰.toPresieveOverProp p, ⟨𝒰, h𝒰, p, rfl⟩, hle⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, AlgebraicGeometry.Scheme.Cover.toPresieveOverProp, 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
X : P.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.toComma (P := P) (Q := ⊤) (W := ⊤).left
h𝒰 : Cover.Over S (P := P) 𝒰
p : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp (P := P) (Q := P) p ≤ R.arrows
⊢ R ∈
    (Pretopology.toGrothendieck (smallPretopology P P : Pretopology (P.Over ⊤ S)) : (a : P.Over ⊤ S) → Set (Sieve a)) X

Tactic:
exact ⟨𝒰.toPresieveOverProp p, ⟨𝒰, h𝒰, p, rfl⟩, hle⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
W : X.Opens
hW : IsAffineOpen W
g : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) W hW)) : Type u)
hV : IsAffineOpen (X.basicOpen g)
f : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen g) hV)) : Type u)
hU : IsAffineOpen (X.basicOpen f)
⊢ ∃ (f_1 : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) W hW)) : Type u)),
    X.basicOpen f_1 = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hU)

Tactic:
hW.basicOpen_basicOpen_is_basicOpen g f

Premises used: Set.Mem, setOf, AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen, AlgebraicGeometry.RingedSpace.basicOpen, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
W : X.Opens
hW : IsAffineOpen W
g : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) W hW)) : Type u)
hV : IsAffineOpen (X.basicOpen g)
f : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen g) hV)) : Type u)
hU : IsAffineOpen (X.basicOpen f)
⊢ ∃ (f_1 : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) W hW)) : Type u)),
    X.basicOpen f_1 = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hU)

Tactic:
exact hW.basicOpen_basicOpen_is_basicOpen g f

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
V : X.Opens
hV : IsAffineOpen V
f : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)) : Type u)
hU : IsAffineOpen (X.basicOpen f)
⊢ toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hU) ≤
    toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)

Tactic:
X.basicOpen_le _

Premises used: Set.Mem, AlgebraicGeometry.Scheme.basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
V : X.Opens
hV : IsAffineOpen V
f : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)) : Type u)
hU : IsAffineOpen (X.basicOpen f)
⊢ toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hU) ≤
    toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)

Tactic:
exact X.basicOpen_le _

Premises used: AlgebraicGeometry.Scheme.basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
⊢ Function.Injective.{u + 1, u + 1} (α := X.AffineZariskiSite) toOpens

Tactic:
Subtype.val_injective

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite, Subtype.val_injective
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
f : (↑Γ(X, U.toOpens) : Type u)
⊢ U.basicOpen f ≤ U

Tactic:
⟨f, rfl⟩

Premises used: Exists.intro, rfl