awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : R
d : ↥v.asIdeal.primeCompl
hnd : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
⊢ ∃ (n : R) (d : ↥v.asIdeal.primeCompl),
    HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) (↑d : R) : K) = (algebraMap R K : (a : R) → K) n
have inr : n ∈ v.asIdeal.primeCompl
Tactic: refine ⟨d, ⟨n, ?_⟩, hnd⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : R
d : ↥v.asIdeal.primeCompl
hnd : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
⊢ n ∈ v.asIdeal.primeCompl
have inr : Eq (α := WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: rw [← v.intValuation_eq_one_iff_mem_primeCompl]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : R
d : ↥v.asIdeal.primeCompl
hnd : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have inr : 1 ≤
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
Tactic: apply eq_one_of_one_le_mul_right hv (intValuation_le_one v n)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : R
d : ↥v.asIdeal.primeCompl
hnd : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
⊢ 1 ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
have inr : (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑d : R) ≤
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
Tactic: rw [← (v.intValuation_eq_one_iff_mem_primeCompl d).mpr d.prop,
      ← valuation_of_algebraMap (K := K), ← valuation_of_algebraMap (K := K), ← map_mul, hnd]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : R
d : ↥v.asIdeal.primeCompl
hnd : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
inr :
  (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑d : R) ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
⊢ 1 ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
have inr₁ : ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑(↑d : R) : K) ≤
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
Tactic: rw [← (v.intValuation_eq_one_iff_mem_primeCompl d).mpr d.prop,
      ← valuation_of_algebraMap (K := K), ← valuation_of_algebraMap (K := K), ← map_mul, hnd]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : R
d : ↥v.asIdeal.primeCompl
hnd : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
inr :
  (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑d : R) ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
inr₁ :
  ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (↑(↑d : R) : K) ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
⊢ 1 ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
have inr₂ : ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑(↑d : R) : K) ≤
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑n : K) :
      WithZero (Multiplicative ℤ))
Tactic: rw [← (v.intValuation_eq_one_iff_mem_primeCompl d).mpr d.prop,
      ← valuation_of_algebraMap (K := K), ← valuation_of_algebraMap (K := K), ← map_mul, hnd]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : R
d : ↥v.asIdeal.primeCompl
hnd : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
inr :
  (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑d : R) ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
inr₁ :
  ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (↑(↑d : R) : K) ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
inr₂ :
  ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (↑(↑d : R) : K) ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑n : K) :
        WithZero (Multiplicative ℤ))
⊢ 1 ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
have inr₃ : LE.le (α := WithZero (Multiplicative ℤ))
  (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (↑(↑d : R) : K) :
    WithZero (Multiplicative ℤ))
  (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (x * (↑n : K)) :
    WithZero (Multiplicative ℤ))
Tactic: rw [← (v.intValuation_eq_one_iff_mem_primeCompl d).mpr d.prop,
      ← valuation_of_algebraMap (K := K), ← valuation_of_algebraMap (K := K), ← map_mul, hnd]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
γ : Multiplicative ℤ
⊢ ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * a) < (↑γ : WithZero (Multiplicative ℤ))
have pos : ∀ (ha : a = 0),
  ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * a) < (↑γ : WithZero (Multiplicative ℤ))
Tactic: by_cases ha: a = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
γ : Multiplicative ℤ
pos :
  ∀ (ha : a = 0),
    ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * a) < (↑γ : WithZero (Multiplicative ℤ))
⊢ ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * a) < (↑γ : WithZero (Multiplicative ℤ))
have neg : ∀ (ha : ¬a = 0),
  ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * a) < (↑γ : WithZero (Multiplicative ℤ))
Tactic: by_cases ha: a = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
γ : Multiplicative ℤ
ha : a = 0
⊢ ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * a) < (↑γ : WithZero (Multiplicative ℤ))
have pos : ∀
  (hv :
    LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) 0 : WithZero (Multiplicative ℤ))),
  ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * 0) < (↑γ : WithZero (Multiplicative ℤ))
Tactic: subst ha
Cleared hypotheses: a, hv, ha
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
b : R
γ : Multiplicative ℤ
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) 0 : WithZero (Multiplicative ℤ))
⊢ ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * 0) < (↑γ : WithZero (Multiplicative ℤ))
have hv₁ : Eq (α := WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
  (0 : WithZero (Multiplicative ℤ))
Tactic: rw [map_zero, le_zero_iff] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
γ : Multiplicative ℤ
ha : ¬a = 0
⊢ ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * a) < (↑γ : WithZero (Multiplicative ℤ))
have hvaz : Ne (α := WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
  (0 : WithZero (Multiplicative ℤ))
Tactic: have hvaz := intValuation_ne_zero v a ha
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz :
  Ne (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
⊢ ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * a) < (↑γ : WithZero (Multiplicative ℤ))
have hγz : (↑γ : WithZero (Multiplicative ℤ)) ≠ 0
Tactic: have hγz : WithZero.coe γ ≠ 0 := WithZero.coe_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz :
  Ne (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
hγz : (↑γ : WithZero (Multiplicative ℤ)) ≠ 0
⊢ ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * a) < (↑γ : WithZero (Multiplicative ℤ))
have neg : ∀ (n : ℕ)
  (hna :
    LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a))
  (hnγ : exp (-(↑n : ℤ)) < (↑γ : WithZero (Multiplicative ℤ))),
  ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * a) < (↑γ : WithZero (Multiplicative ℤ))
Tactic: obtain ⟨n, hna, hnγ⟩ := exists_exp_neg_natCast_lt_and_lt hvaz hγz
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz :
  Ne (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
hγz : (↑γ : WithZero (Multiplicative ℤ)) ≠ 0
n : ℕ
hna :
  LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a)
hnγ : exp (-(↑n : ℤ)) < (↑γ : WithZero (Multiplicative ℤ))
⊢ ∃ (y : R), (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - y * a) < (↑γ : WithZero (Multiplicative ℤ))
have neg : ∃ (a_1 : R),
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - a_1 * a) : WithZero (Multiplicative ℤ))
    (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
Tactic: apply Exists.imp (fun _ h ↦ lt_of_le_of_lt h hnγ)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz :
  Ne (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
hγz : (↑γ : WithZero (Multiplicative ℤ)) ≠ 0
n : ℕ
hna :
  LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a)
hnγ : exp (-(↑n : ℤ)) < (↑γ : WithZero (Multiplicative ℤ))
⊢ emultiplicity v.asIdeal (Ideal.span {a}) ≤ (↑n : ℕ∞)
have grw : LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ))) ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a)
Tactic: grw [← exp_le_intValuation_iff_emultiplicity_le, hna]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz :
  Ne (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
hγz : (↑γ : WithZero (Multiplicative ℤ)) ≠ 0
n : ℕ
hna :
  LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a)
hnγ : exp (-(↑n : ℤ)) < (↑γ : WithZero (Multiplicative ℤ))
grw :
  LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a)
⊢ emultiplicity v.asIdeal (Ideal.span {a}) ≤ (↑n : ℕ∞)
have grw₁ : LE.le (α := WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
Tactic: grw [← exp_le_intValuation_iff_emultiplicity_le, hna]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
a b : R
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
γ : Multiplicative ℤ
ha : ¬a = 0
hvaz :
  Ne (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
hγz : (↑γ : WithZero (Multiplicative ℤ)) ≠ 0
n : ℕ
hna :
  LT.lt (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) a)
hnγ : exp (-(↑n : ℤ)) < (↑γ : WithZero (Multiplicative ℤ))
⊢ ∃ (a_1 : R),
    LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - a_1 * a) : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
have hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ (↑n : ℕ∞)
Tactic: have hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ n := by
      grw [← exp_le_intValuation_iff_emultiplicity_le, hna]