awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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
⊢ IsArtinianRing.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {x}))
have rw : Order.krullDim.{u_1} (PrimeSpectrum (HasQuotient.Quotient R (B := Ideal R) (span {x}))) + 1 ≤ 1
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]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (hypothesis)
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
⊢ 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 ℤ))
have this : IsDomain R
Tactic: have := (FaithfulSMul.algebraMap_injective R K).isDomain
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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 ℤ))
have 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 ℤ))
Tactic: refine (Submonoid.LocalizationMap.lift_eq ..).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
x : ↥R⁰
⊢ 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 ℤ))
have 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 ℤ))
Tactic: simp only [SetLike.coe_mem, ordMonoidWithZeroHom_eq_ord, ordMonoidHom, MonoidHom.coe_mk,
    OneHom.coe_mk, toAdd_ofAdd]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
inst_3 : Nontrivial R
x : ↥R⁰
⊢ 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 ℤ))
have rw : Eq (α := WithZero (Multiplicative ℤ))
  ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑(ENat.toNat (↑((ord R (↑x : R)).lift sorry) : ℕ∞)) : ℤ)) :
      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 sorry) : ℕ∞) :
    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]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
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 ℤ))
⊢ 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 ℤ))
have rw₁ : Eq (α := WithZero (Multiplicative ℤ))
  ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑(ENat.toNat (↑((ord R (↑x : R)).lift sorry) : ℕ∞)) : ℤ)) :
      WithZero (Multiplicative ℤ)) :
    WithZero (Multiplicative ℤ))
  ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑((ord R (↑x : R)).lift sorry) : ℤ)) :
      WithZero (Multiplicative ℤ)) :
    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]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
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 ℤ))
⊢ 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 ℤ))
have 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 sorry) : ℤ)) :
      WithZero (Multiplicative ℤ)) :
    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]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
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 ℤ))
⊢ 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 ℤ))
have 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 ℤ))
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]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
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
⊢ Ne (α := WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) a :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
have lift : ∀ (a : ↥R⁰),
  Ne (α := WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) (↑a : R) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
Tactic: lift a to R⁰ using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
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
⊢ 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 ℤ))
have 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 ℤ))
Tactic: lift a to R⁰ using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
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⁰
⊢ 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 ℤ))
have 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 ℤ))
Tactic: lift b to R⁰ using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
⊢ ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
have pos : ∀ (hx : x = 0), ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
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
⊢ ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
have neg : ∀ (hx : ¬x = 0), ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x = 0
⊢ ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
have pos : Module.length R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x})) = ⊤
Tactic: simp only [ord, hx, AddValuation.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : x = 0
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {x})) = ⊤
have pos : Module.length R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0})) = ⊤
Tactic: subst hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0})) = ⊤
have pos : ∀ (this : Module.length R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0})) ≠ ⊤), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
this : Module.length R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0})) ≠ ⊤
⊢ False
have this₁ : IsNoetherian R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0})) ∧
  IsArtinian R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0}))
Tactic: rw [Module.length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
this :
  IsNoetherian R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0})) ∧
    IsArtinian R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0}))
⊢ False
have art : IsArtinian R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0}))
Tactic: have art := this.2
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
this :
  IsNoetherian R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0})) ∧
    IsArtinian R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0}))
art : IsArtinian R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0}))
⊢ False
have art₁ : IsArtinian R (HasQuotient.Quotient R (B := Ideal R) ⊥)
Tactic: rw [Ideal.span_singleton_zero] at art
Cleared hypotheses: art
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
this :
  IsNoetherian R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0})) ∧
    IsArtinian R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0}))
art : IsArtinian R (HasQuotient.Quotient R (B := Ideal R) ⊥)
⊢ False
have this₁ : IsArtinianRing R
Tactic: have : IsArtinianRing R :=
      (LinearEquiv.isArtinian_iff (Submodule.quotEquivOfEqBot ⊥ rfl).symm).mpr art
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : ¬x = 0
⊢ ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
have neg : ∀ (ϖ : R) (hϖ : Irreducible ϖ), ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
Tactic: obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible R
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x : R
hx : ¬x = 0
ϖ : R
hϖ : Irreducible ϖ
⊢ ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
have neg : ∀ (m : ℕ) (α : Rˣ) (hx : ¬(↑α : R) * ϖ ^ m = 0),
  ord R ((↑α : R) * ϖ ^ m) = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑α : R) * ϖ ^ m)
Tactic: obtain ⟨m, α, rfl⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hx hϖ
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬(↑α : R) * ϖ ^ m = 0
⊢ ord R ((↑α : R) * ϖ ^ m) = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑α : R) * ϖ ^ m)
have neg : ord R (↑α : R) + HSMul.hSMul (β := ℕ∞) m 1 =
  ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑α : R) * ϖ ^ m)
Tactic: rw [ord_mul, ord_pow, ord_of_irreducible hϖ]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬(↑α : R) * ϖ ^ m = 0
neg :
  ord R (↑α : R) + HSMul.hSMul (β := ℕ∞) m 1 =
    ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑α : R) * ϖ ^ m)
⊢ ord R ((↑α : R) * ϖ ^ m) = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑α : R) * ϖ ^ m)
have neg₁ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) ϖ
Tactic: rw [ord_mul, ord_pow, ord_of_irreducible hϖ]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
m : ℕ
α : Rˣ
hx : ¬(↑α : R) * ϖ ^ m = 0
neg :
  ord R (↑α : R) + HSMul.hSMul (β := ℕ∞) m 1 =
    ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑α : R) * ϖ ^ m)
neg₁ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) ϖ
⊢ ord R ((↑α : R) * ϖ ^ m) = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑α : R) * ϖ ^ m)
have neg₂ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (ϖ ^ m)
Tactic: rw [ord_mul, ord_pow, ord_of_irreducible hϖ]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
⊢ min (ord R x) (ord R y) ≤ ord R (x + y)
have grw : min (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) (ord R y) ≤ ord R (x + y)
Tactic: grw [ord_eq_addVal x, ord_eq_addVal y, ord_eq_addVal (x + y), IsDiscreteValuationRing.addVal_add]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
grw : min (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) (ord R y) ≤ ord R (x + y)
⊢ min (ord R x) (ord R y) ≤ ord R (x + y)
have grw₁ : min (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y) ≤
  ord R (x + y)
Tactic: grw [ord_eq_addVal x, ord_eq_addVal y, ord_eq_addVal (x + y), IsDiscreteValuationRing.addVal_add]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
grw : min (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) (ord R y) ≤ ord R (x + y)
grw₁ :
  min (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y) ≤
    ord R (x + y)
⊢ min (ord R x) (ord R y) ≤ ord R (x + y)
have grw₂ : LE.le (α := ℕ∞)
  (min (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y) : ℕ∞)
  (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (x + y) : ℕ∞)
Tactic: grw [ord_eq_addVal x, ord_eq_addVal y, ord_eq_addVal (x + y), IsDiscreteValuationRing.addVal_add]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
grw : min (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) (ord R y) ≤ ord R (x + y)
grw₁ :
  min (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y) ≤
    ord R (x + y)
grw₂ :
  LE.le (α := ℕ∞)
    (min (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) y) : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (x + y) : ℕ∞)
⊢ min (ord R x) (ord R y) ≤ ord R (x + y)
have grw₃ : LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (x + y) : ℕ∞)
  (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (x + y) : ℕ∞)
Tactic: grw [ord_eq_addVal x, ord_eq_addVal y, ord_eq_addVal (x + y), IsDiscreteValuationRing.addVal_add]