awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
t : Finset (↑Γ(X, (↑V : X.Opens)) : Type u_1)
ht₁ : (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ⊆ Set.range f
ht₂ : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1))) ⊤
i : (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hi : i ∈ t
⊢ P
    (X.affineBasicOpen
      (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ↦ x ∈ t) i hi) :
        (↑Γ(X, (↑V : X.Opens)) : Type u_1)))
have obtain : ∀ (x : ↥(↑V : X.Opens)) (hi : f x ∈ t),
  P
    (X.affineBasicOpen
      (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ↦ x ∈ t) (f x) hi) :
        (↑Γ(X, (↑V : X.Opens)) : Type u_1)))
Tactic: obtain ⟨x, rfl⟩ := ht₁ hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
⊢ P V
have suffices : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
Tactic: suffices Ideal.span (Set.range f) = ⊤ by
    obtain ⟨t, ht₁, ht₂⟩ := (Ideal.span_eq_top_iff_finite _).mp this
    apply openCover V t ht₂
    rintro ⟨i, hi⟩
    obtain ⟨x, rfl⟩ := ht₁ hi
    exact hf₂ x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
⊢ Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
have rw : (↑V : X.Opens) ≤ ⨆ (f_1 : (↑(Set.range f) : Type u_1)), X.basicOpen (↑f_1 : (↑Γ(X, (↑V : X.Opens)) : Type u_1))
Tactic: rw [← V.prop.self_le_iSup_basicOpen_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
x : ↥X
hx : x ∈ (↑V : X.Opens)
⊢ Membership.mem (γ := Opens ↥X)
    (⨆ (f_1 : (↑(Set.range f) : Type u_1)), X.basicOpen (↑f_1 : (↑Γ(X, (↑V : X.Opens)) : Type u_1))) x
have rw : ∃ (i : ↥(↑V : X.Opens)), x ∈ X.basicOpen (f i)
Tactic: rw [iSup_range', Opens.mem_iSup]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
⊢ P V
have have : ∀ (x : ↥(↑V : X.Opens)), ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
Tactic: classical
  have : ∀ (x : V.1), ∃ f : Γ(X, V), ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f) := by
    intro x
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (iSup_U.ge (Set.mem_univ x))
    obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩
    refine ⟨f, hf, ?_⟩
    convert! basicOpen _ g (hU i) using 1
    ext1
    exact e
  choose f hf₁ hf₂ using this
  suffices Ideal.span (Set.range f) = ⊤ by
    obtain ⟨t, ht₁, ht₂⟩ := (Ideal.span_eq_top_iff_finite _).mp this
    apply openCover V t ht₂
    rintro ⟨i, hi⟩
    obtain ⟨x, rfl⟩ := ht₁ hi
    exact hf₂ x
  rw [← V.prop.self_le_iSup_basicOpen_iff]
  intro x hx
  rw [iSup_range', Opens.mem_iSup]
  exact ⟨_, hf₁ ⟨x, hx⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
have :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
⊢ P V
have have₁ : ∀
  (this :
    ∀ (x : ↥(↑V : X.Opens)),
      ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)),
  P V
Tactic: classical
  have : ∀ (x : V.1), ∃ f : Γ(X, V), ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f) := by
    intro x
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (iSup_U.ge (Set.mem_univ x))
    obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩
    refine ⟨f, hf, ?_⟩
    convert! basicOpen _ g (hU i) using 1
    ext1
    exact e
  choose f hf₁ hf₂ using this
  suffices Ideal.span (Set.range f) = ⊤ by
    obtain ⟨t, ht₁, ht₂⟩ := (Ideal.span_eq_top_iff_finite _).mp this
    apply openCover V t ht₂
    rintro ⟨i, hi⟩
    obtain ⟨x, rfl⟩ := ht₁ hi
    exact hf₂ x
  rw [← V.prop.self_le_iSup_basicOpen_iff]
  intro x hx
  rw [iSup_range', Opens.mem_iSup]
  exact ⟨_, hf₁ ⟨x, hx⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
have :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
have₁ :
  ∀
    (this :
      ∀ (x : ↥(↑V : X.Opens)),
        ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)),
    P V
have₂ :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
have₃ have₄ :
  ∀
    (this :
      ∀ (x : ↥(↑V : X.Opens)),
        ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)),
    P V
⊢ P V
have have₅ : ∀ (f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1))
  (hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x))
  (hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))), P V
Tactic: classical
  have : ∀ (x : V.1), ∃ f : Γ(X, V), ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f) := by
    intro x
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (iSup_U.ge (Set.mem_univ x))
    obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩
    refine ⟨f, hf, ?_⟩
    convert! basicOpen _ g (hU i) using 1
    ext1
    exact e
  choose f hf₁ hf₂ using this
  suffices Ideal.span (Set.range f) = ⊤ by
    obtain ⟨t, ht₁, ht₂⟩ := (Ideal.span_eq_top_iff_finite _).mp this
    apply openCover V t ht₂
    rintro ⟨i, hi⟩
    obtain ⟨x, rfl⟩ := ht₁ hi
    exact hf₂ x
  rw [← V.prop.self_le_iSup_basicOpen_iff]
  intro x hx
  rw [iSup_range', Opens.mem_iSup]
  exact ⟨_, hf₁ ⟨x, hx⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
have :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
have₁ :
  ∀
    (this :
      ∀ (x : ↥(↑V : X.Opens)),
        ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)),
    P V
have₂ :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
have₃ have₄ :
  ∀
    (this :
      ∀ (x : ↥(↑V : X.Opens)),
        ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)),
    P V
have₅ :
  ∀ (f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1))
    (hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x))
    (hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))), P V
⊢ P V
have have₆ : ∀ (f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1))
  (hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x))
  (hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))),
  Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
Tactic: classical
  have : ∀ (x : V.1), ∃ f : Γ(X, V), ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f) := by
    intro x
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (iSup_U.ge (Set.mem_univ x))
    obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩
    refine ⟨f, hf, ?_⟩
    convert! basicOpen _ g (hU i) using 1
    ext1
    exact e
  choose f hf₁ hf₂ using this
  suffices Ideal.span (Set.range f) = ⊤ by
    obtain ⟨t, ht₁, ht₂⟩ := (Ideal.span_eq_top_iff_finite _).mp this
    apply openCover V t ht₂
    rintro ⟨i, hi⟩
    obtain ⟨x, rfl⟩ := ht₁ hi
    exact hf₂ x
  rw [← V.prop.self_le_iSup_basicOpen_iff]
  intro x hx
  rw [iSup_range', Opens.mem_iSup]
  exact ⟨_, hf₁ ⟨x, hx⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
have :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
have₁ :
  ∀
    (this :
      ∀ (x : ↥(↑V : X.Opens)),
        ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)),
    P V
have₂ :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
have₃ have₄ :
  ∀
    (this :
      ∀ (x : ↥(↑V : X.Opens)),
        ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)),
    P V
have₅ :
  ∀ (f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1))
    (hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x))
    (hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))), P V
have₆ :
  ∀ (f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1))
    (hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x))
    (hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))),
    Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
⊢ P V
have have₇ : ∀ (f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1))
  (hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x))
  (hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))),
  (↑V : X.Opens) ≤ ⨆ (f_1 : (↑(Set.range f) : Type u_1)), X.basicOpen (↑f_1 : (↑Γ(X, (↑V : X.Opens)) : Type u_1))
Tactic: classical
  have : ∀ (x : V.1), ∃ f : Γ(X, V), ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f) := by
    intro x
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (iSup_U.ge (Set.mem_univ x))
    obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩
    refine ⟨f, hf, ?_⟩
    convert! basicOpen _ g (hU i) using 1
    ext1
    exact e
  choose f hf₁ hf₂ using this
  suffices Ideal.span (Set.range f) = ⊤ by
    obtain ⟨t, ht₁, ht₂⟩ := (Ideal.span_eq_top_iff_finite _).mp this
    apply openCover V t ht₂
    rintro ⟨i, hi⟩
    obtain ⟨x, rfl⟩ := ht₁ hi
    exact hf₂ x
  rw [← V.prop.self_le_iSup_basicOpen_iff]
  intro x hx
  rw [iSup_range', Opens.mem_iSup]
  exact ⟨_, hf₁ ⟨x, hx⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
⊢ f = g
have this : Mono φ
Tactic: have : Mono φ := ConcreteCategory.mono_of_injective _ hφ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ f = g
have rw : IsOpenImmersion.lift U.ι f sorry ≫ U.ι = IsOpenImmersion.lift U.ι g sorry ≫ U.ι
Tactic: rw [← IsOpenImmersion.lift_fac U.ι f (by simpa [Set.range_subset_iff] using fun x hx ↦ hUf.ge hx),
    ← IsOpenImmersion.lift_fac U.ι g (by simpa [Set.range_subset_iff] using fun x hx ↦ hUg.ge hx)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ IsOpenImmersion.lift U.ι f ⋯ ≫ U.ι = IsOpenImmersion.lift U.ι g ⋯ ≫ U.ι
have e_a : IsOpenImmersion.lift U.ι f sorry = IsOpenImmersion.lift U.ι g sorry
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ IsOpenImmersion.lift U.ι f ⋯ = IsOpenImmersion.lift U.ι g ⋯
have e_a : Eq (α := Spec S ⟶ Spec Γ(X, U))
  (Spec.map
    ((Spec.homEquiv : (a : Spec R ⟶ Spec Γ(X, U)) → Γ(X, U) ⟶ R) (IsOpenImmersion.lift U.ι f sorry ≫ hU.isoSpec.hom) ≫ φ))
  (Spec.map
    ((Spec.homEquiv : (a : Spec R ⟶ Spec Γ(X, U)) → Γ(X, U) ⟶ R) (IsOpenImmersion.lift U.ι g sorry ≫ hU.isoSpec.hom) ≫ φ))
Tactic: rw [← cancel_mono hU.isoSpec.hom, ← Spec.homEquiv.injective.eq_iff,
    ← cancel_mono φ, ← Spec.map_injective.eq_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
s : Set (↑Γ(X, ⊤) : Type u)
⊢ Eq (α := Set ↥(Spec Γ(X, ⊤))) (⇑X.isoSpec.hom '' X.zeroLocus s) (PrimeSpectrum.zeroLocus s)
have rw : Eq (α := Set ↥(Spec Γ(X, ⊤)))
  (Set.image (α := ↥X) (⇑X.isoSpec.hom) (Set.preimage (β := ↥(Spec Γ(X, ⊤))) (⇑X.toSpecΓ) (PrimeSpectrum.zeroLocus s)))
  (PrimeSpectrum.zeroLocus s)
Tactic: rw [← X.toSpecΓ_preimage_zeroLocus]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
s : Set (↑Γ(X, ⊤) : Type u)
⊢ Eq (α := Set ↥(Spec Γ(X, ⊤))) (⇑X.isoSpec.inv ⁻¹' X.zeroLocus s) (PrimeSpectrum.zeroLocus s)
have rw : Eq (α := Set ↥(Spec Γ(X, ⊤))) (Set.preimage (β := ↥(Spec Γ(X, ⊤))) (⇑(𝟙 (Spec Γ(X, ⊤)))) (PrimeSpectrum.zeroLocus s))
  (PrimeSpectrum.zeroLocus s)
Tactic: rw [← toSpecΓ_preimage_zeroLocus, ← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base,
    X.isoSpec_inv_toSpecΓ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
s : Set (↑Γ(X, ⊤) : Type u)
⊢ Set.image (α := ↥(Spec Γ(X, ⊤))) (⇑X.isoSpec.inv) (PrimeSpectrum.zeroLocus s) = X.zeroLocus s
have h : Function.Surjective (α := ↥(Spec Γ(X, ⊤))) (β := ↥X) ⇑X.isoSpec.inv
Tactic: rw [← isoSpec_inv_preimage_zeroLocus, Set.image_preimage_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
⊢ IsClosed s ↔ ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
have refine_1 : ∀ (hs : IsClosed s), ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
Tactic: refine ⟨fun hs ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
refine_1 : ∀ (hs : IsClosed s), ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
⊢ IsClosed s ↔ ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
have refine_2 : (∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))) → IsClosed s
Tactic: refine ⟨fun hs ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
⊢ ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
have hZ : IsClosed Z
Tactic: have hZ : IsClosed Z := (X.isoSpec.hom.homeomorph).isClosedMap _ hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
hZ : IsClosed Z
⊢ ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
have refine_1 : ∀ (I : Ideal (↑Γ(X, ⊤) : Type u)) (hI : Z = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))),
  ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
Tactic: obtain ⟨I, (hI : Z = _)⟩ := (PrimeSpectrum.isClosed_iff_zeroLocus_ideal _).mp hZ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal (↑Γ(X, ⊤) : Type u)
hI : Z = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
⊢ ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
have h : s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
Tactic: use I
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal (↑Γ(X, ⊤) : Type u)
hI : Z = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
⊢ s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
have h : s = ⇑X.toSpecΓ ⁻¹' X.toΓSpecFun '' s
Tactic: simp only [← Scheme.toSpecΓ_preimage_zeroLocus, ← hI, Z]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal (↑Γ(X, ⊤) : Type u)
hI : Z = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
⊢ s = ⇑X.toSpecΓ ⁻¹' X.toΓSpecFun '' s
have h : ⇑X.toSpecΓ ⁻¹' X.toΓSpecFun '' s = s
Tactic: symm