awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X Y Z : Scheme
𝒰_1 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : JointlySurjective K
𝒰 : Cover.{u_1, u} K X
h : ∀ (j : 𝒰.I₀), Q (𝒰.f j)
rw :
  (∀ (x : ↥X), ∃ (i : 𝒰.I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x) ∧
    ∀ (i : 𝒰.I₀), Q (𝒰.f i)
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1} 𝒰.toPreZeroHypercover ∈ (precoverage Q).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X Y Z : Scheme
𝒰_1 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : JointlySurjective K
𝒰 : Cover.{u_1, u} K X
h : ∀ (j : 𝒰.I₀), Q (𝒰.f j)
⊢ (∀ (x : ↥X), ∃ (i : 𝒰.I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x) ∧
    ∀ (i : 𝒰.I₀), Q (𝒰.f i)

Tactic:
⟨𝒰.exists_eq, h⟩

Premises used: And.intro, AlgebraicGeometry.Scheme.Cover.exists_eq
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X Y Z : Scheme
𝒰_1 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : JointlySurjective K
𝒰 : Cover.{u_1, u} K X
h : ∀ (j : 𝒰.I₀), Q (𝒰.f j)
⊢ (∀ (x : ↥X), ∃ (i : 𝒰.I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x) ∧
    ∀ (i : 𝒰.I₀), Q (𝒰.f i)

Tactic:
exact ⟨𝒰.exists_eq, h⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
rw :
  (∀ (x : ↥X),
      ∃ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i))
            ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i))
          x) ∧
    ∀ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      P ({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i)
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1} { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X } ∈
    (precoverage P).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
⊢ (∀ (x : ↥X),
      ∃ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i))
            ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i))
          x) ∧
    ∀ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      P ({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i)

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

Premises used: And.intro
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
refine_1 :
  ∀ (x : ↥X),
    ∃ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i))
          ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i))
        x
refine_2 :
  ∀ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    P ({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i)
⊢ (∀ (x : ↥X),
      ∃ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i))
            ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i))
          x) ∧
    ∀ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      P ({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i)

Tactic:
refine ⟨fun x ↦ ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
x : ↥X
refine_1 :
  ∀ (i : 𝒰.I₀) (y : ↥(𝒰.X i)),
    ∃ (i_1 : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      Membership.mem (α := ↥X) (γ := Set ↥X)
        (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i_1))
          ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i_1))
        ((𝒰.f i) y : ↥X)
⊢ ∃ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i))
        ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i))
      x

Tactic:
obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq x

Premises used: AlgebraicGeometry.Scheme.Cover.exists_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
i : 𝒰.I₀
y : ↥(𝒰.X i)
refine_1 :
  ∀ (i : J) (y : ↥(𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i))),
    ∃ (i_1 : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      Membership.mem (α := ↥X) (γ := Set ↥X)
        (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i_1))
          ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i_1))
        ((𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)) y : ↥X)
⊢ ∃ (i_1 : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (α := ↥X) (γ := Set ↥X)
      (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i_1))
        ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i_1))
      ((𝒰.f i) y : ↥X)

Tactic:
obtain ⟨i, rfl⟩ := e₁.surjective i

Premises used: Equiv.surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
i : J
y : ↥(𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i))
h₁ :
  Eq (α := ↥X)
    (({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i) ((e₂ i).inv y : ↥(obj i)) : ↥X)
    ((𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)) y : ↥X)
⊢ ∃ (i_1 : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (α := ↥X) (γ := Set ↥X)
      (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i_1))
        ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i_1))
      ((𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)) y : ↥X)

Tactic:
use i, (e₂ i).inv y

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
i : J
y : ↥(𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i))
⊢ Eq (α := ↥X)
    (({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i) ((e₂ i).inv y : ↥(obj i)) : ↥X)
    ((𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)) y : ↥X)

Tactic:
simp [h]
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
refine_2 : ∀ (i : J), P (X := 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)) (𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i))
⊢ ∀ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    P ({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i)

Tactic:
simp_rw [h, MorphismProperty.cancel_left_of_respectsIso]

Premises used: CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
i : J
⊢ P (X := 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)) (𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i))

Tactic:
𝒰.map_prop _

Premises used: AlgebraicGeometry.Scheme.Cover.map_prop
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
i : J
⊢ P (X := 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)) (𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i))

Tactic:
exact 𝒰.map_prop _

Premises used: AlgebraicGeometry.Scheme.Cover.map_prop
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y_1 Z : Scheme
𝒰_1 : Cover K X_1
f_1 : X_1 ⟶ Z
g : Y_1 ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f_1) g
P Q : MorphismProperty Scheme
X Y : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : Y ⟶ X
hf : P f
rw :
  (∀ (x : ↥X),
      ∃ (i : (𝒰.add f).I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥((𝒰.add f).X i)) ⇑((𝒰.add f).f i)) x) ∧
    ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1} (𝒰.add f) ∈ (precoverage P).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y_1 Z : Scheme
𝒰_1 : Cover K X_1
f_1 : X_1 ⟶ Z
g : Y_1 ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f_1) g
P Q : MorphismProperty Scheme
X Y : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ (∀ (x : ↥X),
      ∃ (i : (𝒰.add f).I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥((𝒰.add f).X i)) ⇑((𝒰.add f).f i)) x) ∧
    ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)

Tactic:
⟨fun x ↦ ⟨some <| 𝒰.idx x, 𝒰.covers x⟩, ?_⟩

Premises used: AlgebraicGeometry.Scheme.Cover.covers, Option.some, And.intro, Exists.intro, AlgebraicGeometry.Scheme.Cover.idx
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y_1 Z : Scheme
𝒰_1 : Cover K X_1
f_1 : X_1 ⟶ Z
g : Y_1 ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f_1) g
P Q : MorphismProperty Scheme
X Y : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : Y ⟶ X
hf : P f
refine : ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)
⊢ (∀ (x : ↥X),
      ∃ (i : (𝒰.add f).I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥((𝒰.add f).X i)) ⇑((𝒰.add f).f i)) x) ∧
    ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)

Tactic:
refine ⟨fun x ↦ ⟨some <| 𝒰.idx x, 𝒰.covers x⟩, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y_1 Z : Scheme
𝒰_1 : Cover K X_1
f_1 : X_1 ⟶ Z
g : Y_1 ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f_1) g
P Q : MorphismProperty Scheme
X Y : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ P (X := (𝒰.add f).X none) ((𝒰.add f).f none)

Tactic:
simp [hf, 𝒰.map_prop]

Premises used: AlgebraicGeometry.Scheme.Cover.map_prop
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y_1 Z : Scheme
𝒰_1 : Cover K X_1
f_1 : X_1 ⟶ Z
g : Y_1 ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f_1) g
P Q : MorphismProperty Scheme
X Y : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : Y ⟶ X
hf : P f
i : 𝒰.I₀
⊢ P (X := (𝒰.add f).X (some i)) ((𝒰.add f).f (some i))

Tactic:
simp [hf, 𝒰.map_prop]

Premises used: AlgebraicGeometry.Scheme.Cover.map_prop
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : ∀ (x : 𝒰.I₀), HasPullback f (𝒰.f x)
i : 𝒰.toPreZeroHypercover.1
⊢ 𝒰.pullbackHom (P := P) f i ≫ 𝒰.f i = (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f

Tactic:
pullback.condition.symm

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.pullback.condition, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover.{u_1, u} P X
rw :
  (∀ (x : ↥X),
      ∃ (i :
        { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
            PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                    PreZeroHypercover.{u_1, u, u + 1} X }.X
                i))
            ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                    PreZeroHypercover.{u_1, u, u + 1} X }.f
                i))
          x) ∧
    ∀
      (i :
        { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
            PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      P
        ({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
              PreZeroHypercover.{u_1, u, u + 1} X }.f
          i)
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1}
      { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
        PreZeroHypercover.{u_1, u, u + 1} X } ∈
    (precoverage P).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover.{u_1, u} P X
⊢ (∀ (x : ↥X),
      ∃ (i :
        { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
            PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                    PreZeroHypercover.{u_1, u, u + 1} X }.X
                i))
            ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                    PreZeroHypercover.{u_1, u, u + 1} X }.f
                i))
          x) ∧
    ∀
      (i :
        { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
            PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      P
        ({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
              PreZeroHypercover.{u_1, u, u + 1} X }.f
          i)

Tactic:
⟨fun x ↦ ?_, 𝒰.map_prop⟩

Premises used: AlgebraicGeometry.Scheme.AffineCover.map_prop, And.intro
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover.{u_1, u} P X
refine :
  ∀ (x : ↥X),
    ∃ (i :
      { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
          PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                  PreZeroHypercover.{u_1, u, u + 1} X }.X
              i))
          ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                  PreZeroHypercover.{u_1, u, u + 1} X }.f
              i))
        x
⊢ (∀ (x : ↥X),
      ∃ (i :
        { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
            PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                    PreZeroHypercover.{u_1, u, u + 1} X }.X
                i))
            ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                    PreZeroHypercover.{u_1, u, u + 1} X }.f
                i))
          x) ∧
    ∀
      (i :
        { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
            PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      P
        ({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
              PreZeroHypercover.{u_1, u, u + 1} X }.f
          i)

Tactic:
refine ⟨fun x ↦ ?_, 𝒰.map_prop⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover.{u_1, u} P X
x : ↥X
obtain :
  ∀ (y : ↥(Spec (𝒰.X (P := P) (𝒰.idx (P := P) x)))) (hy : (𝒰.f (P := P) (𝒰.idx (P := P) x)) y = x),
    ∃ (i :
      { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
          PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                  PreZeroHypercover.{u_1, u, u + 1} X }.X
              i))
          ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                  PreZeroHypercover.{u_1, u, u + 1} X }.f
              i))
        x
⊢ ∃ (i :
    { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
        PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.X
            i))
        ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.f
            i))
      x

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

Premises used: AlgebraicGeometry.Scheme.AffineCover.covers
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover.{u_1, u} P X
x : ↥X
y : ↥(Spec (𝒰.X (P := P) (𝒰.idx (P := P) x)))
hy : (𝒰.f (P := P) (𝒰.idx (P := P) x)) y = x
w :
  { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
      PreZeroHypercover.{u_1, u, u + 1} X }.I₀
w₁ :
  ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
          PreZeroHypercover.{u_1, u, u + 1} X }.X
      (𝒰.idx (P := P) x))
h :
  ({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) }.f
        (𝒰.idx (P := P) x))
      y =
    x
⊢ ∃ (i :
    { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
        PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.X
            i))
        ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.f
            i))
      x

Tactic:
use 𝒰.idx x, y

Premises used: AlgebraicGeometry.Scheme.AffineCover.idx