awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
pos :
  ∀ (hx : x = 0),
    (if x * y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
              ℤ))) =
      HMul.hMul (α := WithZero (Multiplicative ℤ))
        (if x = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) :
                ℤ)))
        (if y = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) :
                ℤ)))
neg :
  ∀ (hx : ¬x = 0),
    (if x * y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
              ℤ))) =
      HMul.hMul (α := WithZero (Multiplicative ℤ))
        (if x = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) :
                ℤ)))
        (if y = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) :
                ℤ)))
⊢ (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
pos :
  (if 0 * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0 * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if Eq.{u_1 + 1} (α := R) 0 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
pos₁ :
  (if Eq.{u_1 + 1} (α := R) 0 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0})))) : ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if Eq.{u_1 + 1} (α := R) 0 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
pos₂ :
  0 =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) 0
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
pos₃ pos₄ : Eq (α := WithZero (Multiplicative ℤ)) 0 0
⊢ (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))

Tactic:
rw [hx, zero_mul, if_pos rfl, zero_mul]

Premises used: MulZeroClass.zero_mul, if_pos, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
pos :
  ∀ (hy : y = 0),
    (if x * y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
              ℤ))) =
      HMul.hMul (α := WithZero (Multiplicative ℤ))
        (if x = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) :
                ℤ)))
        (if y = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) :
                ℤ)))
neg :
  ∀ (hy : ¬y = 0),
    (if x * y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
              ℤ))) =
      HMul.hMul (α := WithZero (Multiplicative ℤ))
        (if x = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) :
                ℤ)))
        (if y = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) :
                ℤ)))
⊢ (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
pos :
  (if x * 0 = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * 0})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if Eq.{u_1 + 1} (α := R) 0 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0})))) : ℤ)))
pos₁ :
  (if Eq.{u_1 + 1} (α := R) 0 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0})))) : ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if Eq.{u_1 + 1} (α := R) 0 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {0})))) : ℤ)))
pos₂ :
  0 =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      0
pos₃ pos₄ : Eq (α := WithZero (Multiplicative ℤ)) 0 0
⊢ (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))

Tactic:
rw [hy, mul_zero, if_pos rfl, mul_zero]

Premises used: if_pos, MulZeroClass.mul_zero, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
simp :
  (if x * y = 0 then 0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
            ℤ))) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if x = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (if y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
pos :
  ∀ (hx : x = 0),
    (if x * y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
              ℤ))) =
      HMul.hMul (α := WithZero (Multiplicative ℤ))
        (if x = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) :
                ℤ)))
        (if y = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) :
                ℤ)))
neg neg₁ :
  ∀ (hx : ¬x = 0),
    (if x * y = 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) :
              ℤ))) =
      HMul.hMul (α := WithZero (Multiplicative ℤ))
        (if x = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) :
                ℤ)))
        (if y = 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) :
                ℤ)))
⊢ v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y

Tactic:
classical
  simp only [intValuationDef]
  by_cases hx : x = 0
  · rw [hx, zero_mul, if_pos rfl, zero_mul]
  · by_cases hy : y = 0
    · rw [hy, mul_zero, if_pos rfl, mul_zero]
    · rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← exp_add,
        ← Ideal.span_singleton_mul_span_singleton, ← Associates.mk_mul_mk, ← neg_add,
        Associates.count_mul (Associates.mk_ne_zero'.mpr hx) (Associates.mk_ne_zero'.mpr hy)
          v.associates_irreducible,
        Nat.cast_add]

Premises used: WithZero.exp_add, MulZeroClass.zero_mul, IsDedekindDomain.HeightOneSpectrum.intValuationDef, neg_add, if_pos, MulZeroClass.mul_zero, Nat.cast_add, Ideal.span_singleton_mul_span_singleton, Associates.mk_mul_mk, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
a b c : ℕ
rw :
  LE.le (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑c : ℤ)) : Multiplicative ℤ)
        ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑a : ℤ)) : Multiplicative ℤ) ∨
      LE.le (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑c : ℤ)) : Multiplicative ℤ)
        ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑b : ℤ)) : Multiplicative ℤ) ↔
    min a b ≤ c
rw₁ :
  LE.le (α := ℤ) (-(↑c : ℤ)) (-(↑a : ℤ)) ∨
      LE.le (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑c : ℤ)) : Multiplicative ℤ)
        ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑b : ℤ)) : Multiplicative ℤ) ↔
    min a b ≤ c
rw₂ : LE.le (α := ℤ) (-(↑c : ℤ)) (-(↑a : ℤ)) ∨ LE.le (α := ℤ) (-(↑c : ℤ)) (-(↑b : ℤ)) ↔ min a b ≤ c
rw₃ : LE.le (α := ℤ) (↑a : ℤ) (↑c : ℤ) ∨ LE.le (α := ℤ) (-(↑c : ℤ)) (-(↑b : ℤ)) ↔ min a b ≤ c
rw₄ : LE.le (α := ℤ) (↑a : ℤ) (↑c : ℤ) ∨ LE.le (α := ℤ) (↑b : ℤ) (↑c : ℤ) ↔ min a b ≤ c
rw₅ : a ≤ c ∨ LE.le (α := ℤ) (↑b : ℤ) (↑c : ℤ) ↔ min a b ≤ c
rw₆ : a ≤ c ∨ b ≤ c ↔ min a b ≤ c
rw₇ rw₈ : min a b ≤ c ↔ min a b ≤ c
⊢ LE.le (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑c : ℤ)) : Multiplicative ℤ)
      (max ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑a : ℤ))) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑b : ℤ))) :
        Multiplicative ℤ) ↔
    min a b ≤ c

Tactic:
rw [le_max_iff, ofAdd_le, ofAdd_le, neg_le_neg_iff, neg_le_neg_iff, Int.ofNat_le, Int.ofNat_le,
    ← min_le_iff]

Premises used: Multiplicative.ofAdd_le, min_le_iff, Int.ofNat_le, le_max_iff, neg_le_neg_iff
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
pos : ∀ (hx : x = 0), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
neg : ∀ (hx : ¬x = 0), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
pos : v.intValuationDef y ≤ max (v.intValuationDef 0) (v.intValuationDef y)
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
rw [hx, zero_add]

Premises used: zero_add
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
pos pos₁ pos₂ pos₃ : ¬v.intValuationDef y ≤ max (v.intValuationDef 0) (v.intValuationDef y) → False
pos₄ pos₅ pos₆ pos₇ pos₈ pos₉ pos₁₀ pos₁₁ :
  max (v.intValuationDef 0) (v.intValuationDef y) < v.intValuationDef y → False
⊢ v.intValuationDef y ≤ max (v.intValuationDef 0) (v.intValuationDef y)

Tactic:
order
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
pos : ∀ (hy : y = 0), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
neg : ∀ (hy : ¬y = 0), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
pos : v.intValuationDef x ≤ max (v.intValuationDef x) (v.intValuationDef 0)
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
rw [hy, add_zero]

Premises used: add_zero
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
pos pos₁ pos₂ pos₃ : ¬v.intValuationDef x ≤ max (v.intValuationDef x) (v.intValuationDef 0) → False
pos₄ pos₅ pos₆ pos₇ pos₈ pos₉ pos₁₀ pos₁₁ :
  max (v.intValuationDef x) (v.intValuationDef 0) < v.intValuationDef x → False
⊢ v.intValuationDef x ≤ max (v.intValuationDef x) (v.intValuationDef 0)

Tactic:
order
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
pos : ∀ (hxy : x + y = 0), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
neg : ∀ (hxy : ¬x + y = 0), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
by_cases hxy : x + y = 0
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
pos : 0 ≤ max (v.intValuationDef x) (v.intValuationDef y)
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
rw [intValuationDef, if_pos hxy]

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuationDef, if_pos
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ 0 ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
zero_le'

Premises used: zero_le'
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ 0 ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
exact zero_le'

Premises used: zero_le'
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
neg :
  LE.le (α := WithZero (Multiplicative ℤ))
      (exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))) :
            ℤ)))
      (exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ))) ∨
    LE.le (α := WithZero (Multiplicative ℤ))
      (exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))) :
            ℤ)))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
rw [v.intValuationDef_if_neg hxy, v.intValuationDef_if_neg hx, v.intValuationDef_if_neg hy,
          le_max_iff]

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg, le_max_iff
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
neg :
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
      (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) ≤
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))) :
            ℤ)))
      (exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ))) ∨
    LE.le (α := WithZero (Multiplicative ℤ))
      (exp
        (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))) :
            ℤ)))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))

Tactic:
simp only [exp_le_exp, neg_le_neg_iff, Nat.cast_le, ← min_le_iff]

Premises used: min_le_iff, WithZero.exp_le_exp, Nat.cast_le, neg_le_neg_iff
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
neg :
  let nmin :=
    min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
      (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))));
  nmin ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))
⊢ min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
      (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) ≤
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x + y})))

Tactic:
set nmin :=
          min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
            ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)

Premises used: Associates.mk, Associates.count, IsDedekindDomain.HeightOneSpectrum.asIdeal, Ideal.span, Associates.factors, Singleton.singleton, Min.min
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
rw : nmin ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))
rw₁ : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
⊢ x ∈ v.asIdeal ^ nmin

Tactic:
rw [← Associates.le_singleton_iff x nmin _,
            Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hx) _]

Premises used: Iff.mpr, Associates.prime_pow_dvd_iff_le, Associates.le_singleton_iff, Associates.mk_ne_zero'
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
⊢ nmin ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))

Tactic:
min_le_left _ _

Premises used: min_le_left
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
⊢ nmin ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))

Tactic:
exact min_le_left _ _

Premises used: min_le_left
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
⊢ Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)

Tactic:
v.associates_irreducible

Premises used: IsDedekindDomain.HeightOneSpectrum.associates_irreducible
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x}))))
    (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y}))))
⊢ Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)

Tactic:
exact v.associates_irreducible

Premises used: IsDedekindDomain.HeightOneSpectrum.associates_irreducible