awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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})) ≠ ⊤
⊢ 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

Premises used: Module.length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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}))
⊢ IsArtinian R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {0}))

Tactic:
have art := this.2
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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}))
⊢ IsArtinian R (HasQuotient.Quotient R (B := Ideal R) ⊥)

Tactic:
rw [Ideal.span_singleton_zero] at art

Premises used: Ideal.span_singleton_zero
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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) ⊥)
⊢ IsArtinianRing R

Tactic:
have : IsArtinianRing R :=
      (LinearEquiv.isArtinian_iff (Submodule.quotEquivOfEqBot ⊥ rfl).symm).mpr art
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
this_1 :
  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) ⊥)
this : IsArtinianRing R
⊢ False

Tactic:
IsDiscreteValuationRing.not_krullDimLE_zero R inferInstance

Premises used: inferInstance, IsDiscreteValuationRing.not_krullDimLE_zero
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
this_1 :
  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) ⊥)
this : IsArtinianRing R
⊢ False

Tactic:
exact IsDiscreteValuationRing.not_krullDimLE_zero R inferInstance

Premises used: inferInstance, IsDiscreteValuationRing.not_krullDimLE_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
neg :
  ∀ (ϖ : R) (hϖ : Irreducible ϖ), ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x
⊢ ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x

Tactic:
obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible R

Premises used: IsDiscreteValuationRing.exists_irreducible
-- 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
ϖ : R
hϖ : Irreducible ϖ
neg :
  ∀ (m : ℕ) (α : Rˣ) (hx : ¬(↑α : R) * ϖ ^ m = 0),
    ord R ((↑α : R) * ϖ ^ m) =
      ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑α : R) * ϖ ^ m)
⊢ ord R x = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) x

Tactic:
obtain ⟨m, α, rfl⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hx hϖ

Premises used: IsDiscreteValuationRing.eq_unit_mul_pow_irreducible, rfl
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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) ϖ
neg₂ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (ϖ ^ m)
⊢ ord R ((↑α : R) * ϖ ^ m) = ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑α : R) * ϖ ^ m)

Tactic:
rw [ord_mul, ord_pow, ord_of_irreducible hϖ]

Premises used: Ring.ord_pow, Ring.ord_of_irreducible, Ring.ord_mul
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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) + HSMul.hSMul (β := ℕ∞) m 1 =
    ((IsDiscreteValuationRing.addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) ((↑α : R) * ϖ ^ m)

Tactic:
simp [IsDiscreteValuationRing.addVal_uniformizer hϖ]

Premises used: IsDiscreteValuationRing.addVal_uniformizer
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) ϖ

Tactic:
simp_all [Irreducible.ne_zero hϖ]

Premises used: Irreducible.ne_zero
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (ϖ ^ m)

Tactic:
simp_all [Irreducible.ne_zero hϖ]

Premises used: Irreducible.ne_zero
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
x y : R
⊢ ord R x = ord R y ↔ Associated x y

Tactic:
simp [addVal_eq_iff_associated]

Premises used: IsDiscreteValuationRing.addVal_eq_iff_associated
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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) : ℕ∞)
grw₃ grw₄ :
  LE.le (α := ℕ∞) (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (x + y) : ℕ∞)
    (((addVal R : AddValuation R ℕ∞) : (a : R) → ℕ∞) (x + y) : ℕ∞)
⊢ min (ord 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]

Premises used: Ring.ord_eq_addVal, IsDiscreteValuationRing.addVal_add, HAdd.hAdd
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x

Tactic:
simpa
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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
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 ℤ))
⊢ 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))

Premises used: ENat.ne_top_iff_exists, Iff.mp, Ring.ord_ne_top
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x

Tactic:
simpa
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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 ℤ)
simp_rw₄ : LE.le (α := ℤ) 0 (↑m : ℤ)
⊢ 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:
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 _]

Premises used: Multiplicative.ofAdd_le, Ring.ordFrac_eq_ord, ofAdd_zero, Nat.cast_nonneg, Ring.ordMonoidWithZeroHom_eq_coe, WithZero.one_le_coe, Eq.symm
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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 ℤ))
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 ℤ))
⊢ 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
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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 ℤ))

Tactic:
simp [j]
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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
this :
  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 ℤ))
⊢ 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:
simp_all only [ne_eq,
    algebraMap_smul]

Premises used: algebraMap_smul, ne_eq
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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
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 ℤ))
⊢ 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:
suffices ordFrac R f ≤ ordFrac R (algebraMap S K a • f) by simp_all only [ne_eq,
    algebraMap_smul]
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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
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 ℤ))
⊢ 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:
simp only [smul_eq_mul, map_mul]

Premises used: map_mul, smul_eq_mul
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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
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 ℤ))
⊢ ((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:
apply le_mul_of_one_le_left'

Premises used: le_mul_of_one_le_left'
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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 ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap S K : (a : S) → K) a) :
      WithZero (Multiplicative ℤ))

Tactic:
simp [IsScalarTower.algebraMap_eq S R K, ordFrac_ge_one_of_ne_zero ha]

Premises used: IsScalarTower.algebraMap_eq, Ring.ordFrac_ge_one_of_ne_zero
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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 : IsUnit x
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) x) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simp [ordFrac_eq_ord R (IsUnit.ne_zero hx), IsUnit.mem_nonZeroDivisors hx,
      ordMonoidWithZeroHom_eq_ord, ord_of_isUnit hx]

Premises used: Ring.ordMonoidWithZeroHom_eq_ord, Ring.ord_of_isUnit, Ring.ordFrac_eq_ord, IsUnit.mem_nonZeroDivisors, IsUnit.ne_zero
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing 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 ℤ))
    ((((IsDedekindDomain.HeightOneSpectrum.intValuation (IsDiscreteValuationRing.maximalIdeal R) :
              Valuation R (WithZero (Multiplicative ℤ))) :
            (a : R) → WithZero (Multiplicative ℤ))
          x)⁻¹ :
      WithZero (Multiplicative ℤ))

Tactic:
simp [ordMonoidWithZeroHom_eq_ord h, IsDiscreteValuationRing.intValuation_maximalIdeal]

Premises used: Ring.ordMonoidWithZeroHom_eq_ord, IsDiscreteValuationRing.intValuation_maximalIdeal
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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 ℤ))
rw₁ 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 ℤ))
⊢ 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 ℤ))

Tactic:
rw [ordFrac_eq_ord R h,
      ordMonoidWithZeroHom_eq_intValuation (mem_nonZeroDivisors_of_ne_zero h)]

Premises used: Ring.ordFrac_eq_ord, Ring.ordMonoidWithZeroHom_eq_intValuation, mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian
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
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 ℤ))
⊢ Eq (α := K →*₀ WithZero (Multiplicative ℤ)) (ordFrac R)
    (MonoidWithZeroHom.comp MonoidWithZero.inverse
      (Valuation.toMonoidWithZeroHom
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R))))

Tactic:
ext a