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
𝒰 : Cover.{v, u} (precoverage P) X
rw :
  (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
      P
        (PreZeroHypercover.f
          { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X } i)
⊢ PreZeroHypercover.presieve₀ { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx 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 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
𝒰 : Cover.{v, u} (precoverage P) X
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
      P
        (PreZeroHypercover.f
          { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X } i)

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

Premises used: And.intro, AlgebraicGeometry.Scheme.Cover.map_prop, AlgebraicGeometry.Scheme.Cover.idx
-- 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
𝒰 : Cover.{v, u} (precoverage P) X
refine :
  ∀ (x : ↥X),
    ∃ (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X)
        { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X }
              i))
        x
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
      P
        (PreZeroHypercover.f
          { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X } i)

Tactic:
refine ⟨fun x ↦ ?_, fun i ↦ 𝒰.map_prop _⟩
-- 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
𝒰 : Cover.{v, u} (precoverage P) X
x : ↥X
w :
  PreZeroHypercover.I₀ (C := Scheme) (S := X)
    { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }
w₁ :
  ↥(PreZeroHypercover.X (S := X)
      { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X } x)
h :
  (PreZeroHypercover.f { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) } x)
      (⋯.choose (p := fun (y : ↥(𝒰.X (⋯.choose (p := fun (i : 𝒰.I₀) ↦ ∃ (y : ↥(𝒰.X i)), (𝒰.f i) y = x)))) ↦
        (𝒰.f (⋯.choose (p := fun (i : 𝒰.I₀) ↦ ∃ (y : ↥(𝒰.X i)), (𝒰.f i) y = x))) y = x)) =
    x
⊢ ∃ (i :
    PreZeroHypercover.I₀ (C := Scheme) (S := X)
      { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X } i))
        ⇑(PreZeroHypercover.f
            { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X } i))
      x

Tactic:
use x, (𝒰.exists_eq x).choose_spec.choose, (𝒰.exists_eq x).choose_spec.choose_spec

Premises used: Exists.choose_spec, AlgebraicGeometry.Scheme.Cover.exists_eq, Exists.choose
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X Y Z : Scheme
𝒰 : OpenCover.{u_1, u} X
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
i : 𝒰.I₀
⊢ IsOpenImmersion (𝒰.f i)

Tactic:
𝒰.map_prop i

Premises used: AlgebraicGeometry.Scheme.Cover.map_prop
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X_1 Y Z : Scheme
𝒰 : X_1.OpenCover
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
choose :
  (U : (x : (↑X.toTopCat : Type u)) → OpenNhds x) →
    (R : (x : (↑X.toTopCat : Type u)) → CommRingCat.{u}) →
      (h : ∀ (x : (↑X.toTopCat : Type u)), Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))) →
        X.OpenCover
⊢ X.OpenCover

Tactic:
choose U R h using X.local_affine

Premises used: AlgebraicGeometry.Scheme.local_affine
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X_1 Y Z : Scheme
𝒰 : X_1.OpenCover
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : (↑X.toTopCat : Type u)) → OpenNhds x
R : (x : (↑X.toTopCat : Type u)) → CommRingCat
h : ∀ (x : (↑X.toTopCat : Type u)), Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : (↑X.toTopCat : Type u)) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) :=
  fun (x : (↑X.toTopCat : Type u)) ↦ ⋯.some
rw :
  (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
            f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
                  f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ : (Spec (R x)).Hom X } :
                  PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
                  f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ : (Spec (R x)).Hom X } :
                  PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
            f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
            f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ : (Spec (R x)).Hom X } : PreZeroHypercover X }
          i)
⊢ PreZeroHypercover.presieve₀
      { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x), f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } } ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X_1 Y Z : Scheme
𝒰 : X_1.OpenCover
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : (↑X.toTopCat : Type u)) → OpenNhds x
R : (x : (↑X.toTopCat : Type u)) → CommRingCat
h : ∀ (x : (↑X.toTopCat : Type u)), Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : (↑X.toTopCat : Type u)) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) :=
  fun (x : (↑X.toTopCat : Type u)) ↦ ⋯.some
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
            f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
                  f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ : (Spec (R x)).Hom X } :
                  PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
                  f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ : (Spec (R x)).Hom X } :
                  PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
            f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
            f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ : (Spec (R x)).Hom X } : PreZeroHypercover X }
          i)

Tactic:
⟨fun x ↦ ⟨x, ⟨(e x).hom.base ⟨x, (U x).2⟩, ?_⟩⟩, inferInstance⟩

Premises used: CategoryTheory.ConcreteCategory.hom, inferInstance, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, Subtype.mk, And.intro, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.Iso.hom, DFunLike.coe, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X_1 Y Z : Scheme
𝒰 : X_1.OpenCover
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : (↑X.toTopCat : Type u)) → OpenNhds x
R : (x : (↑X.toTopCat : Type u)) → CommRingCat
h : ∀ (x : (↑X.toTopCat : Type u)), Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : (↑X.toTopCat : Type u)) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) :=
  fun (x : (↑X.toTopCat : Type u)) ↦ ⋯.some
refine :
  ∀ (x : ↥X),
    (PreZeroHypercover.f
          { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x), f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }
          x)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (e x).hom.base :
              (a : (↑(↑(X.restrict ⋯).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑(Spec.toLocallyRingedSpace.obj (op (R x))).toPresheafedSpace : TopCat) : Type u))
            (Subtype.mk (p := fun (x_1 : (↑X.toTopCat : Type u)) ↦
              x_1 ∈ (↑(U x) : TopologicalSpace.Opens (↑X.toTopCat : Type u))) x ⋯) :
          (↑(↑(Spec.toLocallyRingedSpace.obj (op (R x))).toPresheafedSpace : TopCat) : Type u)) =
      x
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
            f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
                  f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ : (Spec (R x)).Hom X } :
                  PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
                  f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ : (Spec (R x)).Hom X } :
                  PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
            f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
            f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ : (Spec (R x)).Hom X } : PreZeroHypercover X }
          i)

Tactic:
refine ⟨fun x ↦ ⟨x, ⟨(e x).hom.base ⟨x, (U x).2⟩, ?_⟩⟩, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X_1 Y Z : Scheme
𝒰 : X_1.OpenCover
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : (↑X.toTopCat : Type u)) → OpenNhds x
R : (x : (↑X.toTopCat : Type u)) → CommRingCat
h : ∀ (x : (↑X.toTopCat : Type u)), Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : (↑X.toTopCat : Type u)) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) :=
  fun (x : (↑X.toTopCat : Type u)) ↦ ⋯.some
x : ↥X
change :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (((e x).hom ≫ (e x).inv).base ≫ (X.ofRestrict ⋯).base) :
        (a : (↑(↑(X.restrict ⋯).toPresheafedSpace : TopCat) : Type u)) → ↥X)
      (Subtype.mk (p := fun (x_1 : (↑X.toTopCat : Type u)) ↦
        x_1 ∈ (↑(U x) : TopologicalSpace.Opens (↑X.toTopCat : Type u))) x ⋯) =
    x
⊢ (PreZeroHypercover.f
        { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x), f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } } x)
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (e x).hom.base :
            (a : (↑(↑(X.restrict ⋯).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(Spec.toLocallyRingedSpace.obj (op (R x))).toPresheafedSpace : TopCat) : Type u))
          (Subtype.mk (p := fun (x_1 : (↑X.toTopCat : Type u)) ↦
            x_1 ∈ (↑(U x) : TopologicalSpace.Opens (↑X.toTopCat : Type u))) x ⋯) :
        (↑(↑(Spec.toLocallyRingedSpace.obj (op (R x))).toPresheafedSpace : TopCat) : Type u)) =
    x

Tactic:
change ((((e x).hom ≫ (e x).inv).base ≫ (X.ofRestrict _).base)) ⟨x, _⟩ = x

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.mk, AlgebraicGeometry.Scheme.ofRestrict, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X_1 Y Z : Scheme
𝒰 : X_1.OpenCover
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : (↑X.toTopCat : Type u)) → OpenNhds x
R : (x : (↑X.toTopCat : Type u)) → CommRingCat
h : ∀ (x : (↑X.toTopCat : Type u)), Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : (↑X.toTopCat : Type u)) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) :=
  fun (x : (↑X.toTopCat : Type u)) ↦ ⋯.some
⊢ X.OpenCover

Tactic:
exact
  { I₀ := X
    X x := Spec (R x)
    f x := ⟨(e x).inv ≫ X.toLocallyRingedSpace.ofRestrict _⟩
    mem₀ := by
      rw [presieve₀_mem_precoverage_iff]
      refine ⟨fun x ↦ ⟨x, ⟨(e x).hom.base ⟨x, (U x).2⟩, ?_⟩⟩, inferInstance⟩
      change ((((e x).hom ≫ (e x).inv).base ≫ (X.ofRestrict _).base)) ⟨x, _⟩ = x
      cat_disch }
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
rw : ⋃ (i : 𝒰.I₀), (↑(Hom.opensRange (𝒰.f i)) : Set ↥X) = (↑⊤ : Set ↥X)
⊢ (↑(⨆ (i : 𝒰.I₀), Hom.opensRange (𝒰.f i)) : Set ↥X) = (↑⊤ : Set ↥X)

Tactic:
rw [Opens.coe_iSup]

Premises used: TopologicalSpace.Opens.coe_iSup
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
⊢ ⋃ (i : 𝒰.I₀), (↑(Hom.opensRange (𝒰.f i)) : Set ↥X) = (↑⊤ : Set ↥X)

Tactic:
𝒰.iUnion_range

Premises used: AlgebraicGeometry.Scheme.Cover.iUnion_range, Set.univ, setOf, Set.range
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
⊢ ⋃ (i : 𝒰.I₀), (↑(Hom.opensRange (𝒰.f i)) : Set ↥X) = (↑⊤ : Set ↥X)

Tactic:
exact 𝒰.iUnion_range

Premises used: AlgebraicGeometry.Scheme.Cover.iUnion_range
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
⊢ IsOpenCover.{u_1, u} (X := ↥X) fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)

Tactic:
.mk 𝒰.iSup_opensRange

Premises used: AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, TopologicalSpace.IsOpenCover.mk
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X_1 Y Z : Scheme
𝒰_1 : X_1.OpenCover
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
X : Scheme
𝒰 : OpenCover.{u_1, u} X
H : CompactSpace.{u} ↥X
⊢ ∃ (t : Finset ↥X),
    Eq.{u + 1} (α := Set ↥X)
      (⋃ x ∈ t, (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x) ⊤

Tactic:
have :=
    @CompactSpace.elim_nhds_subcover _ _ H (fun x : X => Set.range (𝒰.f (𝒰.idx x)))
      fun x => (IsOpenImmersion.isOpen_range (𝒰.f (𝒰.idx x))).mem_nhds (𝒰.covers x)
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X_1 Y Z : Scheme
𝒰_1 : X_1.OpenCover
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
X : Scheme
𝒰 : OpenCover.{u_1, u} X
H : CompactSpace.{u} ↥X
this :
  ∃ (t : Finset ↥X),
    Eq.{u + 1} (α := Set ↥X)
      (⋃ x ∈ t, (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x) ⊤
t : Finset ↥X :=
  this.choose (p := fun (t : Finset ↥X) ↦
    Eq.{u + 1} (α := Set ↥X)
      (⋃ x ∈ t, (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x) ⊤)
x : ↥X
⊢ Membership.mem (γ := Set ↥X) ⊤ x

Tactic:
have h' : x ∈ (⊤ : Set X) := trivial
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X_1 Y Z : Scheme
𝒰_1 : X_1.OpenCover
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
X : Scheme
𝒰 : OpenCover.{u_1, u} X
H : CompactSpace.{u} ↥X
this :
  ∃ (t : Finset ↥X),
    Eq.{u + 1} (α := Set ↥X)
      (⋃ x ∈ t, (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x) ⊤
t : Finset ↥X :=
  this.choose (p := fun (t : Finset ↥X) ↦
    Eq.{u + 1} (α := Set ↥X)
      (⋃ x ∈ t, (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x) ⊤)
x : ↥X
h' : Membership.mem (γ := Set ↥X) ⊤ x
⊢ ∃ (i : ↥X),
    Membership.mem (γ := Set ↥X)
      (⋃ (_ :
        i ∈
          Classical.choose (p := fun (x : Finset ↥X) ↦
            Eq.{u + 1} (α := Set ↥X)
              (⋃ x_1 ∈ x,
                (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x_1)
              ⊤)
            this),
        (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) i)
      x

Tactic:
rw [← Classical.choose_spec this, Set.mem_iUnion] at h'

Premises used: Set.mem_iUnion, Classical.choose_spec
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X_1 Y Z : Scheme
𝒰_1 : X_1.OpenCover
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
X : Scheme
𝒰 : OpenCover.{u_1, u} X
H : CompactSpace.{u} ↥X
this :
  ∃ (t : Finset ↥X),
    Eq.{u + 1} (α := Set ↥X)
      (⋃ x ∈ t, (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x) ⊤
t : Finset ↥X :=
  this.choose (p := fun (t : Finset ↥X) ↦
    Eq.{u + 1} (α := Set ↥X)
      (⋃ x ∈ t, (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x) ⊤)
x : ↥X
h' :
  ∃ (i : ↥X),
    Membership.mem (γ := Set ↥X)
      (⋃ (_ :
        i ∈
          Classical.choose (p := fun (x : Finset ↥X) ↦
            Eq.{u + 1} (α := Set ↥X)
              (⋃ x_1 ∈ x,
                (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x_1)
              ⊤)
            this),
        (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) i)
      x
rcases :
  ∀ (y : ↥X)
    (hy :
      y ∈
        Classical.choose (p := fun (x : Finset ↥X) ↦
          Eq.{u + 1} (α := Set ↥X)
            (⋃ x_1 ∈ x, (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x_1)
            ⊤)
          this)
    (hy' :
      Membership.mem (γ := Set ↥X)
        ((fun
              (h :
                y ∈
                  Classical.choose (p := fun (x : Finset ↥X) ↦
                    Eq.{u + 1} (α := Set ↥X)
                      (⋃ x_1 ∈ x,
                        (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x_1)
                      ⊤)
                    this) ↦
            ((fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) y : Set ↥X))
          hy)
        x),
    ∃ (y : ↥t),
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 (↑y : ↥X)))) ⇑(𝒰.f (Cover.idx 𝒰 (↑y : ↥X)))) x
⊢ ∃ (y : ↥t),
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 (↑y : ↥X)))) ⇑(𝒰.f (Cover.idx 𝒰 (↑y : ↥X)))) x

Tactic:
rcases h' with ⟨y, _, ⟨hy, rfl⟩, hy'⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X_1 Y Z : Scheme
𝒰_1 : X_1.OpenCover
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
X : Scheme
𝒰 : OpenCover.{u_1, u} X
H : CompactSpace.{u} ↥X
this :
  ∃ (t : Finset ↥X),
    Eq.{u + 1} (α := Set ↥X)
      (⋃ x ∈ t, (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x) ⊤
t : Finset ↥X :=
  this.choose (p := fun (t : Finset ↥X) ↦
    Eq.{u + 1} (α := Set ↥X)
      (⋃ x ∈ t, (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x) ⊤)
x y : ↥X
hy :
  y ∈
    Classical.choose (p := fun (x : Finset ↥X) ↦
      Eq.{u + 1} (α := Set ↥X)
        (⋃ x_1 ∈ x, (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x_1) ⊤)
      this
hy' :
  Membership.mem (γ := Set ↥X)
    ((fun
          (h :
            y ∈
              Classical.choose (p := fun (x : Finset ↥X) ↦
                Eq.{u + 1} (α := Set ↥X)
                  (⋃ x_1 ∈ x,
                    (fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) x_1)
                  ⊤)
                this) ↦
        ((fun (x : ↥X) ↦ (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 x))) ⇑(𝒰.f (Cover.idx 𝒰 x)) : Set ↥X)) y : Set ↥X))
      hy)
    x
⊢ ∃ (y : ↥t),
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 (↑y : ↥X)))) ⇑(𝒰.f (Cover.idx 𝒰 (↑y : ↥X)))) x

Tactic:
⟨⟨y, hy⟩, hy'⟩

Premises used: Subtype.mk, Exists.intro