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
d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
hd0 : d ≠ 0
z : R
h :
  ∀ (v : HeightOneSpectrum R),
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (IsLocalization.mk' K (d * z)
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d
              hd)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
hx :
  IsLocalization.mk' K (d * z)
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd) =
      (algebraMap R K : (a : R) → K) z ∨
    Eq.{u_2 + 1} (α := K)
      ((algebraMap R K : (a : R) → K)
          (↑(d * z,
                  Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x)
                    d hd).2 :
            R) :
        K)
      (0 : K)
hn0 : d * z ≠ 0
this : Dvd.dvd (α := Ideal R) (Ideal.span {d}) (Ideal.span {d * z})
⊢ ((algebraMap R K : R →+* K) : (a : R) → K) z =
    IsLocalization.mk' K (d * z)
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd)

Tactic:
exact (hx.resolve_right fun h => by simp [hd0] at h).symm

Premises used: Or.resolve_right, Eq.symm
-- 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
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 : Dvd.dvd (α := Ideal R) (Ideal.span {d}) (Ideal.span {n})
⊢ Membership.mem (γ := Subring K) (RingHom.range.{u_1, u_2} (R := R) (algebraMap R K))
    (IsLocalization.mk' K n
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd))

Tactic:
suffices Ideal.span {d} ∣ (Ideal.span {n} : Ideal R) by
    obtain ⟨z, rfl⟩ := Ideal.span_singleton_le_span_singleton.1 (Ideal.le_of_dvd this)
    use z
    rw [map_mul, mul_comm, mul_eq_mul_left_iff] at hx
    exact (hx.resolve_right fun h => by simp [hd0] at h).symm
-- 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
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
⊢ ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥

Tactic:
have ine {r : R} : r ≠ 0 → Ideal.span {r} ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp
-- 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
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
ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥
inr :
  ∀ (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})

Tactic:
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]

Premises used: Multiset.le_iff_count, Associates.mk_le_mk_iff_dvd, Associates.factors_mk, Associates.factors_le, WithTop.coe_le_coe
-- 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
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
ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥
v : Associates (Ideal R)
hv : Irreducible v
inr :
  ∀ (v : Ideal R) (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v)),
    Multiset.count (Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v) hv)
        (Associates.factors' (Ideal.span {d})) ≤
      Multiset.count (Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v) hv)
        (Associates.factors' (Ideal.span {n}))
⊢ 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:
obtain ⟨v, rfl⟩ := Associates.mk_surjective v

Premises used: Associates.mk_surjective, rfl
-- 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
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
ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥
v : Ideal R
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v)
⊢ Irreducible (M := Associates (Ideal R)) (Associates.mk v)

Tactic:
have hv' := hv
-- 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
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
ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥
v : Ideal R
hv hv' : Irreducible (M := Associates (Ideal R)) (Associates.mk v)
⊢ Prime v

Tactic:
rw [Associates.irreducible_mk, irreducible_iff_prime] at hv

Premises used: Associates.irreducible_mk, irreducible_iff_prime
-- 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
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
ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥
v : Ideal R
hv hv' : Irreducible (M := Associates (Ideal R)) (Associates.mk v)
hv₁ : Prime v
⊢ Irreducible (M := Associates (Ideal R)) (Associates.mk v)

Tactic:
rw [Associates.irreducible_mk, irreducible_iff_prime] at hv

Premises used: Associates.irreducible_mk, irreducible_iff_prime
-- 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
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
ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥
v : Ideal R
hv_1 : Irreducible (M := Associates (Ideal R)) (Associates.mk v)
hv : Prime v
hv' : Irreducible (M := Associates (Ideal R)) (Associates.mk v)
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K { asIdeal := v, isPrime := ⋯, ne_bot := ⋯ : HeightOneSpectrum R } :
            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 ℤ))

Tactic:
specialize h ⟨v, Ideal.isPrime_of_prime hv, hv.ne_zero⟩

Premises used: IsDedekindDomain.HeightOneSpectrum.mk, Prime.ne_zero, Ideal.isPrime_of_prime
-- 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
n d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
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
ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥
v : Ideal R
hv_1 : Irreducible (M := Associates (Ideal R)) (Associates.mk v)
hv : Prime v
hv' : Irreducible (M := Associates (Ideal R)) (Associates.mk v)
h :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K { asIdeal := v, isPrime := ⋯, ne_bot := ⋯ : HeightOneSpectrum R } :
            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 ℤ))
⊢ HSub.hSub (α := ℤ)
      (-(↑(Multiset.count (Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v) hv')
              (Associates.factors' (Ideal.span {n}))) :
          ℤ))
      (-(↑(Multiset.count (Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v) hv')
              (Associates.factors' (Ideal.span {d}))) :
          ℤ)) ≤
    0

Tactic:
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

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, WithZero.exp_sub, Associates.count_some, Associates.factors_mk, WithZero.exp_le_exp, IsDedekindDomain.HeightOneSpectrum.valuation_of_mk', WithZero.exp_zero
-- 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
n d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
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
ine : ∀ {r : R}, r ≠ 0 → Ne (α := Ideal R) (Ideal.span {r}) ⊥
v : Ideal R
hv_1 : Irreducible (M := Associates (Ideal R)) (Associates.mk v)
hv : Prime v
hv' : Irreducible (M := Associates (Ideal R)) (Associates.mk v)
h :
  HSub.hSub (α := ℤ)
      (-(↑(Multiset.count (Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v) hv')
              (Associates.factors' (Ideal.span {n}))) :
          ℤ))
      (-(↑(Multiset.count (Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v) hv')
              (Associates.factors' (Ideal.span {d}))) :
          ℤ)) ≤
    0
⊢ Multiset.count (Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v) hv_1)
      (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count (Subtype.mk (p := fun (a : Associates (Ideal R)) ↦ Irreducible a) (Associates.mk v) hv_1)
      (Associates.factors' (Ideal.span {n}))

Tactic:
simpa using h
-- 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
p q : HeightOneSpectrum R
hpq : Valuation.IsEquiv (valuation K p) (valuation K q)
⊢ p = q

Tactic:
simp_all [Valuation.isEquiv_iff_val_lt_one, HeightOneSpectrum.ext_iff, Ideal.ext_iff,
    ← valuation_lt_one_iff_mem (K := K)]

Premises used: IsDedekindDomain.HeightOneSpectrum.ext_iff, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, Valuation.isEquiv_iff_val_lt_one, Ideal.ext_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
⊢ IsDedekindDomain.{u_2} ↥(subalgebra.ofField K v.asIdeal.primeCompl ⋯)

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

Premises used: Localization.subalgebra.ofField, Membership.mem, IsDedekindDomain.HeightOneSpectrum.asIdeal, Subtype, 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
⊢ IsLocalRing.{u_2} ↥(subalgebra.ofField K v.asIdeal.primeCompl ⋯)

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

Premises used: Localization.subalgebra.ofField, Membership.mem, IsDedekindDomain.HeightOneSpectrum.asIdeal, Subtype, IsLocalization.AtPrime.isLocalRing, 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
x : K
⊢ Membership.mem (γ := Subring K) (Subalgebra.toSubring (subalgebra.ofField K v.asIdeal.primeCompl ⋯)) x ∨
    Membership.mem (γ := Subring K) (Subalgebra.toSubring (subalgebra.ofField K v.asIdeal.primeCompl ⋯)) x⁻¹

Tactic:
simpa [IsLocalization.IsInteger] using ValuationRing.isInteger_or_isInteger
        (subalgebra.ofField K _ v.asIdeal.primeCompl_le_nonZeroDivisors) x

Premises used: IsLocalization.IsInteger, Localization.subalgebra.ofField, Membership.mem, IsDedekindDomain.HeightOneSpectrum.asIdeal, Subtype, Ideal.primeCompl_le_nonZeroDivisors, Ideal.primeCompl, 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
⊢ Eq (α := Subring K) (ValuationSubring.toSubring (valuationSubringAtPrime K v))
    (Subalgebra.toSubring (subalgebra.ofField K v.asIdeal.primeCompl ⋯))

Tactic:
rfl

Premises used: rfl