awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
y : ↥(nonZeroDivisors R)
⊢ Eq (α := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          ⊤ :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ↔
    Eq (α := ℕ∞) ⊤ ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
y : ↥(nonZeroDivisors R)
a : ℕ
⊢ Eq (α := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (↑a : ℕ∞) :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ↔
    Eq (α := ℕ∞) (↑a : ℕ∞) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
x : R
h : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        (ord R x) :
      WithZero (Multiplicative ℤ))

Tactic:
dif_pos h

Premises used: dif_pos, dite, ite
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
n : ℕ
hn : ord R x = (↑n : ℕ∞)
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑n : ℤ)) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))

Tactic:
simp [ordMonoidWithZeroHom_eq_ord hx, hn]

Premises used: Ring.ordMonoidWithZeroHom_eq_ord
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
x : R
h : x ∉ nonZeroDivisors R
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))

Tactic:
dif_neg h

Premises used: dif_neg, dite, ite
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
rw :
  IsNoetherian R (HasQuotient.Quotient R (B := Ideal R) (span {x})) ∧
    IsArtinian R (HasQuotient.Quotient R (B := Ideal R) (span {x}))
⊢ IsFiniteLength R (HasQuotient.Quotient R (B := Ideal R) (span {x}))

Tactic:
rw [isFiniteLength_iff_isNoetherian_isArtinian]

Premises used: isFiniteLength_iff_isNoetherian_isArtinian
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
suffices : IsArtinianRing.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {x}))
⊢ IsNoetherian R (HasQuotient.Quotient R (B := Ideal R) (span {x})) ∧
    IsArtinian R (HasQuotient.Quotient R (B := Ideal R) (span {x}))

Tactic:
suffices IsArtinianRing (R ⧸ Ideal.span {x}) from
    ⟨isNoetherian_quotient (Ideal.span {x}),
      isArtinian_of_surjective_algebraMap (Ideal.Quotient.mk_surjective (I := .span {x}))⟩
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ Ne (α := WithBot (WithTop ℕ)) 1 ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ ¬Eq (α := WithTop ℕ) 1 ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
rw : Order.krullDim.{u_1} (PrimeSpectrum (HasQuotient.Quotient R (B := Ideal R) (span {x}))) + 1 ≤ 1
⊢ IsArtinianRing.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {x}))

Tactic:
rw [isArtinianRing_iff_krullDimLE_zero, Ring.KrullDimLE, Order.krullDimLE_iff,
    ← WithBot.add_le_add_iff_right' (c := 1) (by simp) (WithBot.coe_eq_coe.not.mpr (by simp)),
    Nat.cast_zero, zero_add]

Premises used: WithBot.add_le_add_iff_right', zero_add, Nat.cast_zero, Ring.KrullDimLE, isArtinianRing_iff_krullDimLE_zero, Order.krullDimLE_iff
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ Order.krullDim.{u_1} (PrimeSpectrum (HasQuotient.Quotient R (B := Ideal R) (span {x}))) + 1 ≤ 1

Tactic:
(ringKrullDim_quotient_succ_le_of_nonZeroDivisor hx).trans (Order.KrullDimLE.krullDim_le)

Premises used: WithBot, Set.Mem, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, ENat, ringKrullDim, Order.KrullDimLE.krullDim_le, LE.le.trans, WithTop
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ Order.krullDim.{u_1} (PrimeSpectrum (HasQuotient.Quotient R (B := Ideal R) (span {x}))) + 1 ≤ 1

Tactic:
exact (ringKrullDim_quotient_succ_le_of_nonZeroDivisor hx).trans (Order.KrullDimLE.krullDim_le)

Premises used: ringKrullDim_quotient_succ_le_of_nonZeroDivisor, Order.KrullDimLE.krullDim_le, LE.le.trans
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
a : R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
⊢ ord R a ≠ ⊤

Tactic:
simp [isFiniteLength_quotient_span_singleton R ha, Ring.ord, Module.length_ne_top_iff]

Premises used: Ring.ord, isFiniteLength_quotient_span_singleton, Module.length_ne_top_iff
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
a : R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
⊢ ord R a < ⊤

Tactic:
(ord_ne_top ha).lt_top

Premises used: Ne.lt_top, Ring.ord_ne_top
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
y : ↥(nonZeroDivisors R)
⊢ IsUnit (M := WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) (↑y : R) :
      WithZero (Multiplicative ℤ))

Tactic:
simp [ordMonoidWithZeroHom_eq_zero_iff, ord_ne_top]

Premises used: Ring.ordMonoidWithZeroHom_eq_zero_iff, Ring.ord_ne_top
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
K : Type u_3
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
inst_6 : Nontrivial R
x : R
hx : x ≠ 0
⊢ IsDomain R

Tactic:
have := (FaithfulSMul.algebraMap_injective R K).isDomain
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
K : Type u_3
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
inst_6 : Nontrivial R
x : R
hx : x ≠ 0
this : IsDomain R
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) x) :
      WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))

Tactic:
(Submonoid.LocalizationMap.lift_eq ..).trans ?_

Premises used: Set.Mem, Submonoid.LocalizationMap.lift_eq, Eq.trans
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
K : Type u_3
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
inst_6 : Nontrivial R
x : R
hx : x ≠ 0
this : IsDomain R
refine :
  Eq (α := WithZero (Multiplicative ℤ))
    ((((↑(ordMonoidWithZeroHom R) : R →* WithZero (Multiplicative ℤ)) : R →* WithZero (Multiplicative ℤ)) :
          (a : R) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) x) :
      WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))

Tactic:
refine (Submonoid.LocalizationMap.lift_eq ..).trans ?_

Premises used: Submonoid.LocalizationMap.lift_eq, Eq.trans
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
K : Type u_3
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
inst_6 : Nontrivial R
x : R
hx : x ≠ 0
this : IsDomain R
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((((↑(ordMonoidWithZeroHom R) : R →* WithZero (Multiplicative ℤ)) : R →* WithZero (Multiplicative ℤ)) :
          (a : R) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))

Tactic:
simp [ordMonoidWithZeroHom, mem_nonZeroDivisors_iff_ne_zero.mpr hx]

Premises used: Iff.mpr, mem_nonZeroDivisors_iff_ne_zero, Ring.ordMonoidWithZeroHom
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
K : Type u_3
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
inst_6 : Nontrivial R
a b : ↥(nonZeroDivisors R)
⊢ ((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) (mk' K (↑a : R) b) =
    HDiv.hDiv (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) (↑a : R) :
        WithZero (Multiplicative ℤ))
      (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) (↑b : R) :
        WithZero (Multiplicative ℤ))

Tactic:
simp [ordFrac_eq_ord]

Premises used: Ring.ordFrac_eq_ord
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_2
inst_1 : CommRing R
inst_2 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_3
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
⊢ Eq (α := Multiplicative ℕ)
    ((Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) (ord R (↑1 : R)).toNat : Multiplicative ℕ)
    (1 : Multiplicative ℕ)

Tactic:
simp [OneMemClass.coe_one, isUnit_one, ord_of_isUnit]

Premises used: Ring.ord_of_isUnit, OneMemClass.coe_one, isUnit_one
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R_1 : Type u_1
inst : CommRing R_1
R : Type u_2
inst_1 : CommRing R
inst_2 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_3
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
x y : ↥R⁰
⊢ (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) (ord R (↑(x * y) : R)).toNat =
    HMul.hMul (α := Multiplicative ℕ) (β := Multiplicative ℕ)
      ((Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) (ord R (↑x : R)).toNat : Multiplicative ℕ)
      ((Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) (ord R (↑y : R)).toNat : Multiplicative ℕ)

Tactic:
simp [ord_mul, ENat.toNat_add (ord_ne_top x.2) (ord_ne_top y.2)]

Premises used: ENat.toNat_add, Ring.ord_ne_top, Ring.ord_mul, Subtype.property
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
x : ↥R⁰
⊢ (↑((Multiplicative.toAdd : (a : Multiplicative ℕ) → ℕ)
          (((ordMonoidHom : ↥R⁰ →* Multiplicative ℕ) : (a : ↥R⁰) → Multiplicative ℕ) x : Multiplicative ℕ)) :
      ℕ∞) =
    ord R (↑x : R)

Tactic:
(ENat.coe_toNat (ord_ne_top x.2))

Premises used: ENat.coe_toNat, ENat.toNat, Ring.ord_ne_top, WithTop.untopD, WithTop.recTopCoe, Subtype.property
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
x : ↥R⁰
simp :
  Eq (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑(ord R (↑x : R)).toNat : ℤ)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        (ord R (↑x : R)) :
      WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ)
            (↑((Multiplicative.toAdd : (a : Multiplicative ℕ) → ℕ)
                  (((ordMonoidHom : ↥R⁰ →* Multiplicative ℕ) : (a : ↥R⁰) → Multiplicative ℕ) x : Multiplicative ℕ)) :
              ℤ)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) (↑x : R) :
      WithZero (Multiplicative ℤ))

Tactic:
simp only [SetLike.coe_mem, ordMonoidWithZeroHom_eq_ord, ordMonoidHom, MonoidHom.coe_mk,
    OneHom.coe_mk, toAdd_ofAdd]

Premises used: Ring.ordMonoidWithZeroHom_eq_ord, SetLike.coe_mem, OneHom.coe_mk, toAdd_ofAdd, Ring.ordMonoidHom, MonoidHom.coe_mk
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
x : ↥R⁰
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑(ENat.toNat (↑((ord R (↑x : R)).lift ⋯) : ℕ∞)) : ℤ)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        (↑((ord R (↑x : R)).lift ⋯) : ℕ∞) :
      WithZero (Multiplicative ℤ))
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑(ENat.toNat (↑((ord R (↑x : R)).lift ⋯) : ℕ∞)) : ℤ)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑((ord R (↑x : R)).lift ⋯) : ℤ)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑(ord R (↑x : R)).toNat : ℤ)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑((ord R (↑x : R)).lift ⋯) : ℤ)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
rw₃ rw₄ :
  Eq (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑(ord R (↑x : R)).toNat : ℤ)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑(ord R (↑x : R)).toNat : ℤ)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑(ord R (↑x : R)).toNat : ℤ)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        (ord R (↑x : R)) :
      WithZero (Multiplicative ℤ))

Tactic:
rw [← ENat.coe_lift (ord R x.1) (ord_lt_top x.2), ENat.recTopCoe_coe,
    ENat.coe_lift, ENat.lift_eq_toNat_of_lt_top]

Premises used: Ring.ord, ENat.coe_lift, ENat.recTopCoe_coe, ENat.lift_eq_toNat_of_lt_top, Ring.ord_lt_top, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
a : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
⊢ Membership.mem (γ := Submonoid R) R⁰ a

Tactic:
ha
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
a : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
lift :
  ∀ (a : ↥R⁰),
    Ne (α := WithZero (Multiplicative ℤ))
      (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) (↑a : R) :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ Ne (α := WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) a :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))

Tactic:
lift a to R⁰ using ha
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
a : ↥R⁰
⊢ Ne (α := WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) (↑a : R) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))

Tactic:
simp [← ordMonoidWithZeroHom_eq_ordMonoidHom]

Premises used: Ring.ordMonoidWithZeroHom_eq_ordMonoidHom
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
hb : Membership.mem (γ := Submonoid R) R⁰ b
⊢ Membership.mem (γ := Submonoid R) R⁰ a

Tactic:
ha
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
a b : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
hb : Membership.mem (γ := Submonoid R) R⁰ b
lift :
  ∀ (a : ↥R⁰),
    ord R (↑a : R) ≤ ord R b ↔
      LE.le (α := WithZero (Multiplicative ℤ))
        (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ))
            (↑a : R) :
          WithZero (Multiplicative ℤ))
        (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) b :
          WithZero (Multiplicative ℤ))
⊢ ord R a ≤ ord R b ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) a :
        WithZero (Multiplicative ℤ))
      (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) b :
        WithZero (Multiplicative ℤ))

Tactic:
lift a to R⁰ using ha
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
b : R
hb : Membership.mem (γ := Submonoid R) R⁰ b
a : ↥R⁰
⊢ Membership.mem (γ := Submonoid R) R⁰ b

Tactic:
hb
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
b : R
hb : Membership.mem (γ := Submonoid R) R⁰ b
a : ↥R⁰
lift :
  ∀ (b : ↥R⁰),
    ord R (↑a : R) ≤ ord R (↑b : R) ↔
      LE.le (α := WithZero (Multiplicative ℤ))
        (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ))
            (↑a : R) :
          WithZero (Multiplicative ℤ))
        (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ))
            (↑b : R) :
          WithZero (Multiplicative ℤ))
⊢ ord R (↑a : R) ≤ ord R b ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) (↑a : R) :
        WithZero (Multiplicative ℤ))
      (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) b :
        WithZero (Multiplicative ℤ))

Tactic:
lift b to R⁰ using hb
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
a b : ↥R⁰
⊢ ord R (↑a : R) ≤ ord R (↑b : R) ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) (↑a : R) :
        WithZero (Multiplicative ℤ))
      (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) (↑b : R) :
        WithZero (Multiplicative ℤ))

Tactic:
simp [← ordMonoidWithZeroHom_eq_ordMonoidHom, ← ordMonoidHom_eq_ord]

Premises used: Ring.ordMonoidWithZeroHom_eq_ordMonoidHom, Ring.ordMonoidHom_eq_ord
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
pos : ∀ (hx : x = 0), ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
neg : ∀ (hx : ¬x = 0), ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
⊢ ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x = 0
pos : Module.length R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x})) = ⊤
⊢ ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x

Tactic:
simp only [ord, hx, AddValuation.map_zero]

Premises used: Ring.ord, AddValuation.map_zero
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x = 0
pos : Module.length R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0})) = ⊤
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x})) = ⊤

Tactic:
subst hx
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
pos : ∀ (this : Module.length R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0})) ≠ ⊤), False
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0})) = ⊤

Tactic:
by_contra!