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
n d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
h :
  ∀ (v : HeightOneSpectrum R),
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (IsLocalization.mk' K n
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d
              hd)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
hx :
  HMul.hMul (β := K)
      (IsLocalization.mk' K n
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd))
      ((algebraMap R K : (a : R) → K)
          (↑(n,
                  Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x)
                    d hd).2 :
            R) :
        K) =
    (algebraMap R K : (a : R) → K)
      (n, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd).1
hn0 : n ≠ 0
hd0 : d ≠ 0
⊢ Dvd.dvd (α := Ideal R) (Ideal.span {d}) (Ideal.span {n})
have inr : ∀ (ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥),
  Dvd.dvd (α := Ideal R) (Ideal.span {d}) (Ideal.span {n})
Tactic: classical
  have ine {r : R} : r ≠ 0 → Ideal.span {r} ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp
  rw [← Associates.mk_le_mk_iff_dvd, ← Associates.factors_le, Associates.factors_mk _ (ine hn0),
    Associates.factors_mk _ (ine hd0), WithTop.coe_le_coe, Multiset.le_iff_count]
  rintro ⟨v, hv⟩
  obtain ⟨v, rfl⟩ := Associates.mk_surjective v
  have hv' := hv
  rw [Associates.irreducible_mk, irreducible_iff_prime] at hv
  specialize h ⟨v, Ideal.isPrime_of_prime hv, hv.ne_zero⟩
  simp_rw [valuation_of_mk', intValuation_if_neg _ hn0, intValuation_if_neg _ hd0, ← exp_sub,
    ← exp_zero, exp_le_exp, Associates.factors_mk _ (ine hn0),
    Associates.factors_mk _ (ine hd0), Associates.count_some hv'] at h
  simpa using 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
n d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
h :
  ∀ (v : HeightOneSpectrum R),
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (IsLocalization.mk' K n
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d
              hd)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
hx :
  HMul.hMul (β := K)
      (IsLocalization.mk' K n
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd))
      ((algebraMap R K : (a : R) → K)
          (↑(n,
                  Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x)
                    d hd).2 :
            R) :
        K) =
    (algebraMap R K : (a : R) → K)
      (n, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd).1
hn0 : n ≠ 0
hd0 : d ≠ 0
inr inr₁ inr₂ :
  ∀ (ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥),
    Dvd.dvd (α := Ideal R) (Ideal.span {d}) (Ideal.span {n})
⊢ Dvd.dvd (α := Ideal R) (Ideal.span {d}) (Ideal.span {n})
have inr₃ : ∀ (ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥) (a : { a : Associates (Ideal R) // Irreducible a }),
  Multiset.count a (Associates.factors' (Ideal.span {d})) ≤ Multiset.count a (Associates.factors' (Ideal.span {n}))
Tactic: classical
  have ine {r : R} : r ≠ 0 → Ideal.span {r} ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp
  rw [← Associates.mk_le_mk_iff_dvd, ← Associates.factors_le, Associates.factors_mk _ (ine hn0),
    Associates.factors_mk _ (ine hd0), WithTop.coe_le_coe, Multiset.le_iff_count]
  rintro ⟨v, hv⟩
  obtain ⟨v, rfl⟩ := Associates.mk_surjective v
  have hv' := hv
  rw [Associates.irreducible_mk, irreducible_iff_prime] at hv
  specialize h ⟨v, Ideal.isPrime_of_prime hv, hv.ne_zero⟩
  simp_rw [valuation_of_mk', intValuation_if_neg _ hn0, intValuation_if_neg _ hd0, ← exp_sub,
    ← exp_zero, exp_le_exp, Associates.factors_mk _ (ine hn0),
    Associates.factors_mk _ (ine hd0), Associates.count_some hv'] at h
  simpa using 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
n d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
h :
  ∀ (v : HeightOneSpectrum R),
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (IsLocalization.mk' K n
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d
              hd)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
hx :
  HMul.hMul (β := K)
      (IsLocalization.mk' K n
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd))
      ((algebraMap R K : (a : R) → K)
          (↑(n,
                  Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x)
                    d hd).2 :
            R) :
        K) =
    (algebraMap R K : (a : R) → K)
      (n, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd).1
hn0 : n ≠ 0
hd0 : d ≠ 0
inr inr₁ inr₂ :
  ∀ (ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥),
    Dvd.dvd (α := Ideal R) (Ideal.span {d}) (Ideal.span {n})
inr₃ :
  ∀ (ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥) (a : { a : Associates (Ideal R) // Irreducible a }),
    Multiset.count a (Associates.factors' (Ideal.span {d})) ≤ Multiset.count a (Associates.factors' (Ideal.span {n}))
⊢ Dvd.dvd (α := Ideal R) (Ideal.span {d}) (Ideal.span {n})
have inr₄ : ∀ (ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥) (v : Associates (Ideal R)) (hv : Irreducible v),
  Multiset.count (Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) v hv)
      (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count (Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) v hv)
      (Associates.factors' (Ideal.span {n}))
Tactic: classical
  have ine {r : R} : r ≠ 0 → Ideal.span {r} ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp
  rw [← Associates.mk_le_mk_iff_dvd, ← Associates.factors_le, Associates.factors_mk _ (ine hn0),
    Associates.factors_mk _ (ine hd0), WithTop.coe_le_coe, Multiset.le_iff_count]
  rintro ⟨v, hv⟩
  obtain ⟨v, rfl⟩ := Associates.mk_surjective v
  have hv' := hv
  rw [Associates.irreducible_mk, irreducible_iff_prime] at hv
  specialize h ⟨v, Ideal.isPrime_of_prime hv, hv.ne_zero⟩
  simp_rw [valuation_of_mk', intValuation_if_neg _ hn0, intValuation_if_neg _ hd0, ← exp_sub,
    ← exp_zero, exp_le_exp, Associates.factors_mk _ (ine hn0),
    Associates.factors_mk _ (ine hd0), Associates.count_some hv'] at h
  simpa using 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
a s : R
hs : s ∈ v.asIdeal.primeCompl
this :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (↑a : K) (↑s : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ Membership.mem (γ := ValuationSubring K) (Valuation.valuationSubring (valuation K v))
    (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) (((algebraMap R K : (a : R) → K) s)⁻¹ : K))
have rwa : ∀
  (this :
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (HMul.hMul (α := K) (↑a : K) (↑s : K)⁻¹) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))),
  Membership.mem (γ := ValuationSubring K) (Valuation.valuationSubring (valuation K v))
    (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) (((algebraMap R K : (a : R) → K) s)⁻¹ : K))
Tactic: rwa [division_def (a : K) s] at this
Cleared hypotheses: this
-- 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
a s : R
hs : s ∈ v.asIdeal.primeCompl
⊢ Membership.mem (γ := ValuationSubring K) (Valuation.valuationSubring (valuation K v))
    (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) (((algebraMap R K : (a : R) → K) s)⁻¹ : K))
have suffices : LE.le (α := WithZero (Multiplicative ℤ))
  (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (HDiv.hDiv (α := K) (↑a : K) (↑s : K)) :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: suffices (valuation K v) (a / (s : K)) ≤ 1 by rwa [division_def (a : K) s] at this
-- 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
a s : R
hs : s ∈ v.asIdeal.primeCompl
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := K) (↑a : K) (↑s : K)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have rwa : s ∉ v.asIdeal
Tactic: rwa [valuation_div_le_one_iff (K := K) v a (by aesop) (fun _ ↦ by contradiction)]
-- 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
⊢ Ne (α := ValuationSubring K) (Valuation.valuationSubring (valuation K v)) ⊤
have simp : Valuation.IsNontrivial (valuation K v)
Tactic: simp only [ne_eq, Valuation.valuationSubring_eq_top_iff, not_not]
-- 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
⊢ ∃ (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 ∨
      HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
have inl : ∀ (r : ↥(valuationSubringAtPrime K v))
  (hr : (algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K) r = x),
  ∃ (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 ∨
      HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
Tactic: obtain (⟨r, hr⟩ | ⟨r, hr⟩) :=
    ValuationRing.isInteger_or_isInteger (valuationSubringAtPrime K v) x
-- 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
inl :
  ∀ (r : ↥(valuationSubringAtPrime K v))
    (hr : (algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K) r = x),
    ∃ (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 ∨
        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 ∨
      HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
have inr : ∀ (r : ↥(valuationSubringAtPrime K v))
  (hr : (algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K) r = x⁻¹),
  ∃ (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 ∨
      HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
Tactic: obtain (⟨r, hr⟩ | ⟨r, hr⟩) :=
    ValuationRing.isInteger_or_isInteger (valuationSubringAtPrime K v) x
-- 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
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K) r = x
⊢ ∃ (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 ∨
      HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
have inl : ∀ (n : R) (d : ↥v.asIdeal.primeCompl)
  (hnd :
    HMul.hMul (β := ↥(valuationSubringAtPrime K v)) r
        ((algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (↑(n, d).2 : R) :
          ↥(valuationSubringAtPrime K v)) =
      (algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (n, d).1),
  ∃ (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 ∨
      HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
Tactic: obtain ⟨⟨n, d⟩, hnd⟩ := IsLocalization.surj v.asIdeal.primeCompl r
-- 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
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K) r = x⁻¹
⊢ ∃ (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 ∨
      HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
have inr : ∀ (n : R) (d : ↥v.asIdeal.primeCompl)
  (hnd :
    HMul.hMul (β := ↥(valuationSubringAtPrime K v)) r
        ((algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (↑(n, d).2 : R) :
          ↥(valuationSubringAtPrime K v)) =
      (algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (n, d).1),
  ∃ (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 ∨
      HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
Tactic: obtain ⟨⟨n, d⟩, hnd⟩ := IsLocalization.surj v.asIdeal.primeCompl r
-- 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
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K) r = x
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  HMul.hMul (β := ↥(valuationSubringAtPrime K v)) r
      ((algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (↑(n, d).2 : R) :
        ↥(valuationSubringAtPrime K v)) =
    (algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ ∃ (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 ∨
      HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
have h : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) (↑d : R) : K) = (algebraMap R K : (a : R) → K) n ∨
  HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
Tactic: use n, d
-- 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
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K) r = x⁻¹
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  HMul.hMul (β := ↥(valuationSubringAtPrime K v)) r
      ((algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (↑(n, d).2 : R) :
        ↥(valuationSubringAtPrime K v)) =
    (algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ ∃ (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 ∨
      HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
have h : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) (↑d : R) : K) = (algebraMap R K : (a : R) → K) n ∨
  HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
Tactic: use n, d
-- 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
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K) r = x
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  HMul.hMul (β := ↥(valuationSubringAtPrime K v)) r
      ((algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (↑(n, d).2 : R) :
        ↥(valuationSubringAtPrime K v)) =
    (algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) (↑d : R) : K) = (algebraMap R K : (a : R) → K) n ∨
    HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
have hnd₁ : Eq (α := K)
  ((algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K)
      (HMul.hMul (β := ↥(valuationSubringAtPrime K v)) r
        ((algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (↑(n, d).2 : R) :
          ↥(valuationSubringAtPrime K v))) :
    K)
  ((algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K)
      ((algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (n, d).1 :
        ↥(valuationSubringAtPrime K v)) :
    K)
Tactic: apply_fun algebraMap _ K at hnd
Cleared hypotheses: hnd
-- 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
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K) r = x⁻¹
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  HMul.hMul (β := ↥(valuationSubringAtPrime K v)) r
      ((algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (↑(n, d).2 : R) :
        ↥(valuationSubringAtPrime K v)) =
    (algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) (↑d : R) : K) = (algebraMap R K : (a : R) → K) n ∨
    HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
have hnd₁ : Eq (α := K)
  ((algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K)
      (HMul.hMul (β := ↥(valuationSubringAtPrime K v)) r
        ((algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (↑(n, d).2 : R) :
          ↥(valuationSubringAtPrime K v))) :
    K)
  ((algebraMap (↥(valuationSubringAtPrime K v)) K : (a : ↥(valuationSubringAtPrime K v)) → K)
      ((algebraMap R ↥(valuationSubringAtPrime K v) : (a : R) → ↥(valuationSubringAtPrime K v)) (n, d).1 :
        ↥(valuationSubringAtPrime K v)) :
    K)
Tactic: apply_fun algebraMap _ K at hnd
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 ℤ))
⊢ ∃ (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 inl : ∀ (n : R) (d : ↥v.asIdeal.primeCompl)
  (hnd : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) (↑d : R) : K) = (algebraMap R K : (a : R) → K) n),
  ∃ (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
Tactic: obtain ⟨n, d, (hnd | hnd)⟩ := exists_primeCompl_mul_eq_or_mul_eq v x
-- 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 ℤ))
inl :
  ∀ (n : R) (d : ↥v.asIdeal.primeCompl)
    (hnd : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) (↑d : R) : K) = (algebraMap R K : (a : R) → K) n),
    ∃ (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
⊢ ∃ (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 : 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
Tactic: obtain ⟨n, d, (hnd | hnd)⟩ := exists_primeCompl_mul_eq_or_mul_eq v x