awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
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
have w : PreZeroHypercover.I₀ (C := Scheme) (S := X)
  { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }
Tactic: use x, (𝒰.exists_eq x).choose_spec.choose, (𝒰.exists_eq x).choose_spec.choose_spec
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
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) }
⊢ ∃ (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
have w₁ : ↥(PreZeroHypercover.X (S := X)
    { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X } x)
Tactic: use x, (𝒰.exists_eq x).choose_spec.choose, (𝒰.exists_eq x).choose_spec.choose_spec
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
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)
⊢ ∃ (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
have h : (PreZeroHypercover.f { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) } x)
    (sorry.choose (p := fun (y : ↥(𝒰.X (sorry.choose (p := fun (i : 𝒰.I₀) ↦ ∃ (y : ↥(𝒰.X i)), (𝒰.f i) y = x)))) ↦
      (𝒰.f (sorry.choose (p := fun (i : 𝒰.I₀) ↦ ∃ (y : ↥(𝒰.X i)), (𝒰.f i) y = x))) y = x)) =
  x
Tactic: use x, (𝒰.exists_eq x).choose_spec.choose, (𝒰.exists_eq x).choose_spec.choose_spec
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
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
⊢ X.OpenCover
have 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 sorry ≅ Spec.toLocallyRingedSpace.obj (op (R x)))) →
      X.OpenCover
Tactic: choose U R h using X.local_affine
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
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
⊢ 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
have 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 sorry } }),
      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 sorry : (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 sorry : (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 sorry } }),
    IsOpenImmersion
      (PreZeroHypercover.f
        { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x),
          f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict sorry : (Spec (R x)).Hom X } : PreZeroHypercover X }
        i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
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)
have refine : ∀ (x : ↥X),
  (PreZeroHypercover.f
        { I₀ := ↥X, X := fun (x : ↥X) ↦ Spec (R x), f := fun (x : ↥X) ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict sorry } } 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 sorry).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 sorry) :
        (↑(↑(Spec.toLocallyRingedSpace.obj (op (R x))).toPresheafedSpace : TopCat) : Type u)) =
    x
Tactic: refine ⟨fun x ↦ ⟨x, ⟨(e x).hom.base ⟨x, (U x).2⟩, ?_⟩⟩, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
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
⊢ (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
have 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 sorry).base) :
      (a : (↑(↑(X.restrict sorry).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 sorry) =
  x
Tactic: change ((((e x).hom ≫ (e x).inv).base ≫ (X.ofRestrict _).base)) ⟨x, _⟩ = x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
⊢ (↑(⨆ (i : 𝒰.I₀), Hom.opensRange (𝒰.f i)) : Set ↥X) = (↑⊤ : Set ↥X)
have rw : ⋃ (i : 𝒰.I₀), (↑(Hom.opensRange (𝒰.f i)) : Set ↥X) = (↑⊤ : Set ↥X)
Tactic: rw [Opens.coe_iSup]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (hypothesis)
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
⊢ X.OpenCover
have 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) ⊤
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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (hypothesis)
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
⊢ ∃ (y : ↥t),
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 (↑y : ↥X)))) ⇑(𝒰.f (Cover.idx 𝒰 (↑y : ↥X)))) x
have h' : Membership.mem (γ := Set ↥X) ⊤ x
Tactic: have h' : x ∈ (⊤ : Set X) := trivial
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (hypothesis)
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
⊢ ∃ (y : ↥t),
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 (↑y : ↥X)))) ⇑(𝒰.f (Cover.idx 𝒰 (↑y : ↥X)))) x
have 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
Tactic: rw [← Classical.choose_spec this, Set.mem_iUnion] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
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
⊢ ∃ (y : ↥t),
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 (↑y : ↥X)))) ⇑(𝒰.f (Cover.idx 𝒰 (↑y : ↥X)))) x
have 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
Tactic: rcases h' with ⟨y, _, ⟨hy, rfl⟩, hy'⟩
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (hypothesis)
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.OpenCover
have h : ∀ (x : ↥X),
  ∃ (y : ↥t),
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 (↑y : ↥X)))) ⇑(𝒰.f (Cover.idx 𝒰 (↑y : ↥X)))) x
Tactic: have h : ∀ x : X, ∃ y : t, x ∈ Set.range (𝒰.f (𝒰.idx y)) := by
    intro x
    have h' : x ∈ (⊤ : Set X) := trivial
    rw [← Classical.choose_spec this, Set.mem_iUnion] at h'
    rcases h' with ⟨y, _, ⟨hy, rfl⟩, hy'⟩
    exact ⟨⟨y, hy⟩, hy'⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
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) ⊤)
h :
  ∀ (x : ↥X),
    ∃ (y : ↥t),
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 (↑y : ↥X)))) ⇑(𝒰.f (Cover.idx 𝒰 (↑y : ↥X)))) x
⊢ PreZeroHypercover.presieve₀
      { I₀ := ↥t, X := fun (x : ↥t) ↦ 𝒰.X (Cover.idx 𝒰 (↑x : ↥X)), f := fun (x : ↥t) ↦ 𝒰.f (Cover.idx 𝒰 (↑x : ↥X)) } ∈
    (precoverage IsOpenImmersion).coverings X
have rw : (∀ (x : ↥X),
    ∃ (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X)
        { I₀ := ↥t, X := fun (x : ↥t) ↦ 𝒰.X (Cover.idx 𝒰 (↑x : ↥X)), f := fun (x : ↥t) ↦ 𝒰.f (Cover.idx 𝒰 (↑x : ↥X)) }),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := ↥t, X := fun (x : ↥t) ↦ 𝒰.X (Cover.idx 𝒰 (↑x : ↥X)),
                f := fun (x : ↥t) ↦ 𝒰.f (Cover.idx 𝒰 (↑x : ↥X)) : PreZeroHypercover X }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := ↥t, X := fun (x : ↥t) ↦ 𝒰.X (Cover.idx 𝒰 (↑x : ↥X)),
                f := fun (x : ↥t) ↦ 𝒰.f (Cover.idx 𝒰 (↑x : ↥X)) : PreZeroHypercover X }
              i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X)
        { I₀ := ↥t, X := fun (x : ↥t) ↦ 𝒰.X (Cover.idx 𝒰 (↑x : ↥X)), f := fun (x : ↥t) ↦ 𝒰.f (Cover.idx 𝒰 (↑x : ↥X)) }),
    IsOpenImmersion
      (PreZeroHypercover.f
        { I₀ := ↥t, X := fun (x : ↥t) ↦ 𝒰.X (Cover.idx 𝒰 (↑x : ↥X)), f := fun (x : ↥t) ↦ 𝒰.f (Cover.idx 𝒰 (↑x : ↥X)) :
          PreZeroHypercover X }
        i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace.{u} ↥(𝒰.X i)
⊢ CompactSpace.{u} ↥X
have intro : ∀ (val : Fintype 𝒰.I₀), CompactSpace.{u} ↥X
Tactic: cases nonempty_fintype 𝒰.I₀
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace.{u} ↥(𝒰.X i)
val : Fintype 𝒰.I₀
⊢ CompactSpace.{u} ↥X
have intro : IsCompact.{u} (X := ↥X) (⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))
Tactic: rw [← isCompact_univ_iff, ← 𝒰.iUnion_range]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace.{u} ↥(𝒰.X i)
val : Fintype 𝒰.I₀
⊢ IsCompact.{u} (X := ↥X) (⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))
have intro : ∀ (i : 𝒰.I₀), IsCompact (X := ↥X) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))
Tactic: apply isCompact_iUnion
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace.{u} ↥(𝒰.X i)
val : Fintype 𝒰.I₀
i : 𝒰.I₀
⊢ IsCompact (X := ↥X) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))
have intro : CompactSpace.{u} (↑(Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u)
Tactic: rw [isCompact_iff_compactSpace]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → (↑R : Type u_2)
hs : Eq (α := Ideal (↑R : Type u_2)) (Ideal.span (Set.range s)) ⊤
x : ↥(Spec R)
⊢ ∃ (i : ι), s i ∉ x.asIdeal
have by_contra! : ∀ (h : ∀ (i : ι), s i ∈ x.asIdeal), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → (↑R : Type u_2)
hs : Eq (α := Ideal (↑R : Type u_2)) (Ideal.span (Set.range s)) ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ False
have apply : x.asIdeal = ⊤
Tactic: apply x.2.ne_top
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → (↑R : Type u_2)
hs : Eq (α := Ideal (↑R : Type u_2)) (Ideal.span (Set.range s)) ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ x.asIdeal = ⊤
have rwa : ⊤ ≤ x.asIdeal
Tactic: rwa [← top_le_iff, ← hs, Ideal.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → (↑R : Type u_2)
hs : Eq (α := Ideal (↑R : Type u_2)) (Ideal.span (Set.range s)) ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
rwa : ⊤ ≤ x.asIdeal
⊢ x.asIdeal = ⊤
have rwa₁ : Ideal.span (Set.range s) ≤ x.asIdeal
Tactic: rwa [← top_le_iff, ← hs, Ideal.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → (↑R : Type u_2)
hs : Eq (α := Ideal (↑R : Type u_2)) (Ideal.span (Set.range s)) ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
rwa : ⊤ ≤ x.asIdeal
rwa₁ : Ideal.span (Set.range s) ≤ x.asIdeal
⊢ x.asIdeal = ⊤
have rwa₂ : Set.range s ⊆ (↑x.asIdeal : Set (↑R : Type u_2))
Tactic: rwa [← top_le_iff, ← hs, Ideal.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → (↑R : Type u_2)
hs : Eq (α := Ideal (↑R : Type u_2)) (Ideal.span (Set.range s)) ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
rwa : ⊤ ≤ x.asIdeal
rwa₁ : Ideal.span (Set.range s) ≤ x.asIdeal
rwa₂ : Set.range s ⊆ (↑x.asIdeal : Set (↑R : Type u_2))
⊢ x.asIdeal = ⊤
have rwa₃ : ∀ (y : ι), s y ∈ (↑x.asIdeal : Set (↑R : Type u_2))
Tactic: rwa [← top_le_iff, ← hs, Ideal.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → (↑R : Type u_2)
hs : Eq (α := Ideal (↑R : Type u_2)) (Ideal.span (Set.range s)) ⊤
x : ↥(Spec R)
⊢ ι
have have : (this : ∃ (i : ι), s i ∉ x.asIdeal) → ι
Tactic: have : ∃ i, s i ∉ x.asIdeal := by
      by_contra! h; apply x.2.ne_top; rwa [← top_le_iff, ← hs, Ideal.span_le, Set.range_subset_iff]