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
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 ℤ))
hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ (↑n : ℕ∞)
⊢ b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a})
have rwa : LE.le (α := WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) b : WithZero (Multiplicative ℤ))
  (exp (-(↑(multiplicity v.asIdeal (Ideal.span {a})) : ℤ)) : WithZero (Multiplicative ℤ))
Tactic: rwa [← intValuation_le_pow_iff_mem, ← v.intValuation_eq_exp_neg_multiplicity 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 ℤ))
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 ℤ))
hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ (↑n : ℕ∞)
⊢ ∃ (a_1 : R),
    LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - a_1 * a) : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
have hb : b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a})
Tactic: have hb : b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a}) := by
      rwa [← intValuation_le_pow_iff_mem, ← v.intValuation_eq_exp_neg_multiplicity ha]
-- 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 ℤ))
hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ (↑n : ℕ∞)
hb : b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a})
⊢ Ne (α := Ideal R) (Ideal.span {a}) ⊥
have rwa : ¬Eq (α := Ideal R) (Ideal.span {a}) ⊥
Tactic: rwa [ne_eq, Ideal.span_singleton_eq_bot]
-- 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 ℤ))
hvn : emultiplicity v.asIdeal (Ideal.span {a}) ≤ (↑n : ℕ∞)
hb : b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a})
⊢ ∃ (a_1 : R),
    LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (b - a_1 * a) : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ))
have hnz : Ne (α := Ideal R) (Ideal.span {a}) ⊥
Tactic: have hnz : Ideal.span {a} ≠ ⊥ := by rwa [ne_eq, Ideal.span_singleton_eq_bot]
-- 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 ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
⊢ ∃ (a : R),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
      (↑γ : WithZero (Multiplicative ℤ))
have obtain : ∀ (n d : R) (hd : d ∈ v.asIdeal.primeCompl)
  (hnd :
    HMul.hMul (β := K) x
        ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd) : R) : K) =
      (algebraMap R K : (a : R) → K) n),
  ∃ (a : R),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
      (↑γ : WithZero (Multiplicative ℤ))
Tactic: obtain ⟨n, ⟨d, hd⟩, hnd⟩ := exists_primeCompl_mul_eq_of_integer v x hv
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
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 ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd : d ∈ v.asIdeal.primeCompl
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd) : R) : K) =
    (algebraMap R K : (a : R) → K) n
⊢ ∃ (a : R),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
      (↑γ : WithZero (Multiplicative ℤ))
have hd₁ : Eq (α := WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: rw [← intValuation_eq_one_iff_mem_primeCompl] at hd
Cleared hypotheses: 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 ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
have grw : LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
Tactic: grw [v.intValuation_le_one n, hd]
-- 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 ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
grw :
  LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
have grw₁ : LE.le (α := WithZero (Multiplicative ℤ)) 1 1
Tactic: grw [v.intValuation_le_one n, hd]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
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 ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
⊢ ∃ (a : R),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
      (↑γ : WithZero (Multiplicative ℤ))
have hd' : LE.le (α := WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
Tactic: have hd' : v.intValuation n ≤ v.intValuation d := by grw [v.intValuation_le_one n, hd]
-- 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 ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
hd' :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
⊢ ∃ (a : R),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
      (↑γ : WithZero (Multiplicative ℤ))
have obtain : ∀ (a : R)
  (hval :
    LT.lt (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) : WithZero (Multiplicative ℤ))
      ((↑((unitsWithZeroEquiv : (a : (WithZero (Multiplicative ℤ))ˣ) → Multiplicative ℤ) γ) :
          WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))),
  ∃ (a : R),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
      (↑γ : WithZero (Multiplicative ℤ))
Tactic: obtain ⟨a, hval⟩ := exists_intValuation_mul_sub_lt v hd' (WithZero.unitsWithZeroEquiv γ)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
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 ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
hd' :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
a : R
hval :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) : WithZero (Multiplicative ℤ))
    ((↑((unitsWithZeroEquiv : (a : (WithZero (Multiplicative ℤ))ˣ) → Multiplicative ℤ) γ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
⊢ ∃ (a : R),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
      (↑γ : WithZero (Multiplicative ℤ))
have hval₁ : (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) < (↑γ : WithZero (Multiplicative ℤ))
Tactic: rw [unitsWithZeroEquiv_apply, coe_unzero] at hval
Cleared hypotheses: hval
-- 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 ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
hd' :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
a : R
hval : (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) < (↑γ : WithZero (Multiplicative ℤ))
⊢ ∃ (a : R),
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
      (↑γ : WithZero (Multiplicative ℤ))
have h : ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
    (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
  (↑γ : WithZero (Multiplicative ℤ))
Tactic: use a
-- 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 ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
hd' :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
a : R
hval : (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) < (↑γ : WithZero (Multiplicative ℤ))
⊢ ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) <
    (↑γ : WithZero (Multiplicative ℤ))
have h : Eq (α := WithZero (Multiplicative ℤ))
  (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
    WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) : WithZero (Multiplicative ℤ))
Tactic: suffices h : v.valuation K (algebraMap R K a - x) = v.intValuation (n - a * d) by rwa [h]
-- 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 ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
hd' :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
a : R
hval : (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) < (↑γ : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
      WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) : WithZero (Multiplicative ℤ))
have h : Eq (α := WithZero (Multiplicative ℤ))
  (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
    WithZero (Multiplicative ℤ))
  (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (↑(n - a * d) : K) :
    WithZero (Multiplicative ℤ))
Tactic: rw [← valuation_of_algebraMap (K := K), Algebra.cast, map_sub _ n, map_mul, ← hnd, ← sub_mul,
    map_mul, valuation_of_algebraMap, hd, mul_one, Valuation.map_sub_swap]