awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
rw :
  (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := (↑X.affineOpens : Type u),
                  X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := (↑X.affineOpens : Type u),
                  X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
          i)
⊢ PreZeroHypercover.presieve₀
      { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
        f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι } ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := (↑X.affineOpens : Type u),
                  X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := (↑X.affineOpens : Type u),
                  X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
          i)

Tactic:
⟨fun x ↦ ?_, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
refine :
  ∀ (x : ↥X),
    ∃ (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X)
        { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
          f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
                f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
                f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
              i))
        x
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := (↑X.affineOpens : Type u),
                  X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := (↑X.affineOpens : Type u),
                  X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
          i)

Tactic:
refine ⟨fun x ↦ ?_, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
x : ↥X
h :
  Membership.mem (γ := Set ↥X)
    (Set.range (ι :=
      ↥(PreZeroHypercover.X (S := X)
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
          (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
            (⋯.choose (p := fun (U' : TopologicalSpace.Opens ↥X) ↦ U' ∈ X.affineOpens ∧ x ∈ U' ∧ U' ≤ ⊤)) ⋯)))
      ⇑(PreZeroHypercover.f
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }
          (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
            (⋯.choose (p := fun (U' : TopologicalSpace.Opens ↥X) ↦ U' ∈ X.affineOpens ∧ x ∈ U' ∧ U' ≤ ⊤)) ⋯)))
    x
⊢ ∃ (i :
    PreZeroHypercover.I₀ (C := Scheme) (S := X)
      { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
        f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
              f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
              f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
            i))
      x

Tactic:
use ⟨(isBasis_iff_nbhd.mp X.isBasis_affineOpens (mem_top x)).choose,
      (isBasis_iff_nbhd.mp X.isBasis_affineOpens (mem_top x)).choose_spec.1⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
x : ↥X
⊢ Membership.mem (γ := Set ↥X)
    (Set.range (ι :=
      ↥(PreZeroHypercover.X (S := X)
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
          (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
            (⋯.choose (p := fun (U' : TopologicalSpace.Opens ↥X) ↦ U' ∈ X.affineOpens ∧ x ∈ U' ∧ U' ≤ ⊤)) ⋯)))
      ⇑(PreZeroHypercover.f
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }
          (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
            (⋯.choose (p := fun (U' : TopologicalSpace.Opens ↥X) ↦ U' ∈ X.affineOpens ∧ x ∈ U' ∧ U' ≤ ⊤)) ⋯)))
    x

Tactic:
simpa using (isBasis_iff_nbhd.mp X.isBasis_affineOpens (mem_top x)).choose_spec.2.1

Premises used: TopologicalSpace.Opens.mem_top, Exists.choose_spec, TopologicalSpace.Opens.isBasis_iff_nbhd, And.right, And.left, Iff.mp, AlgebraicGeometry.Scheme.isBasis_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
i j : X.directedAffineCover.I₀
simp : i ≤ j ↔ i ≤ j
⊢ i ≤ j ↔ Hom.opensRange (X.directedAffineCover.f i) ≤ Hom.opensRange (X.directedAffineCover.f j)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
i j : X.directedAffineCover.I₀
⊢ i ≤ j ↔ i ≤ j

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
⊢ TopologicalSpace.Opens.IsBasis X.affineOpens

Tactic:
X.isBasis_affineOpens

Premises used: AlgebraicGeometry.Scheme.isBasis_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
h : (Set.range fun (i : X.directedAffineCover.I₀) ↦ Hom.opensRange (X.directedAffineCover.f i)) = X.affineOpens
⊢ TopologicalSpace.Opens.IsBasis.{u} (α := ↥X)
    (Set.range fun (i : X.directedAffineCover.I₀) ↦ Hom.opensRange (X.directedAffineCover.f i))

Tactic:
convert! X.isBasis_affineOpens

Premises used: AlgebraicGeometry.Scheme.isBasis_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
⊢ (Set.range fun (i : X.directedAffineCover.I₀) ↦ Hom.opensRange (X.directedAffineCover.f i)) = X.affineOpens

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
X : Scheme
U V : (↑X.affineOpens : Type u)
hUV : U ≤ V
⊢ Cover.trans (P := IsOpenImmersion) X.directedAffineCover (homOfLE hUV) = X.homOfLE hUV

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.homOfLE, AlgebraicGeometry.Scheme.restrict, AlgebraicGeometry.Scheme.ofRestrict, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Opens.toScheme, AlgebraicGeometry.Scheme.Cover.trans, rfl
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X : Scheme
inst : JointlySurjective K
𝒰 : Cover.{u_1, u} K X
x : ↥X
obtain : ∀ ⦃Y : Scheme.{u}⦄ (i : 𝒰.I₀) (y : ↥(𝒰.X i)) (hy : (𝒰.f i) y = x), ∃ (i : 𝒰.I₀) (y : ↥(𝒰.X i)), (𝒰.f i) y = x
⊢ ∃ (i : 𝒰.I₀) (y : ↥(𝒰.X i)), (𝒰.f i) y = x

Tactic:
obtain ⟨Y, g, ⟨i⟩, y, hy⟩ := JointlySurjective.exists_eq 𝒰.presieve₀ 𝒰.mem₀ x

Premises used: CategoryTheory.PreZeroHypercover.presieve₀, CategoryTheory.Precoverage.ZeroHypercover.mem₀, AlgebraicGeometry.Scheme.JointlySurjective.exists_eq, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X : Scheme
inst : JointlySurjective K
𝒰 : Cover.{u_1, u} K X
x : ↥X
Y : Scheme
i : 𝒰.I₀
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = x
w : 𝒰.I₀
w₁ : ↥(𝒰.X i)
h : (𝒰.f i) y = x
⊢ ∃ (i : 𝒰.I₀) (y : ↥(𝒰.X i)), (𝒰.f i) y = x

Tactic:
use i, y
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X : Scheme
inst : JointlySurjective K
𝒰 : Cover.{u_1, u} K X
x : ↥X
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X (𝒰.idx x))) ⇑(𝒰.f (𝒰.idx x))) x

Tactic:
(𝒰.exists_eq x).choose_spec

Premises used: Exists.choose_spec, Set.Mem, setOf, AlgebraicGeometry.Scheme.Cover.exists_eq, Set.range, AlgebraicGeometry.Scheme.Cover.idx
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
inst : JointlySurjective K
X : Scheme
𝒰 : Cover.{u_1, u} K X
rw : ∀ (x : ↥X), Membership.mem (γ := Set ↥X) (⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x
⊢ Eq.{u + 1} (α := Set ↥X) (⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
inst : JointlySurjective K
X : Scheme
𝒰 : Cover.{u_1, u} K X
x : ↥X
rw : ∃ (i : 𝒰.I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x
⊢ Membership.mem (γ := Set ↥X) (⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x

Tactic:
rw [Set.mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
inst : JointlySurjective K
X : Scheme
𝒰 : Cover.{u_1, u} K X
x : ↥X
⊢ ∃ (i : 𝒰.I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x

Tactic:
𝒰.exists_eq x

Premises used: Set.Mem, setOf, AlgebraicGeometry.Scheme.Cover.exists_eq, Set.range
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
inst : JointlySurjective K
X : Scheme
𝒰 : Cover.{u_1, u} K X
x : ↥X
⊢ ∃ (i : 𝒰.I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x

Tactic:
exact 𝒰.exists_eq x

Premises used: 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
inst_1 : JointlySurjective K
inst_2 : Nonempty.{u + 1} ↥X
𝒰 : Cover.{u_1, u} K X
obtain : ∀ (i : 𝒰.I₀), (∃ (y : ↥(𝒰.X i)), (𝒰.f i) y = inst_2.some) → Nonempty.{u_1 + 1} 𝒰.I₀
⊢ Nonempty.{u_1 + 1} 𝒰.I₀

Tactic:
obtain ⟨i, _⟩ := 𝒰.exists_eq ‹Nonempty X›.some

Premises used: Nonempty.some, 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
inst_1 : JointlySurjective K
inst_2 : Nonempty.{u + 1} ↥X
𝒰 : Cover.{u_1, u} K X
i : 𝒰.I₀
h : ∃ (y : ↥(𝒰.X i)), (𝒰.f i) y = inst_2.some
val : 𝒰.I₀
⊢ Nonempty.{u_1 + 1} 𝒰.I₀

Tactic:
use i
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
X : Scheme
P : MorphismProperty Scheme
E : PreZeroHypercover.{u_1, u, u + 1} X
⊢ E.presieve₀ ∈ (precoverage P).coverings X ↔
    (∀ (x : ↥X), ∃ (i : E.I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(E.X i)) ⇑(E.f i)) x) ∧
      ∀ (i : E.I₀), P (E.f i)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
X : Scheme
P : MorphismProperty Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
i : 𝒰.I₀
⊢ P (𝒰.f i)

Tactic:
𝒰.mem₀.2 ⟨i⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, And.right, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X Y Z : Scheme
𝒰 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
J : Type u_1
obj : J → Scheme
map : (j : J) → obj j ⟶ X
covers : ∀ (x : ↥X), ∃ (j : J) (y : ↥(obj j)), (map j) y = x
map_prop : ∀ (j : J), P (map j)
simp_rw : (∀ (x : ↥X), ∃ (i : J) (y : ↥(obj i)), (map i) y = x) ∧ ∀ (i : J), P (map 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:
simp_rw [presieve₀_mem_precoverage_iff, Set.mem_range]

Premises used: Set.mem_range, AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X Y Z : Scheme
𝒰 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
J : Type u_1
obj : J → Scheme
map : (j : J) → obj j ⟶ X
covers : ∀ (x : ↥X), ∃ (j : J) (y : ↥(obj j)), (map j) y = x
map_prop : ∀ (j : J), P (map j)
⊢ (∀ (x : ↥X), ∃ (i : J) (y : ↥(obj i)), (map i) y = x) ∧ ∀ (i : J), P (map i)

Tactic:
grind
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y_1 Z : Scheme
𝒰 : Cover K X_1
f_1 : X_1 ⟶ Z
g : Y_1 ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f_1) g
P Q : MorphismProperty Scheme
inst_1 : P.ContainsIdentities
inst_2 : P.RespectsIso
X Y : Scheme
f : X ⟶ Y
inst_3 : IsIso f
x : ↥Y
⊢ ((fun (x : PUnit.{v + 1}) ↦ f) PUnit.unit) ((inv f) x : ↥X) = x

Tactic:
simp [← Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
h : R ∈ (precoverage P).coverings X
x : ↥X
hR : R ∈ jointlySurjectivePrecoverage.coverings X
right : R ∈ P.precoverage.coverings X
⊢ ∀ (x : forget.obj X),
    ∃ (Y : Scheme.{u}) (f : Y ⟶ X),
      R f ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (forget.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (forget.obj Y))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map f)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj Y)) → (fun (X : Type u) ↦ X) (forget.obj X)))
          x

Tactic:
rw [jointlySurjectivePrecoverage, Presieve.mem_comap_jointlySurjectivePrecoverage_iff] at hR

Premises used: AlgebraicGeometry.Scheme.jointlySurjectivePrecoverage, CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
h : R ∈ (precoverage P).coverings X
x : ↥X
hR : R ∈ jointlySurjectivePrecoverage.coverings X
right : R ∈ P.precoverage.coverings X
hR₁ :
  ∀ (x : forget.obj X),
    ∃ (Y : Scheme.{u}) (f : Y ⟶ X),
      R f ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (forget.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (forget.obj Y))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map f)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj Y)) → (fun (X : Type u) ↦ X) (forget.obj X)))
          x
⊢ R ∈ P.precoverage.coverings X

Tactic:
rw [jointlySurjectivePrecoverage, Presieve.mem_comap_jointlySurjectivePrecoverage_iff] at hR

Premises used: AlgebraicGeometry.Scheme.jointlySurjectivePrecoverage, CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
h : R ∈ (precoverage P).coverings X
x : ↥X
hR :
  ∀ (x : forget.obj X),
    ∃ (Y : Scheme.{u}) (f : Y ⟶ X),
      R f ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (forget.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (forget.obj Y))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map f)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj Y)) → (fun (X : Type u) ↦ X) (forget.obj X)))
          x
right : R ∈ P.precoverage.coverings X
obtain :
  ∀ (Y : Scheme.{u}) (g : Y ⟶ X) (hg : R g)
    (heq :
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (forget.obj X)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (forget.obj Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map g)) :
            (a : (fun (X : Type u) ↦ X) (forget.obj Y)) → (fun (X : Type u) ↦ X) (forget.obj X)))
        x),
    ∃ (Y : Scheme.{u}) (g : Y ⟶ X), R g ∧ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥Y) ⇑g) x
⊢ ∃ (Y : Scheme.{u}) (g : Y ⟶ X), R g ∧ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥Y) ⇑g) x

Tactic:
obtain ⟨Y, g, hg, heq⟩ := hR x
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y_1 Z : Scheme
𝒰 : Cover K X_1
f : X_1 ⟶ Z
g_1 : Y_1 ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g_1
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
h : R ∈ (precoverage P).coverings X
x : ↥X
hR :
  ∀ (x : forget.obj X),
    ∃ (Y : Scheme.{u}) (f : Y ⟶ X),
      R f ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (forget.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (forget.obj Y))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map f)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj Y)) → (fun (X : Type u) ↦ X) (forget.obj X)))
          x
right_1 : R ∈ P.precoverage.coverings X
Y : Scheme
g : Y ⟶ X
hg : R g
heq :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (forget.obj X)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (forget.obj Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map g)) :
        (a : (fun (X : Type u) ↦ X) (forget.obj Y)) → (fun (X : Type u) ↦ X) (forget.obj X)))
    x
right : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥Y) ⇑g) x
⊢ ∃ (Y : Scheme.{u}) (g : Y ⟶ X), R g ∧ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥Y) ⇑g) x

Tactic:
use Y, g, hg
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y_1 Z : Scheme
𝒰 : Cover K X_1
f : X_1 ⟶ Z
g_1 : Y_1 ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g_1
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
h : R ∈ (precoverage P).coverings X
x : ↥X
hR :
  ∀ (x : forget.obj X),
    ∃ (Y : Scheme.{u}) (f : Y ⟶ X),
      R f ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (forget.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (forget.obj Y))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map f)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj Y)) → (fun (X : Type u) ↦ X) (forget.obj X)))
          x
right : R ∈ P.precoverage.coverings X
Y : Scheme
g : Y ⟶ X
hg : R g
heq :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (forget.obj X)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (forget.obj Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map g)) :
        (a : (fun (X : Type u) ↦ X) (forget.obj Y)) → (fun (X : Type u) ↦ X) (forget.obj X)))
    x
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥Y) ⇑g) x

Tactic:
heq

Premises used: Set.Mem
-- Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Goal:
K : Precoverage Scheme
X_1 Y_1 Z : Scheme
𝒰 : Cover K X_1
f : X_1 ⟶ Z
g_1 : Y_1 ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g_1
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
h : R ∈ (precoverage P).coverings X
x : ↥X
hR :
  ∀ (x : forget.obj X),
    ∃ (Y : Scheme.{u}) (f : Y ⟶ X),
      R f ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (forget.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (forget.obj Y))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map f)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj Y)) → (fun (X : Type u) ↦ X) (forget.obj X)))
          x
right : R ∈ P.precoverage.coverings X
Y : Scheme
g : Y ⟶ X
hg : R g
heq :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (forget.obj X)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (forget.obj Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map g)) :
        (a : (fun (X : Type u) ↦ X) (forget.obj Y)) → (fun (X : Type u) ↦ X) (forget.obj X)))
    x
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥Y) ⇑g) x

Tactic:
exact heq