awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_2
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
x : R
hx : x ≠ 0
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) x) :
      WithZero (Multiplicative ℤ))
have obtain : ∀ (m : ℕ) (hm : (↑m : ℕ∞) = ord R x),
  LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) x) :
      WithZero (Multiplicative ℤ))
Tactic: obtain ⟨m, hm⟩ := ENat.ne_top_iff_exists.mp (ord_ne_top (a := x) (by simpa))
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_2
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : (↑m : ℕ∞) = ord R x
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) x) :
      WithZero (Multiplicative ℤ))
have simp_rw : LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
  (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
    WithZero (Multiplicative ℤ))
Tactic: simp_rw [ordFrac_eq_ord R hx, ordMonoidWithZeroHom_eq_coe _ (by simpa) hm.symm,
    WithZero.one_le_coe, ← ofAdd_zero, Multiplicative.ofAdd_le, Nat.cast_nonneg _]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_2
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : (↑m : ℕ∞) = ord R x
simp_rw :
  LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) x) :
      WithZero (Multiplicative ℤ))
have simp_rw₁ : LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
  ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑m : ℤ)) : WithZero (Multiplicative ℤ)) :
    WithZero (Multiplicative ℤ))
Tactic: simp_rw [ordFrac_eq_ord R hx, ordMonoidWithZeroHom_eq_coe _ (by simpa) hm.symm,
    WithZero.one_le_coe, ← ofAdd_zero, Multiplicative.ofAdd_le, Nat.cast_nonneg _]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_2
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : (↑m : ℕ∞) = ord R x
simp_rw :
  LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
simp_rw₁ :
  LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑m : ℤ)) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) x) :
      WithZero (Multiplicative ℤ))
have simp_rw₂ : LE.le (α := Multiplicative ℤ) (1 : Multiplicative ℤ)
  ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑m : ℤ) : Multiplicative ℤ)
Tactic: simp_rw [ordFrac_eq_ord R hx, ordMonoidWithZeroHom_eq_coe _ (by simpa) hm.symm,
    WithZero.one_le_coe, ← ofAdd_zero, Multiplicative.ofAdd_le, Nat.cast_nonneg _]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_2
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : (↑m : ℕ∞) = ord R x
simp_rw :
  LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
simp_rw₁ :
  LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑m : ℤ)) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
simp_rw₂ :
  LE.le (α := Multiplicative ℤ) (1 : Multiplicative ℤ)
    ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑m : ℤ) : Multiplicative ℤ)
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) x) :
      WithZero (Multiplicative ℤ))
have simp_rw₃ : LE.le (α := Multiplicative ℤ) ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) 0 : Multiplicative ℤ)
  ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑m : ℤ) : Multiplicative ℤ)
Tactic: simp_rw [ordFrac_eq_ord R hx, ordMonoidWithZeroHom_eq_coe _ (by simpa) hm.symm,
    WithZero.one_le_coe, ← ofAdd_zero, Multiplicative.ofAdd_le, Nat.cast_nonneg _]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_2
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
x : R
hx : x ≠ 0
m : ℕ
hm : (↑m : ℕ∞) = ord R x
simp_rw :
  LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
simp_rw₁ :
  LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑m : ℤ)) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
simp_rw₂ :
  LE.le (α := Multiplicative ℤ) (1 : Multiplicative ℤ)
    ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑m : ℤ) : Multiplicative ℤ)
simp_rw₃ :
  LE.le (α := Multiplicative ℤ) ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) 0 : Multiplicative ℤ)
    ((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑m : ℤ) : Multiplicative ℤ)
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) x) :
      WithZero (Multiplicative ℤ))
have simp_rw₄ : LE.le (α := ℤ) 0 (↑m : ℤ)
Tactic: simp_rw [ordFrac_eq_ord R hx, ordMonoidWithZeroHom_eq_coe _ (by simpa) hm.symm,
    WithZero.one_le_coe, ← ofAdd_zero, Multiplicative.ofAdd_le, Nat.cast_nonneg _]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_2
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
S : Type u_3
inst_7 : CommRing S
inst_8 : Algebra S R
inst_9 : Algebra S K
inst_10 : IsScalarTower S R K
a : S
ha : Ne.{u_1 + 1} (α := R) ((algebraMap S R : (a : S) → R) a : R) (0 : R)
f : K
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) f :
      WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) (a • f) :
      WithZero (Multiplicative ℤ))
have pos : ∀ (j : f = 0),
  LE.le (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) f :
      WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) (a • f) :
      WithZero (Multiplicative ℤ))
Tactic: by_cases j : f = 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 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_2
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
S : Type u_3
inst_7 : CommRing S
inst_8 : Algebra S R
inst_9 : Algebra S K
inst_10 : IsScalarTower S R K
a : S
ha : Ne.{u_1 + 1} (α := R) ((algebraMap S R : (a : S) → R) a : R) (0 : R)
f : K
pos :
  ∀ (j : f = 0),
    LE.le (α := WithZero (Multiplicative ℤ))
      (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) (a • f) :
        WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) f :
      WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) (a • f) :
      WithZero (Multiplicative ℤ))
have neg : ∀ (j : ¬f = 0),
  LE.le (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) f :
      WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) (a • f) :
      WithZero (Multiplicative ℤ))
Tactic: by_cases j : f = 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 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_2
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
S : Type u_3
inst_7 : CommRing S
inst_8 : Algebra S R
inst_9 : Algebra S K
inst_10 : IsScalarTower S R K
a : S
ha : Ne.{u_1 + 1} (α := R) ((algebraMap S R : (a : S) → R) a : R) (0 : R)
f : K
j : ¬f = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) f :
      WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) (a • f) :
      WithZero (Multiplicative ℤ))
have neg : LE.le (α := WithZero (Multiplicative ℤ))
  (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) f :
    WithZero (Multiplicative ℤ))
  (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
      (HSMul.hSMul (α := K) ((algebraMap S K : (a : S) → K) a : K) f) :
    WithZero (Multiplicative ℤ))
Tactic: suffices ordFrac R f ≤ ordFrac R (algebraMap S K a • f) by simp_all only [ne_eq,
    algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_2
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
S : Type u_3
inst_7 : CommRing S
inst_8 : Algebra S R
inst_9 : Algebra S K
inst_10 : IsScalarTower S R K
a : S
ha : Ne.{u_1 + 1} (α := R) ((algebraMap S R : (a : S) → R) a : R) (0 : R)
f : K
j : ¬f = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) f :
      WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        (HSMul.hSMul (α := K) ((algebraMap S K : (a : S) → K) a : K) f) :
      WithZero (Multiplicative ℤ))
have neg : ((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) f ≤
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap S K : (a : S) → K) a) :
      WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) f :
      WithZero (Multiplicative ℤ))
Tactic: simp only [smul_eq_mul, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsNoetherianRing R
inst_3 : KrullDimLE 1 R
K : Type u_2
inst_4 : Field K
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
S : Type u_3
inst_7 : CommRing S
inst_8 : Algebra S R
inst_9 : Algebra S K
inst_10 : IsScalarTower S R K
a : S
ha : Ne.{u_1 + 1} (α := R) ((algebraMap S R : (a : S) → R) a : R) (0 : R)
f : K
j : ¬f = 0
⊢ ((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) f ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap S K : (a : S) → K) a) :
        WithZero (Multiplicative ℤ))
      (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
have neg : LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
  (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
      ((algebraMap S K : (a : S) → K) a) :
    WithZero (Multiplicative ℤ))
Tactic: apply le_mul_of_one_le_left'
-- 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
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x : R
h : x ≠ 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) x) :
      WithZero (Multiplicative ℤ))
    ((((IsDedekindDomain.HeightOneSpectrum.intValuation (IsDiscreteValuationRing.maximalIdeal R) :
              Valuation R (WithZero (Multiplicative ℤ))) :
            (a : R) → WithZero (Multiplicative ℤ))
          x)⁻¹ :
      WithZero (Multiplicative ℤ))
have rw : Eq (α := WithZero (Multiplicative ℤ))
  (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
    WithZero (Multiplicative ℤ))
  ((((IsDedekindDomain.HeightOneSpectrum.intValuation (IsDiscreteValuationRing.maximalIdeal R) :
            Valuation R (WithZero (Multiplicative ℤ))) :
          (a : R) → WithZero (Multiplicative ℤ))
        x)⁻¹ :
    WithZero (Multiplicative ℤ))
Tactic: rw [ordFrac_eq_ord R h,
      ordMonoidWithZeroHom_eq_intValuation (mem_nonZeroDivisors_of_ne_zero 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
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x : R
h : x ≠ 0
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    ((((IsDedekindDomain.HeightOneSpectrum.intValuation (IsDiscreteValuationRing.maximalIdeal R) :
              Valuation 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 ℤ))
    ((((IsDedekindDomain.HeightOneSpectrum.intValuation (IsDiscreteValuationRing.maximalIdeal R) :
              Valuation R (WithZero (Multiplicative ℤ))) :
            (a : R) → WithZero (Multiplicative ℤ))
          x)⁻¹ :
      WithZero (Multiplicative ℤ))
have rw₁ : Eq (α := WithZero (Multiplicative ℤ))
  ((((IsDedekindDomain.HeightOneSpectrum.intValuation (IsDiscreteValuationRing.maximalIdeal R) :
            Valuation R (WithZero (Multiplicative ℤ))) :
          (a : R) → WithZero (Multiplicative ℤ))
        x)⁻¹ :
    WithZero (Multiplicative ℤ))
  ((((IsDedekindDomain.HeightOneSpectrum.intValuation (IsDiscreteValuationRing.maximalIdeal R) :
            Valuation R (WithZero (Multiplicative ℤ))) :
          (a : R) → WithZero (Multiplicative ℤ))
        x)⁻¹ :
    WithZero (Multiplicative ℤ))
Tactic: rw [ordFrac_eq_ord R h,
      ordMonoidWithZeroHom_eq_intValuation (mem_nonZeroDivisors_of_ne_zero 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
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
⊢ Eq (α := K →*₀ WithZero (Multiplicative ℤ)) (ordFrac R)
    (MonoidWithZeroHom.comp MonoidWithZero.inverse
      (Valuation.toMonoidWithZeroHom
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))))
have h : ∀ (a : K),
  Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) a :
      WithZero (Multiplicative ℤ))
    (((MonoidWithZeroHom.comp MonoidWithZero.inverse
              (Valuation.toMonoidWithZeroHom
                (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
            K →*₀ WithZero (Multiplicative ℤ)) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
Tactic: ext a
-- 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
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
a : K
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) a :
      WithZero (Multiplicative ℤ))
    (((MonoidWithZeroHom.comp MonoidWithZero.inverse
              (Valuation.toMonoidWithZeroHom
                (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
            K →*₀ WithZero (Multiplicative ℤ)) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
have pos : ∀ (ha : a = 0),
  Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) a :
      WithZero (Multiplicative ℤ))
    (((MonoidWithZeroHom.comp MonoidWithZero.inverse
              (Valuation.toMonoidWithZeroHom
                (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
            K →*₀ WithZero (Multiplicative ℤ)) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
Tactic: by_cases ha : a = 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
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
a : K
pos :
  ∀ (ha : a = 0),
    Eq (α := WithZero (Multiplicative ℤ))
      (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) a :
        WithZero (Multiplicative ℤ))
      (((MonoidWithZeroHom.comp MonoidWithZero.inverse
                (Valuation.toMonoidWithZeroHom
                  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
              K →*₀ WithZero (Multiplicative ℤ)) :
            (a : K) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) a :
      WithZero (Multiplicative ℤ))
    (((MonoidWithZeroHom.comp MonoidWithZero.inverse
              (Valuation.toMonoidWithZeroHom
                (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
            K →*₀ WithZero (Multiplicative ℤ)) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
have neg : ∀ (ha : ¬a = 0),
  Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) a :
      WithZero (Multiplicative ℤ))
    (((MonoidWithZeroHom.comp MonoidWithZero.inverse
              (Valuation.toMonoidWithZeroHom
                (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
            K →*₀ WithZero (Multiplicative ℤ)) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
Tactic: by_cases ha : a = 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
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
a : K
ha : ¬a = 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) a :
      WithZero (Multiplicative ℤ))
    (((MonoidWithZeroHom.comp MonoidWithZero.inverse
              (Valuation.toMonoidWithZeroHom
                (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
            K →*₀ WithZero (Multiplicative ℤ)) :
          (a : K) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))
have neg : ∀ (x y : R) (hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y)
  (ha : ¬HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K) = 0),
  Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)) :
      WithZero (Multiplicative ℤ))
    (((MonoidWithZeroHom.comp MonoidWithZero.inverse
              (Valuation.toMonoidWithZeroHom
                (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))) :
            K →*₀ WithZero (Multiplicative ℤ)) :
          (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) x : K) ((algebraMap R K : (a : R) → K) y : K)) :
      WithZero (Multiplicative ℤ))
Tactic: obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := R) a
Cleared hypotheses: a, ha
-- 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
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
⊢ Eq (α := Submonoid K) (MonoidHom.mker (F := K →*₀ WithZero (Multiplicative ℤ)) (ordFrac R))
    (Submonoid.map (F := R →+* K) (algebraMap R K) (IsUnit.submonoid R))
have rw : Eq (α := Submonoid K)
  (Submonoid.comap (F := K →*₀ WithZero (Multiplicative ℤ))
    (Valuation.toMonoidWithZeroHom (valuation K (IsDiscreteValuationRing.maximalIdeal R))) ⊥)
  (Submonoid.map (F := R →+* K) (algebraMap R K) (IsUnit.submonoid R))
Tactic: rw [ordFrac_eq_inverse_comp_valuation, ← MonoidWithZeroHom.comap_mker,
      MonoidWithZeroHom.mker_inverse]