awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
a b : (↑(X.presheaf.obj (op U)) : Type u_1)
e : a * b = 0
h : (↑(X.basicOpen a) : Set ↥X).Nonempty ∧ (↑(X.basicOpen b) : Set ↥X).Nonempty
⊢ False
have obtain : ∀ (x : ↥X) (hxU : x ∈ U)
  (hx₁ :
    IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x hxU) :
            (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) →
              (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
          a :
        (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1)))
  (w : x ∈ U)
  (hx₂ :
    IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x w) :
            (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) →
              (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
          b :
        (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))),
  False
Tactic: obtain ⟨x, ⟨hxU, hx₁⟩, _, hx₂⟩ :=
      nonempty_preirreducible_inter (X.basicOpen a).2 (X.basicOpen b).2 h.1 h.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
a b : (↑(X.presheaf.obj (op U)) : Type u_1)
e : a * b = 0
h : (↑(X.basicOpen a) : Set ↥X).Nonempty ∧ (↑(X.basicOpen b) : Set ↥X).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x hxU) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        a :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
w : x ∈ U
hx₂ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x w) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        b :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
⊢ False
have e₁ : Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
        (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
      (a * b) :
    (↑(X.presheaf.stalk x) : Type u_1))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
        (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
      0 :
    (↑(X.presheaf.stalk x) : Type u_1))
Tactic: replace e := congr_arg (X.presheaf.germ U x hxU) e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
a b : (↑(X.presheaf.obj (op U)) : Type u_1)
h : (↑(X.basicOpen a) : Set ↥X).Nonempty ∧ (↑(X.basicOpen b) : Set ↥X).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x hxU) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        a :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
w : x ∈ U
hx₂ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x w) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        b :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
e :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        (a * b) :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ False
have e₁ : HMul.hMul (α := (↑(X.presheaf.stalk x) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        a :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        b :
      (↑(X.presheaf.stalk x) : Type u_1)) =
  0
Tactic: rw [map_mul, map_zero] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
a b : (↑(X.presheaf.obj (op U)) : Type u_1)
h : (↑(X.basicOpen a) : Set ↥X).Nonempty ∧ (↑(X.basicOpen b) : Set ↥X).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x hxU) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        a :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
w : x ∈ U
hx₂ :
  IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk x) (X.toRingedSpace.presheaf.germ U x w) :
          (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u_1)) → (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
        b :
      (↑(X.toRingedSpace.presheaf.stalk x) : Type u_1))
e :
  HMul.hMul (α := (↑(X.presheaf.stalk x) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          a :
        (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          b :
        (↑(X.presheaf.stalk x) : Type u_1)) =
    0
⊢ False
have refine : IsUnit.{u_1} (M := (↑(X.presheaf.stalk x) : Type u_1)) 0
Tactic: refine zero_ne_one' (X.presheaf.stalk x) (isUnit_zero_iff.1 ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsReduced X
H : IrreducibleSpace.{u_1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
this : ∃ (x : (↑(X.presheaf.obj (op U)) : Type u_1)) (y : (↑(X.presheaf.obj (op U)) : Type u_1)), x ≠ y
⊢ IsDomain.{u_1} (↑Γ(X, U) : Type u_1)
have this₁ : NoZeroDivisors.{u_1} (↑(X.presheaf.obj (op U)) : Type u_1)
Tactic: have : NoZeroDivisors
      (X.toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace.presheaf.obj (op U)) := by
    refine ⟨fun {a b} e => ?_⟩
    simp_rw [← basicOpen_eq_bot_iff, ← Opens.not_nonempty_iff_eq_bot]
    by_contra! h
    obtain ⟨x, ⟨hxU, hx₁⟩, _, hx₂⟩ :=
      nonempty_preirreducible_inter (X.basicOpen a).2 (X.basicOpen b).2 h.1 h.2
    replace e := congr_arg (X.presheaf.germ U x hxU) e
    rw [map_mul, map_zero] at e
    refine zero_ne_one' (X.presheaf.stalk x) (isUnit_zero_iff.1 ?_)
    convert! hx₁.mul hx₂
    exact e.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
⊢ IsIntegral X
have nonempty : autoParam (Nonempty.{u_1 + 1} ↥X) IsIntegral.nonempty._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
nonempty : autoParam (Nonempty.{u_1 + 1} ↥X) IsIntegral.nonempty._autoParam
⊢ IsIntegral X
have component_integral : autoParam (∀ (U : X.Opens) [Nonempty.{u_1 + 1} ↥(↑U : Scheme)], IsDomain.{u_1} (↑Γ(X, U) : Type u_1))
  IsIntegral.component_integral._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ IsDomain.{u_1} (↑Γ(X, U) : Type u_1)
have component_integral : IsDomain.{u_1} (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u_1)
Tactic: rw [← f.preimage_image_eq U]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ IsDomain.{u_1} (↑Γ(Y, f ''ᵁ U) : Type u_1)
have inst : Nonempty.{u_1 + 1} ↥(↑(f ''ᵁ U) : Scheme)
Tactic: apply +allowSynthFailures IsIntegral.component_integral
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsIntegral Y
inst_2 : Nonempty.{u_1 + 1} ↥X
U : X.Opens
hU : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ IsDomain.{u_1} (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u_1)
have this : IsDomain.{u_1} (↑Γ(Y, f ''ᵁ U) : Type u_1)
Tactic: have : IsDomain Γ(Y, f ''ᵁ U) := by
    apply +allowSynthFailures IsIntegral.component_integral
    exact ⟨⟨_, _, hU.some.prop, rfl⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X Y : Scheme
h : IsIntegral X
f : X ⟶ Y
inst : IsIso f
⊢ IsIntegral Y
have suffices : Nonempty.{u + 1} ↥Y
Tactic: suffices Nonempty Y from isIntegral_of_isOpenImmersion (inv f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ Function.Injective (α := (↑Γ(X, V) : Type u_1)) (β := (↑Γ(X, U) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X.presheaf.map i.op)) :
      (a : (↑Γ(X, V) : Type u_1)) → (↑Γ(X, U) : Type u_1))
have rw : ∀ (a : (↑Γ(X, V) : Type u_1)),
  Eq (α := (↑Γ(X, U) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map i.op) :
            (a : (↑Γ(X, V) : Type u_1)) → (↑Γ(X, U) : Type u_1))
          a :
        (↑Γ(X, U) : Type u_1))
      (0 : (↑Γ(X, U) : Type u_1)) →
    a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
hx :
  Eq (α := (↑Γ(X, U) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i.op) :
          (a : (↑Γ(X, V) : Type u_1)) → (↑Γ(X, U) : Type u_1))
        x :
      (↑Γ(X, U) : Type u_1))
    (0 : (↑Γ(X, U) : Type u_1))
⊢ x = 0
have rw : ∀
  (hx :
    X.basicOpen (U := U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map i.op) :
            (a : (↑Γ(X, V) : Type u_1)) → (↑Γ(X, U) : Type u_1))
          x) =
      ⊥),
  X.basicOpen x = ⊥
Tactic: rw [← basicOpen_eq_bot_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
hx :
  X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map i.op) :
          (a : (↑Γ(X, V) : Type u_1)) → (↑Γ(X, U) : Type u_1))
        x) =
    ⊥
⊢ X.basicOpen x = ⊥
have hx₁ : U ⊓ X.basicOpen x = ⊥
Tactic: rw [Scheme.basicOpen_res] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
hx : U ⊓ X.basicOpen x = ⊥
⊢ X.basicOpen x = ⊥
have revert : ∀ (hx : U ⊓ X.basicOpen x = ⊥), X.basicOpen x = ⊥
Tactic: revert hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
⊢ ∀ (hx : U ⊓ X.basicOpen x = ⊥), X.basicOpen x = ⊥
have contrapose! : X.basicOpen x ≠ ⊥ → U ⊓ X.basicOpen x ≠ ⊥
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
⊢ X.basicOpen x ≠ ⊥ → U ⊓ X.basicOpen x ≠ ⊥
have simp_rw : (↑(X.basicOpen x) : Set ↥X).Nonempty → (↑(U ⊓ X.basicOpen x) : Set ↥X).Nonempty
Tactic: simp_rw [Ne, ← Opens.not_nonempty_iff_eq_bot, Classical.not_not]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
x : (↑Γ(X, V) : Type u_1)
⊢ (↑(X.basicOpen x) : Set ↥X).Nonempty → (↑(U ⊓ X.basicOpen x) : Set ↥X).Nonempty
have apply : (↑U : Set ↥X).Nonempty
Tactic: apply nonempty_preirreducible_inter U.isOpen (RingedSpace.basicOpen _ _).isOpen
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
⊢ x.asIdeal.height = coheight x
have rw : height x = coheight x
Tactic: rw [PrimeSpectrum.height_eq_orderHeight,
    ← Order.coheight_orderIso (specOrderIsoPrimeSpectrum R), ← height_ofDual,
    specOrderIsoPrimeSpectrum_apply, OrderDual.ofDual_toDual]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
rw : height x = coheight x
⊢ x.asIdeal.height = coheight x
have rw₁ : height x =
  coheight (α := (PrimeSpectrum (↑R : Type u_1))ᵒᵈ)
    ((specOrderIsoPrimeSpectrum R : (a : ↥(Spec R)) → (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) x :
      (PrimeSpectrum (↑R : Type u_1))ᵒᵈ)
Tactic: rw [PrimeSpectrum.height_eq_orderHeight,
    ← Order.coheight_orderIso (specOrderIsoPrimeSpectrum R), ← height_ofDual,
    specOrderIsoPrimeSpectrum_apply, OrderDual.ofDual_toDual]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
rw : height x = coheight x
rw₁ :
  height x =
    coheight (α := (PrimeSpectrum (↑R : Type u_1))ᵒᵈ)
      ((specOrderIsoPrimeSpectrum R : (a : ↥(Spec R)) → (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) x :
        (PrimeSpectrum (↑R : Type u_1))ᵒᵈ)
⊢ x.asIdeal.height = coheight x
have rw₂ : height x =
  height (α := PrimeSpectrum (↑R : Type u_1))
    ((OrderDual.ofDual : (a : (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) → PrimeSpectrum (↑R : Type u_1))
        ((specOrderIsoPrimeSpectrum R : (a : ↥(Spec R)) → (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) x) :
      PrimeSpectrum (↑R : Type u_1))
Tactic: rw [PrimeSpectrum.height_eq_orderHeight,
    ← Order.coheight_orderIso (specOrderIsoPrimeSpectrum R), ← height_ofDual,
    specOrderIsoPrimeSpectrum_apply, OrderDual.ofDual_toDual]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
rw : height x = coheight x
rw₁ :
  height x =
    coheight (α := (PrimeSpectrum (↑R : Type u_1))ᵒᵈ)
      ((specOrderIsoPrimeSpectrum R : (a : ↥(Spec R)) → (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) x :
        (PrimeSpectrum (↑R : Type u_1))ᵒᵈ)
rw₂ :
  height x =
    height (α := PrimeSpectrum (↑R : Type u_1))
      ((OrderDual.ofDual : (a : (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) → PrimeSpectrum (↑R : Type u_1))
          ((specOrderIsoPrimeSpectrum R : (a : ↥(Spec R)) → (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) x) :
        PrimeSpectrum (↑R : Type u_1))
⊢ x.asIdeal.height = coheight x
have rw₃ : height x =
  height (α := PrimeSpectrum (↑R : Type u_1))
    ((OrderDual.ofDual : (a : (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) → PrimeSpectrum (↑R : Type u_1))
        ((OrderDual.toDual : (a : PrimeSpectrum (↑R : Type u_1)) → (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) x) :
      PrimeSpectrum (↑R : Type u_1))
Tactic: rw [PrimeSpectrum.height_eq_orderHeight,
    ← Order.coheight_orderIso (specOrderIsoPrimeSpectrum R), ← height_ofDual,
    specOrderIsoPrimeSpectrum_apply, OrderDual.ofDual_toDual]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
R : CommRingCat
x : ↥(Spec R)
rw : height x = coheight x
rw₁ :
  height x =
    coheight (α := (PrimeSpectrum (↑R : Type u_1))ᵒᵈ)
      ((specOrderIsoPrimeSpectrum R : (a : ↥(Spec R)) → (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) x :
        (PrimeSpectrum (↑R : Type u_1))ᵒᵈ)
rw₂ :
  height x =
    height (α := PrimeSpectrum (↑R : Type u_1))
      ((OrderDual.ofDual : (a : (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) → PrimeSpectrum (↑R : Type u_1))
          ((specOrderIsoPrimeSpectrum R : (a : ↥(Spec R)) → (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) x) :
        PrimeSpectrum (↑R : Type u_1))
rw₃ :
  height x =
    height (α := PrimeSpectrum (↑R : Type u_1))
      ((OrderDual.ofDual : (a : (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) → PrimeSpectrum (↑R : Type u_1))
          ((OrderDual.toDual : (a : PrimeSpectrum (↑R : Type u_1)) → (PrimeSpectrum (↑R : Type u_1))ᵒᵈ) x) :
        PrimeSpectrum (↑R : Type u_1))
⊢ x.asIdeal.height = coheight x
have rw₄ : height x = height x
Tactic: rw [PrimeSpectrum.height_eq_orderHeight,
    ← Order.coheight_orderIso (specOrderIsoPrimeSpectrum R), ← height_ofDual,
    specOrderIsoPrimeSpectrum_apply, OrderDual.ofDual_toDual]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
x : ↥X
⊢ ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
have inr : ∀
  (this :
    ∀ {X : Scheme.{u_1}} (x : ↥X) (h : ∃ (R : CommRingCat.{u_1}), X = Spec R),
      ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞))
  (h : ¬∃ (R : CommRingCat.{u_1}), X = Spec R),
  ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
Tactic: wlog h : ∃ R, X = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
x : ↥X
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u_1}} (x : ↥X) (h : ∃ (R : CommRingCat.{u_1}), X = Spec R),
        ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞))
    (h : ¬∃ (R : CommRingCat.{u_1}), X = Spec R),
    ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
⊢ ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
have wlog : ∀ {X : Scheme.{u_1}} (x : ↥X) (h : ∃ (R : CommRingCat.{u_1}), X = Spec R),
  ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
Tactic: wlog h : ∃ R, X = Spec R
Cleared hypotheses: X, x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
x : ↥X
this :
  ∀ {X : Scheme.{u_1}} (x : ↥X) (h : ∃ (R : CommRingCat.{u_1}), X = Spec R),
    ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
h : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
⊢ ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
have inr : ∀ (R : CommRingCat.{u_1}) (f : Spec R ⟶ X) (hf : IsOpenImmersion f)
  (hsub :
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑⊤ : Set ↥X)),
  ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
Tactic: obtain ⟨R, f, hf, hsub⟩ := Scheme.exists_affine_mem_range_and_range_subset
      (show x ∈ ⊤ from trivial)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
x : ↥X
this :
  ∀ {X : Scheme.{u_1}} (x : ↥X) (h : ∃ (R : CommRingCat.{u_1}), X = Spec R),
    ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
h : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
R : CommRingCat
f : Spec R ⟶ X
hf : IsOpenImmersion f
hsub : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑⊤ : Set ↥X)
⊢ ringKrullDim.{u_1} (↑(X.presheaf.stalk x) : Type u_1) = (↑(coheight x) : WithBot ℕ∞)
have inr : ∀ (y : ↥(Spec R))
  (hsub :
    Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) (f y : ↥X) ∧
      Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑⊤ : Set ↥X)),
  ringKrullDim.{u_1} (↑(X.presheaf.stalk (f y)) : Type u_1) = (↑(coheight (α := ↥X) (f y : ↥X)) : WithBot ℕ∞)
Tactic: obtain ⟨y, rfl⟩ := Set.mem_range.mp hsub.1
Cleared hypotheses: x, hsub