awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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 ℤ))
rwa rwa₁ rwa₂ 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))
⊢ 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

Premises used: Algebra.cast, division_def
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
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 ℤ))
⊢ 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:
suffices (valuation K v) (a / (s : K)) ≤ 1 by rwa [division_def (a : K) s] at this
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
⊢ s ≠ 0

Tactic:
aesop
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
h : s ∈ v.asIdeal
⊢ a ∉ v.asIdeal

Tactic:
contradiction
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
rwa rwa₁ rwa₂ rwa₃ : s ∉ v.asIdeal
⊢ 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:
rwa [valuation_div_le_one_iff (K := K) v a (by aesop) (fun _ ↦ by contradiction)]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst_2 : Field K
inst_3 : CommSemiring S
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
v : HeightOneSpectrum R
⊢ IsScalarTower R (↥(valuationSubringAtPrime K v)) K

Tactic:
IsScalarTower.of_algebraMap_eq (fun _ ↦ rfl)

Premises used: IsScalarTower.of_algebraMap_eq, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst_2 : Field K
inst_3 : CommSemiring S
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
v : HeightOneSpectrum R
⊢ IsDedekindDomain.{u_2} ↥(valuationSubringAtPrime K v)

Tactic:
IsLocalization.AtPrime.isDedekindDomain R v.asIdeal
    (subalgebra.ofField K _ v.asIdeal.primeCompl_le_nonZeroDivisors)

Premises used: Set.Mem, Localization.subalgebra.ofField, Membership.mem, IsDedekindDomain.HeightOneSpectrum.asIdeal, Subtype, IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime, ValuationSubring.ofSubring, IsLocalization.AtPrime.isDedekindDomain, Ideal.primeCompl_le_nonZeroDivisors, Ideal.primeCompl
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst_2 : Field K
inst_3 : CommSemiring S
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
v : HeightOneSpectrum R
⊢ Ring.KrullDimLE.{u_2} 1 ↥(valuationSubringAtPrime K v)

Tactic:
Ring.KrullDimLE.mk₁' (fun _ a _ ↦ IsPrime.to_maximal_ideal a)

Premises used: Ring.KrullDimLE.mk₁', IsPrime.to_maximal_ideal
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst_2 : Field K
inst_3 : CommSemiring S
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
v : HeightOneSpectrum R
⊢ IsLocalization.{u_1, u_2} v.asIdeal.primeCompl ↥(valuationSubringAtPrime K v)

Tactic:
Localization.subalgebra.isLocalization_ofField K (v.asIdeal.primeCompl) _

Premises used: Set.Mem, IsDedekindDomain.HeightOneSpectrum.asIdeal, Localization.subalgebra.isLocalization_ofField, IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime, ValuationSubring.ofSubring, Ideal.primeCompl
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
simp : Valuation.IsNontrivial (valuation K v)
⊢ Ne (α := ValuationSubring K) (Valuation.valuationSubring (valuation K v)) ⊤

Tactic:
simp only [ne_eq, Valuation.valuationSubring_eq_top_iff, not_not]

Premises used: Classical.not_not, ne_eq, Valuation.valuationSubring_eq_top_iff
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
⊢ Valuation.IsNontrivial (valuation K v)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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)
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)
⊢ ∃ (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

Premises used: Membership.mem, Subtype, IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime, ValuationRing.isInteger_or_isInteger
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
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)
⊢ ∃ (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

Premises used: IsLocalization.surj, IsDedekindDomain.HeightOneSpectrum.asIdeal, Ideal.primeCompl
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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⁻¹
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)
⊢ ∃ (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

Premises used: IsLocalization.surj, IsDedekindDomain.HeightOneSpectrum.asIdeal, Ideal.primeCompl
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
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)
⊢ ∃ (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:
use n, d
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
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)
⊢ ∃ (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:
use n, d
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
⊢ 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

Premises used: Algebra.algebraMap
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
⊢ 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

Premises used: Algebra.algebraMap
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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 :
  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)
⊢ 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:
grind [=_ IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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 :
  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)
⊢ 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:
grind [=_ IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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
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
⊢ ∃ (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

Premises used: IsDedekindDomain.HeightOneSpectrum.exists_primeCompl_mul_eq_or_mul_eq
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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) (↑d : R) : K) = (algebraMap R K : (a : R) → K) n
w : R
w₁ : ↥v.asIdeal.primeCompl
h : 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:
use n, d
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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

Tactic:
⟨d, ⟨n, ?_⟩, hnd⟩

Premises used: Subtype.mk, Exists.intro, Subtype.val
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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 : n ∈ v.asIdeal.primeCompl
⊢ ∃ (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:
refine ⟨d, ⟨n, ?_⟩, hnd⟩
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
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 :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ n ∈ v.asIdeal.primeCompl

Tactic:
rw [← v.intValuation_eq_one_iff_mem_primeCompl]

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff_mem_primeCompl