awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
neg :
  (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 ℤ))
      (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₁ :
  (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 ℤ))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {y})))) : ℤ)))
neg₂ :
  exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) : ℤ)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x})))) : ℤ)))
      (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})))) : ℤ)))
have neg₃ : exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {x * y})))) : ℤ)) =
  exp
    (HAdd.hAdd (α := ℤ)
      (-(↑(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})))) : ℤ)))
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
⊢ v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y
have 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})))) : ℤ)))
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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
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})))) : ℤ)))
⊢ v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y
have 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})))) : ℤ)))
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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
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})))) :
                ℤ)))
⊢ v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y
have 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})))) : ℤ)))
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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
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
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
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
⊢ LE.le (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑c : ℤ)) : Multiplicative ℤ)
      (max ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑a : ℤ))) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑b : ℤ))) :
        Multiplicative ℤ) ↔
    min a b ≤ c
have rw₁ : LE.le (α := ℤ) (-(↑c : ℤ)) (-(↑a : ℤ)) ∨
    LE.le (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑c : ℤ)) : Multiplicative ℤ)
      ((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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
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
⊢ LE.le (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑c : ℤ)) : Multiplicative ℤ)
      (max ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑a : ℤ))) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑b : ℤ))) :
        Multiplicative ℤ) ↔
    min a b ≤ c
have rw₂ : LE.le (α := ℤ) (-(↑c : ℤ)) (-(↑a : ℤ)) ∨ LE.le (α := ℤ) (-(↑c : ℤ)) (-(↑b : ℤ)) ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
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
⊢ LE.le (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑c : ℤ)) : Multiplicative ℤ)
      (max ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑a : ℤ))) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑b : ℤ))) :
        Multiplicative ℤ) ↔
    min a b ≤ c
have rw₃ : LE.le (α := ℤ) (↑a : ℤ) (↑c : ℤ) ∨ LE.le (α := ℤ) (-(↑c : ℤ)) (-(↑b : ℤ)) ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
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
⊢ LE.le (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑c : ℤ)) : Multiplicative ℤ)
      (max ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑a : ℤ))) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑b : ℤ))) :
        Multiplicative ℤ) ↔
    min a b ≤ c
have rw₄ : LE.le (α := ℤ) (↑a : ℤ) (↑c : ℤ) ∨ LE.le (α := ℤ) (↑b : ℤ) (↑c : ℤ) ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
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
⊢ LE.le (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑c : ℤ)) : Multiplicative ℤ)
      (max ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑a : ℤ))) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑b : ℤ))) :
        Multiplicative ℤ) ↔
    min a b ≤ c
have rw₅ : a ≤ c ∨ LE.le (α := ℤ) (↑b : ℤ) (↑c : ℤ) ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
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
⊢ LE.le (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑c : ℤ)) : Multiplicative ℤ)
      (max ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑a : ℤ))) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑b : ℤ))) :
        Multiplicative ℤ) ↔
    min a b ≤ c
have rw₆ : a ≤ c ∨ b ≤ c ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
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
⊢ LE.le (α := Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑c : ℤ)) : Multiplicative ℤ)
      (max ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑a : ℤ))) ((ofAdd : (a : ℤ) → Multiplicative ℤ) (-(↑b : ℤ))) :
        Multiplicative ℤ) ↔
    min a b ≤ c
have rw₇ : min a b ≤ c ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
have pos : ∀ (hx : x = 0), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
pos : ∀ (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)
have neg : ∀ (hx : ¬x = 0), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
have pos : v.intValuationDef y ≤ max (v.intValuationDef 0) (v.intValuationDef y)
Tactic: rw [hx, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
⊢ v.intValuationDef y ≤ max (v.intValuationDef 0) (v.intValuationDef y)
have pos : ¬v.intValuationDef y ≤ max (v.intValuationDef 0) (v.intValuationDef y) → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
pos pos₁ pos₂ pos₃ : ¬v.intValuationDef y ≤ max (v.intValuationDef 0) (v.intValuationDef y) → False
⊢ v.intValuationDef y ≤ max (v.intValuationDef 0) (v.intValuationDef y)
have pos₄ : max (v.intValuationDef 0) (v.intValuationDef y) < v.intValuationDef y → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
have pos : ∀ (hy : y = 0), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
pos : ∀ (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)
have neg : ∀ (hy : ¬y = 0), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
have pos : v.intValuationDef x ≤ max (v.intValuationDef x) (v.intValuationDef 0)
Tactic: rw [hy, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
⊢ v.intValuationDef x ≤ max (v.intValuationDef x) (v.intValuationDef 0)
have pos : ¬v.intValuationDef x ≤ max (v.intValuationDef x) (v.intValuationDef 0) → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : y = 0
pos pos₁ pos₂ pos₃ : ¬v.intValuationDef x ≤ max (v.intValuationDef x) (v.intValuationDef 0) → False
⊢ v.intValuationDef x ≤ max (v.intValuationDef x) (v.intValuationDef 0)
have pos₄ : max (v.intValuationDef x) (v.intValuationDef 0) < v.intValuationDef x → False
Tactic: order
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
have pos : ∀ (hxy : x + y = 0), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
Tactic: by_cases hxy : x + y = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
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)
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
have neg : ∀ (hxy : ¬x + y = 0), v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
Tactic: by_cases hxy : x + y = 0