awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X Y : Scheme
U_1 : X.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X, U_1) : Type u)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this_1 : Algebra (↑(Y.presheaf.obj (op U)) : Type u)
  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u) :=
  Y.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)
this_2 :
  IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
this : Algebra (↑(X.presheaf.obj (op V)) : Type u)
  (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u) :=
  X.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)
⊢ Arrow.mk (Scheme.Hom.stalkMap f x) ≅
    Arrow.mk (X :=
      CommRingCat.of (Localization.AtPrime (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal))
      (Y :=
      CommRingCat.of (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal))
      (CommRingCat.ofHom
        (Localization.localRingHom (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
          (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯))
have this₁ : IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u)
  (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
Tactic: have := hV.isLocalization_stalk ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
U_1 : X.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X, U_1) : Type u)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this_1 : Algebra (↑(Y.presheaf.obj (op U)) : Type u)
  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u) :=
  Y.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)
this_2 :
  IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
this_3 : Algebra (↑(X.presheaf.obj (op V)) : Type u)
  (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u) :=
  X.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
⊢ Arrow.mk (Scheme.Hom.stalkMap f x) ≅
    Arrow.mk (X :=
      CommRingCat.of (Localization.AtPrime (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal))
      (Y :=
      CommRingCat.of (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal))
      (CommRingCat.ofHom
        (Localization.localRingHom (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
          (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯))
have refine_1 : Y.presheaf.stalk (f x) ≅
  CommRingCat.of (Localization.AtPrime (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) sorry)).asIdeal)
Tactic: refine Arrow.isoMk' _ _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
U_1 : X.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X, U_1) : Type u)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this_1 : Algebra (↑(Y.presheaf.obj (op U)) : Type u)
  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u) :=
  Y.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)
this_2 :
  IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
this_3 : Algebra (↑(X.presheaf.obj (op V)) : Type u)
  (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u) :=
  X.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
refine_1 :
  Y.presheaf.stalk (f x) ≅
    CommRingCat.of (Localization.AtPrime (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal)
⊢ Arrow.mk (Scheme.Hom.stalkMap f x) ≅
    Arrow.mk (X :=
      CommRingCat.of (Localization.AtPrime (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal))
      (Y :=
      CommRingCat.of (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal))
      (CommRingCat.ofHom
        (Localization.localRingHom (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
          (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯))
have refine_2 : X.presheaf.stalk x ≅
  CommRingCat.of (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal)
Tactic: refine Arrow.isoMk' _ _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
    Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
have trans : ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
  Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
    (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ
Tactic: trans ⋃ i : s, (PrimeSpectrum.basicOpen i.1).1 = Set.univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
trans :
  ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
    Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
    Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
have trans₁ : Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
    (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ ↔
  Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
Tactic: trans ⋃ i : s, (PrimeSpectrum.basicOpen i.1).1 = Set.univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
    Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ
have trans : ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
  Eq (α := Set ↥(Spec Γ(X, U)))
    (Set.preimage (β := ↥X) (⇑hU.fromSpec)
      (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
    (⇑hU.fromSpec ⁻¹' U.carrier)
Tactic: trans hU.fromSpec ⁻¹' (⨆ f : s, X.basicOpen (f : Γ(X, U))).1 = hU.fromSpec ⁻¹' U.1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
trans :
  ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
    Eq (α := Set ↥(Spec Γ(X, U)))
      (Set.preimage (β := ↥X) (⇑hU.fromSpec)
        (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
      (⇑hU.fromSpec ⁻¹' U.carrier)
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
    Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ
have trans₁ : Eq (α := Set ↥(Spec Γ(X, U)))
    (Set.preimage (β := ↥X) (⇑hU.fromSpec)
      (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
    (⇑hU.fromSpec ⁻¹' U.carrier) ↔
  Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
    (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ
Tactic: trans hU.fromSpec ⁻¹' (⨆ f : s, X.basicOpen (f : Γ(X, U))).1 = hU.fromSpec ⁻¹' U.1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U
⊢ Eq (α := Set ↥(Spec Γ(X, U)))
    (Set.preimage (β := ↥X) (⇑hU.fromSpec)
      (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
    (⇑hU.fromSpec ⁻¹' U.carrier)
have rw : Eq (α := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' U.carrier) (⇑hU.fromSpec ⁻¹' U.carrier)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
    Eq (α := Set ↥(Spec Γ(X, U)))
      (Set.preimage (β := ↥X) (⇑hU.fromSpec)
        (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
      (⇑hU.fromSpec ⁻¹' U.carrier)
have refine : Eq (α := Set ↥(Spec Γ(X, U)))
    (Set.preimage (β := ↥X) (⇑hU.fromSpec)
      (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
    (⇑hU.fromSpec ⁻¹' U.carrier) →
  ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U
Tactic: refine ⟨fun h => by rw [h], ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h :
  Eq (α := Set ↥(Spec Γ(X, U)))
    (Set.preimage (β := ↥X) (⇑hU.fromSpec)
      (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
    (⇑hU.fromSpec ⁻¹' U.carrier)
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U
have h₁ : Eq (α := Set ↥X)
  (Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec)
    (Set.preimage (β := ↥X) (⇑hU.fromSpec)
      (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))))))
  (Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (⇑hU.fromSpec ⁻¹' U.carrier))
Tactic: apply_fun Set.image hU.fromSpec at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h :
  Eq (α := Set ↥X)
    (Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec)
      (Set.preimage (β := ↥X) (⇑hU.fromSpec)
        (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))))))
    (Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (⇑hU.fromSpec ⁻¹' U.carrier))
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U
have h₁ : Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) ∩ (↑U : Set ↥X) =
  U.carrier ∩ (↑U : Set ↥X)
Tactic: rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.range_fromSpec]
        at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h :
  Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) ∩ (↑U : Set ↥X) =
    U.carrier ∩ (↑U : Set ↥X)
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U
have h₁ : (↑U : Set ↥X) ⊆ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X)
Tactic: simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : (↑U : Set ↥X) ⊆ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X)
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U
have h₁ : (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X) = (↑U : Set ↥X)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : (↑U : Set ↥X) ⊆ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X)
⊢ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X) = (↑U : Set ↥X)
have h₁ : (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X) ⊆ (↑U : Set ↥X)
Tactic: refine Set.Subset.antisymm ?_ h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : (↑U : Set ↥X) ⊆ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X)
⊢ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X) ⊆ (↑U : Set ↥X)
have h₁ : ∀ (x : (↑Γ(X, U) : Type u)) (h : x ∈ s), (↑(X.basicOpen x) : Set ↥X) ⊆ (↑U : Set ↥X)
Tactic: simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ Eq (α := Set ↥(Spec Γ(X, U)))
      (Set.preimage (β := ↥X) (⇑hU.fromSpec)
        (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
      (⇑hU.fromSpec ⁻¹' U.carrier) ↔
    Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ
have simp : Eq (α := Set ↥(Spec Γ(X, U)))
    (⋃ (i : (↑s : Type u)), ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
    (⇑hU.fromSpec ⁻¹' U.carrier) ↔
  Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
    (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ
Tactic: simp only [Opens.iSup_def, Set.preimage_iUnion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ Eq (α := Set ↥(Spec Γ(X, U)))
      (⋃ (i : (↑s : Type u)), ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
      (⇑hU.fromSpec ⁻¹' U.carrier) ↔
    Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ
have a : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u)) →
  Eq.{u + 1} (α := Set ↥(Spec Γ(X, U)))
    (⋃ (i : (↑s : Type u)), ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
    (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u))))
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
a :
  Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u)) →
    Eq.{u + 1} (α := Set ↥(Spec Γ(X, U)))
      (⋃ (i : (↑s : Type u)), ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u))))
⊢ Eq (α := Set ↥(Spec Γ(X, U)))
      (⋃ (i : (↑s : Type u)), ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
      (⇑hU.fromSpec ⁻¹' U.carrier) ↔
    Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ
have a₁ : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u)) →
  Eq (α := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' U.carrier) Set.univ
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
e_1 : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u))
⊢ Eq.{u + 1} (α := Set ↥(Spec Γ(X, U)))
    (⋃ (i : (↑s : Type u)), ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
    (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u))))
have a : Eq.{u + 1} (α := (↑s : Type u) → Set ↥(Spec Γ(X, U)))
  (fun (i : (↑s : Type u)) ↦ ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
  fun (i : (↑s : Type u)) ↦ Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))
Tactic: refine congr_arg (Set.iUnion ·) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
e_1 : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u))
⊢ Eq.{u + 1} (α := (↑s : Type u) → Set ↥(Spec Γ(X, U)))
    (fun (i : (↑s : Type u)) ↦ ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
    fun (i : (↑s : Type u)) ↦ Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))
have a : ∀ (x : (↑s : Type u)),
  Eq (α := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑x : (↑Γ(X, U) : Type u))) : Set ↥X))
    (Opens.carrier (PrimeSpectrum.basicOpen (↑x : (↑Γ(X, U) : Type u))))
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ ↔
    Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
have simp : Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
    (⋃ (i : (↑s : Type u)), (PrimeSpectrum.zeroLocus {(↑i : (↑Γ(X, U) : Type u))})ᶜ) Set.univ ↔
  Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
Tactic: simp only [Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), (PrimeSpectrum.zeroLocus {(↑i : (↑Γ(X, U) : Type u))})ᶜ) Set.univ ↔
    Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
have rw : Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
    (PrimeSpectrum.zeroLocus (⋃ (i : (↑s : Type u)), {(↑i : (↑Γ(X, U) : Type u))})) ∅ ↔
  Eq (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u))) (PrimeSpectrum.zeroLocus s) ∅
Tactic: rw [← Set.compl_iInter, Set.compl_univ_iff, ← PrimeSpectrum.zeroLocus_iUnion, ←
      PrimeSpectrum.zeroLocus_empty_iff_eq_top, PrimeSpectrum.zeroLocus_span]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) ↔
    Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
have rw : U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) ↔
  U = ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))
Tactic: rw [← hU.iSup_basicOpen_eq_self_iff, @comm _ Eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) ↔
    U = ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))
have refine : ∀ (h : U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))),
  ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) ≤ U
Tactic: refine ⟨fun h => le_antisymm h ?_, le_of_eq⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) ≤ U
have simp : ∀ (x : (↑Γ(X, U) : Type u)) (h : x ∈ s), X.basicOpen x ≤ U
Tactic: simp only [iSup_le_iff, SetCoe.forall]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
⊢ Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r) ≅
    Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))
have refine_1 : (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).left ≅
  (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).left
Tactic: refine Arrow.isoMk ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
refine_1 :
  (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).left ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).left
⊢ Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r) ≅
    Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))
have refine_2 : (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).right ≅
  (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).right
Tactic: refine Arrow.isoMk ?_ ?_ ?_