awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ⟨⟨y, hy⟩, hy'⟩
-- 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),
    ∃ (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'⟩
-- 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) ⊤)
h :
  ∀ (x : ↥X),
    ∃ (y : ↥t),
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 (↑y : ↥X)))) ⇑(𝒰.f (Cover.idx 𝒰 (↑y : ↥X)))) x
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)
⊢ 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

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
𝒰_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
⊢ (∀ (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:
⟨h, inferInstance⟩

Premises used: inferInstance, And.intro
-- 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) ⊤)
h :
  ∀ (x : ↥X),
    ∃ (y : ↥t),
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 (↑y : ↥X)))) ⇑(𝒰.f (Cover.idx 𝒰 (↑y : ↥X)))) x
⊢ (∀ (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:
exact ⟨h, inferInstance⟩
-- 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) ⊤)
h :
  ∀ (x : ↥X),
    ∃ (y : ↥t),
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X (Cover.idx 𝒰 (↑y : ↥X)))) ⇑(𝒰.f (Cover.idx 𝒰 (↑y : ↥X)))) x
⊢ X.OpenCover

Tactic:
exact
    { I₀ := t
      X := fun x => 𝒰.X (𝒰.idx x.1)
      f := fun x => 𝒰.f (𝒰.idx x.1)
      mem₀ := by
        rw [presieve₀_mem_precoverage_iff]
        exact ⟨h, inferInstance⟩ }
-- 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
H : CompactSpace.{u} ↥X
⊢ Fintype
    (PreZeroHypercover.I₀ (C := Scheme) (S := X)
      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
        (have this := ⋯;
        let t :=
          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)
              ⊤);
        have h := ⋯;
        { I₀ := ↥t, X := fun (x : ↥t) ↦ 𝒰.X (Cover.idx 𝒰 (↑x : ↥X)), f := fun (x : ↥t) ↦ 𝒰.f (Cover.idx 𝒰 (↑x : ↥X)),
          mem₀ := ⋯ })))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace.{u} ↥(𝒰.X i)
intro : ∀ (val : Fintype 𝒰.I₀), CompactSpace.{u} ↥X
⊢ CompactSpace.{u} ↥X

Tactic:
cases nonempty_fintype 𝒰.I₀

Premises used: CategoryTheory.PreZeroHypercover.I₀, nonempty_fintype, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace.{u} ↥(𝒰.X i)
val : Fintype 𝒰.I₀
intro : IsCompact.{u} (X := ↥X) (⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))
⊢ CompactSpace.{u} ↥X

Tactic:
rw [← isCompact_univ_iff, ← 𝒰.iUnion_range]

Premises used: AlgebraicGeometry.Scheme.Cover.iUnion_range, isCompact_univ_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Finite.{u_1 + 1} 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace.{u} ↥(𝒰.X i)
val : Fintype 𝒰.I₀
intro : ∀ (i : 𝒰.I₀), IsCompact (X := ↥X) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))
⊢ IsCompact.{u} (X := ↥X) (⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))

Tactic:
apply isCompact_iUnion

Premises used: isCompact_iUnion
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
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₀
intro : CompactSpace.{u} (↑(Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u)
⊢ IsCompact (X := ↥X) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))

Tactic:
rw [isCompact_iff_compactSpace]

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
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₀
⊢ CompactSpace.{u} (↑(Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u)

Tactic:
@Homeomorph.compactSpace _ _ _ _ (H i)
      (TopCat.homeoOfIso
        (asIso
          (IsOpenImmersion.isoOfRangeEq (𝒰.f i)
            (X.ofRestrict (Opens.isOpenEmbedding ⟨_, (𝒰.map_prop i).base_open.isOpen_range⟩))
            Subtype.range_coe.symm).hom.base))

Premises used: CategoryTheory.PreZeroHypercover.f, TopologicalSpace.Opens.isOpenEmbedding, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.range_coe, Topology.IsOpenEmbedding.isOpen_range, TopCat.homeoOfIso, AlgebraicGeometry.Scheme.ofRestrict, Homeomorph.compactSpace, TopologicalSpace.Opens.mk, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open, Eq.symm, CategoryTheory.Iso.hom, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
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₀
⊢ CompactSpace.{u} (↑(Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u)

Tactic:
exact
    @Homeomorph.compactSpace _ _ _ _ (H i)
      (TopCat.homeoOfIso
        (asIso
          (IsOpenImmersion.isoOfRangeEq (𝒰.f i)
            (X.ofRestrict (Opens.isOpenEmbedding ⟨_, (𝒰.map_prop i).base_open.isOpen_range⟩))
            Subtype.range_coe.symm).hom.base))

Premises used: CategoryTheory.PreZeroHypercover.f, TopologicalSpace.Opens.isOpenEmbedding, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.range_coe, Topology.IsOpenEmbedding.isOpen_range, TopCat.homeoOfIso, AlgebraicGeometry.Scheme.ofRestrict, Homeomorph.compactSpace, TopologicalSpace.Opens.mk, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open, Eq.symm, CategoryTheory.Iso.hom, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.asIso
-- 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
𝒰 : AffineOpenCover.{u_1, u} X
j : 𝒰.I₀ (P := IsOpenImmersion)
⊢ IsOpenImmersion (𝒰.f (P := IsOpenImmersion) j)

Tactic:
𝒰.map_prop j

Premises used: AlgebraicGeometry.Scheme.AffineCover.map_prop
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
⊢ X.affineOpenCover.openCover = X.affineCover

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.AffineOpenCover.openCover, Classical.choose, AlgebraicGeometry.Scheme.affineCover, rfl, AlgebraicGeometry.Scheme.AffineCover.cover
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f_1) g
f : X ⟶ Y
𝒰 : OpenCover.{u_1, u} Y
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
⊢ PreZeroHypercover.f
        ((fun (i : 𝒰.I₀) ↦
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
              PreZeroHypercover (𝒰.X i)))
          (i.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))))
        (i.snd (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))) ≫
      𝟙
        (𝒰.X
          (i.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i)))) =
    𝟙 (𝒰.affineRefinement.openCover.X i) ≫
      PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (𝒰.X
              (i.fst (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                  ((fun (i : 𝒰.I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                        PreZeroHypercover (𝒰.X i)))
                    i)))).affineCover)
        (i.snd (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                  PreZeroHypercover (𝒰.X i)))
              i)))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
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)
by_contra! : ∀ (h : ∀ (i : ι), s i ∈ x.asIdeal), False
⊢ ∃ (i : ι), s i ∉ x.asIdeal

Tactic:
by_contra! h
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
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
apply : x.asIdeal = ⊤
⊢ False

Tactic:
apply x.2.ne_top

Premises used: PrimeSpectrum.isPrime, Ideal.IsPrime.ne_top
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
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))
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (y : ι), s y ∈ (↑x.asIdeal : Set (↑R : Type u_2))
⊢ x.asIdeal = ⊤

Tactic:
rwa [← top_le_iff, ← hs, Ideal.span_le, Set.range_subset_iff]

Premises used: Ideal.span_le, top_le_iff, Set.range_subset_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
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 : (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]
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
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)
this : ∃ (i : ι), s i ∉ x.asIdeal
⊢ ι

Tactic:
exact this.choose

Premises used: Exists.choose
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
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)
generalize_proofs :
  ∀ (H : ∃ (i : ι), s i ∉ x.asIdeal),
    Membership.mem (γ := Set ↥(Spec R))
      (Set.range (ι :=
        ↥(Spec
            (CommRingCat.of
              (Localization.Away
                (s
                  (have this := H;
                  this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal)))))))
        ⇑(Spec.map
            (CommRingCat.ofHom
              (algebraMap (↑R : Type u_2)
                (Localization.Away
                  (s
                    (have this := H;
                    this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal))))))))
      x
⊢ Membership.mem (γ := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(Spec
          (CommRingCat.of
            (Localization.Away
              (s
                (have this : ∃ (i : ι), s i ∉ x.asIdeal := ⋯;
                this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal)))))))
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R : Type u_2)
              (Localization.Away
                (s
                  (have this : ∃ (i : ι), s i ∉ x.asIdeal := ⋯;
                  this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal))))))))
    x

Tactic:
generalize_proofs H
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
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
i : ι := H.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal)
⊢ Set.range (ι := PrimeSpectrum (Localization.Away (s i)))
      (PrimeSpectrum.comap (algebraMap (↑R : Type u_2) (Localization.Away (s i)))) =
    (↑(PrimeSpectrum.basicOpen (s i)) : Set (PrimeSpectrum (↑R : Type u_2)))

Tactic:
have := PrimeSpectrum.localization_away_comap_range (Localization.Away (s i)) (s i)
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
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
i : ι := H.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal)
this :
  Set.range (ι := PrimeSpectrum (Localization.Away (s i)))
      (PrimeSpectrum.comap (algebraMap (↑R : Type u_2) (Localization.Away (s i)))) =
    (↑(PrimeSpectrum.basicOpen (s i)) : Set (PrimeSpectrum (↑R : Type u_2)))
⊢ Membership.mem (γ := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(Spec
          (CommRingCat.of
            (Localization.Away
              (s
                (have this := H;
                this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal)))))))
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R : Type u_2)
              (Localization.Away
                (s
                  (have this := H;
                  this.choose (p := fun (i : ι) ↦ s i ∉ x.asIdeal))))))))
    x

Tactic:
(eq_iff_iff.mp congr(x ∈ $this)).mpr H.choose_spec

Premises used: Iff.mpr, Exists.choose_spec, congrArg, Set.Mem, OreLocalization, Membership.mem, id, Quotient, Iff.mp, PrimeSpectrum.comap, eq_iff_iff