awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
⊢ ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
have obtain : ∀ (f : (↑Γ(X, U) : Type u)) (hf₁ : X.basicOpen f ≤ V)
  (hf₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x sorry) : ↥X) ∈ X.basicOpen f),
  ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
Tactic: obtain ⟨f, hf₁, hf₂⟩ := hU.exists_basicOpen_le ⟨x, hx.2⟩ hx.1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
f : (↑Γ(X, U) : Type u)
hf₁ : X.basicOpen f ≤ V
hf₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯) : ↥X) ∈ X.basicOpen f
⊢ ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
have obtain : ∀ (g : (↑Γ(X, V) : Type u)) (hg₁ : X.basicOpen g ≤ X.basicOpen f)
  (hg₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ X.basicOpen f) x hf₂) : ↥X) ∈ X.basicOpen g),
  ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
Tactic: obtain ⟨g, hg₁, hg₂⟩ := hV.exists_basicOpen_le ⟨x, hf₂⟩ hx.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
f : (↑Γ(X, U) : Type u)
hf₁ : X.basicOpen f ≤ V
hf₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯) : ↥X) ∈ X.basicOpen f
g : (↑Γ(X, V) : Type u)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ X.basicOpen f) x hf₂) : ↥X) ∈ X.basicOpen g
⊢ ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
have obtain : ∀ (f' : (↑Γ(X, U) : Type u))
  (hf' :
    X.basicOpen f' =
      X.basicOpen (U := X.basicOpen f)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.presheaf.map (homOfLE hf₁).op) :
            (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
          g)),
  ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
Tactic: obtain ⟨f', hf'⟩ :=
    basicOpen_basicOpen_is_basicOpen hU f (X.presheaf.map (homOfLE hf₁ : _ ⟶ V).op g)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
f : (↑Γ(X, U) : Type u)
hf₁ : X.basicOpen f ≤ V
hf₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯) : ↥X) ∈ X.basicOpen f
g : (↑Γ(X, V) : Type u)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ X.basicOpen f) x hf₂) : ↥X) ∈ X.basicOpen g
f' : (↑Γ(X, U) : Type u)
hf' :
  X.basicOpen f' =
    X.basicOpen (U := X.basicOpen f)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE hf₁).op) :
          (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
        g)
⊢ ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
have hf'₁ : X.basicOpen f' = X.toRingedSpace.basicOpen g
Tactic: replace hf' := (hf'.trans (RingedSpace.basicOpen_res _ _ _)).trans (inf_eq_right.mpr hg₁)
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (hU.isoSpec.inv ≫ U.ι) (hU.isoSpec.hom x : ↥(Spec Γ(X, U))) = (↑x : ↥X)
have rw : U.ι x = (↑x : ↥X)
Tactic: rw [← Scheme.Hom.comp_apply, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
⊢ (Spec.map (Scheme.Hom.appLE f U V hVU)) (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)) =
    hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)
have simp : Eq (α := ↥(Spec Γ(Y, U)))
  ((Scheme.Hom.resLE f U V hVU ≫ U.toSpecΓ) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥(Spec Γ(Y, U)))
  (U.toSpecΓ (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) sorry) : ↥(Spec Γ(Y, U)))
Tactic: simp only [IsAffineOpen.primeIdealOf, ← Scheme.Hom.comp_apply, IsAffineOpen.isoSpec_hom,
    Scheme.Opens.toSpecΓ_SpecMap_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
⊢ Eq (α := ↥(Spec Γ(Y, U)))
    (U.toSpecΓ ((Scheme.Hom.resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)) : ↥(Spec Γ(Y, U)))
    (U.toSpecΓ (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥(Spec Γ(Y, U)))
have h : Eq (α := ↥(↑U : Scheme)) ((Scheme.Hom.resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥(↑U : Scheme))
  (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) sorry : ↥U)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
⊢ Eq (α := ↥(↑U : Scheme)) ((Scheme.Hom.resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥(↑U : Scheme))
    (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯ : ↥U)
have h : Eq (α := ↥Y) ((↑((Scheme.Hom.resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)) : ↥Y) : ↥Y)
  ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) sorry) : ↥Y) : ↥Y)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
⊢ (hU.primeIdealOf x).asIdeal.IsMaximal
have hx₀ : IsClosed (X := ↥U) {x}
Tactic: have hx₀ : IsClosed {x} := by
    simpa [← Set.image_singleton, Set.preimage_image_eq _ Subtype.val_injective]
      using hx.preimage U.isOpenEmbedding'.continuous
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
hx₀ : IsClosed (X := ↥U) {x}
⊢ (hU.primeIdealOf x).asIdeal.IsMaximal
have apply : IsClosed (X := PrimeSpectrum (↑Γ(X, U) : Type u)) {hU.primeIdealOf x}
Tactic: apply (hU.primeIdealOf x).isClosed_singleton_iff_isMaximal.mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
hx₀ : IsClosed (X := ↥U) {x}
⊢ IsClosed (X := PrimeSpectrum (↑Γ(X, U) : Type u)) {hU.primeIdealOf x}
have rw : IsClosed (X := PrimeSpectrum (↑Γ(X, U) : Type u)) (Set.image (α := ↥U) ⇑hU.isoSpec.hom {x})
Tactic: rw [primeIdealOf, ← Set.image_singleton]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
hx₀ : IsClosed (X := ↥U) {x}
⊢ IsClosed (X := PrimeSpectrum (↑Γ(X, U) : Type u)) (Set.image (α := ↥U) ⇑hU.isoSpec.hom {x})
have refine : IsHomeomorph (X := ↥U) (Y := PrimeSpectrum (↑Γ(X, U) : Type u)) ⇑hU.isoSpec.hom
Tactic: refine (Topology.IsClosedEmbedding.isClosed_iff_image_isClosed <|
    IsHomeomorph.isClosedEmbedding ?_).mp hx₀
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
hx₀ : IsClosed (X := ↥U) {x}
⊢ IsHomeomorph (X := ↥U) (Y := PrimeSpectrum (↑Γ(X, U) : Type u)) ⇑hU.isoSpec.hom
have apply : IsIso hU.isoSpec.hom.base
Tactic: apply (TopCat.isIso_iff_isHomeomorph _).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hy : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X)
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec y)) : Type u) y.asIdeal
have _ : IsLocalization y.asIdeal.primeCompl (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u)
Tactic: apply
    (@IsLocalization.isLocalization_iff_of_ringEquiv (R := Γ(X, U))
      (S := X.presheaf.stalk (hU.fromSpec y)) _ y.asIdeal.primeCompl _
      (TopCat.Presheaf.algebra_section_stalk X.presheaf ⟨hU.fromSpec y, hy⟩) _ _
      (asIso <| hU.fromSpec.stalkMap y).commRingCatIsoToRingEquiv).mpr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hy : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X)
⊢ IsLocalization y.asIdeal.primeCompl (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u)
have a : IsLocalization y.asIdeal.primeCompl (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u) ↔
  IsLocalization.AtPrime
    (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u) y.asIdeal
Tactic: convert! StructureSheaf.IsLocalization.to_stalk Γ(X, U) y using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hy : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X)
⊢ IsLocalization y.asIdeal.primeCompl (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u) ↔
    IsLocalization y.asIdeal.primeCompl
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u)
have a : (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u) =
    (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u) →
  HEq.{u + 1} (α := CommSemiring (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u)) CommRing.toCommSemiring (β :=
      CommSemiring (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u))
      CommRing.toCommSemiring →
    RingHom.toAlgebra
        ((asIso (Scheme.Hom.stalkMap hU.fromSpec y)).commRingCatIsoToRingEquiv.toRingHom.comp
          (algebraMap (↑Γ(X, U) : Type u) (↑(X.presheaf.stalk (hU.fromSpec y)) : Type u))) =
      (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑Γ(X, U) : Type u) y)).toAlgebra
Tactic: congr!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hy : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X)
e_4 :
  (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u) =
    (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u)
e_5 :
  HEq.{u + 1} (α := CommSemiring (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u)) CommRing.toCommSemiring (β :=
    CommSemiring (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u))
    CommRing.toCommSemiring
⊢ RingHom.toAlgebra
      ((asIso (Scheme.Hom.stalkMap hU.fromSpec y)).commRingCatIsoToRingEquiv.toRingHom.comp
        (algebraMap (↑Γ(X, U) : Type u) (↑(X.presheaf.stalk (hU.fromSpec y)) : Type u))) =
    (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑Γ(X, U) : Type u) y)).toAlgebra
have a : RingHom.toAlgebra (CommRingCat.Hom.hom (Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.germ ⊤ y sorry)) =
  (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑Γ(X, U) : Type u) y)).toAlgebra
Tactic: simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, IsAffineOpen.fromSpec_app_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (↑x : ↥X)) : Type u) (hU.primeIdealOf x).asIdeal
have rcases : ∀ (x : ↥X) (hx : x ∈ U),
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)).asIdeal
Tactic: rcases x with ⟨x, hx⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)).asIdeal
have set : let y := hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx);
∀ (hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)),
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u) y.asIdeal
Tactic: set y := hU.primeIdealOf ⟨x, hx⟩ with hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
y : PrimeSpectrum (↑Γ(X, U) : Type u) := hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)
hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u) y.asIdeal
have this : hU.fromSpec y = x
Tactic: have : hU.fromSpec y = x := hy ▸ hU.fromSpec_primeIdealOf ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
y : PrimeSpectrum (↑Γ(X, U) : Type u) := hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)
hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)
this : hU.fromSpec y = x
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u) y.asIdeal
have clear_value : ∀ (y : PrimeSpectrum (↑Γ(X, U) : Type u)) (hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx))
  (this : hU.fromSpec y = x),
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u) y.asIdeal
Tactic: clear_value y
Cleared hypotheses: y, hy, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)
this : hU.fromSpec y = x
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u) y.asIdeal
have subst : ∀ (hx : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X))
  (hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (hU.fromSpec y) hx)),
  IsLocalization.AtPrime
    (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (hU.fromSpec y) hx) : ↥X)) : Type u) y.asIdeal
Tactic: subst this
Cleared hypotheses: x, hx, hy, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : (↑Γ(X, U) : Type u)
I : Ideal (↑Γ(X, U) : Type u)
⊢ s ∈ I ↔
    ∀ (x : ↥X) (h : x ∈ U),
      Membership.mem (α := (↑(X.presheaf.stalk x) : Type u)) (γ := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x h) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            s :
          (↑(X.presheaf.stalk x) : Type u))
have refine : ∀
  (H :
    ∀ (x : ↥X) (h : x ∈ U),
      Membership.mem (α := (↑(X.presheaf.stalk x) : Type u)) (γ := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x h) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            s :
          (↑(X.presheaf.stalk x) : Type u))),
  s ∈ I
Tactic: refine ⟨fun hs x hxU ↦ Ideal.mem_map_of_mem _ hs, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : (↑Γ(X, U) : Type u)
I : Ideal (↑Γ(X, U) : Type u)
H :
  ∀ (x : ↥X) (h : x ∈ U),
    Membership.mem (α := (↑(X.presheaf.stalk x) : Type u)) (γ := Ideal (↑(X.presheaf.stalk x) : Type u))
      (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x h) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          s :
        (↑(X.presheaf.stalk x) : Type u))
this : (x : ↥(Spec Γ(X, U))) → Algebra (↑Γ(X, U) : Type u) (↑(X.presheaf.stalk (hU.fromSpec x)) : Type u) :=
  fun (x : ↥(Spec Γ(X, U))) ↦
    X.presheaf.algebra_section_stalk
      (((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' : (a : ↥(Spec Γ(X, U))) → ↥(↑U : Scheme)) x)
⊢ s ∈ I
have this₁ : ∀ (P : Ideal (↑Γ(X, U) : Type u)) [hP : P.IsPrime],
  IsLocalization.AtPrime
    (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := hP : PrimeSpectrum (↑Γ(X, U) : Type u) })) : Type u) P
Tactic: have (P : Ideal Γ(X, U)) [hP : P.IsPrime] : IsLocalization.AtPrime _ P :=
      hU.isLocalization_stalk' ⟨P, hP⟩ (hU.isoSpec.inv _).2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
I J : Ideal (↑Γ(X, U) : Type u)
⊢ I = J ↔
    ∀ (x : ↥X) (h : x ∈ U),
      Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)
have simp_rw : I ≤ J ∧ J ≤ I ↔
  ∀ (x : ↥X) (h : x ∈ U),
    LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J) ∧
      LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
Tactic: simp_rw [le_antisymm_iff, hU.ideal_le_iff, forall_and]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
I J : Ideal (↑Γ(X, U) : Type u)
simp_rw :
  I ≤ J ∧ J ≤ I ↔
    ∀ (x : ↥X) (h : x ∈ U),
      LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J) ∧
        LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
⊢ I = J ↔
    ∀ (x : ↥X) (h : x ∈ U),
      Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)
have simp_rw₁ : ((∀ (x : ↥X) (h : x ∈ U),
      LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)) ∧
    ∀ (x : ↥X) (h : x ∈ U),
      LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)) ↔
  ∀ (x : ↥X) (h : x ∈ U),
    LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J) ∧
      LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
Tactic: simp_rw [le_antisymm_iff, hU.ideal_le_iff, forall_and]
-- 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 : 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) ⋯)
⊢ 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 (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) sorry) : ↥Y)) : Type u)
  (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) sorry)).asIdeal
Tactic: have := hU.isLocalization_stalk ⟨f x, hVU hx⟩