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
r : R
n : ℕ
hr : ¬r = 0
neg :
  LE.le (α := WithZero (Multiplicative ℤ))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ)))
      (exp (-(↑n : ℤ))) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₁ :
  LE.le (α := ℤ)
      (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ))
      (-(↑n : ℤ)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₂ :
  LE.le (α := ℤ) (↑n : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
have neg₃ : n ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))) ↔
  v.asIdeal ^ n ∣ Ideal.span {r}
Tactic: rw [v.intValuation_if_neg hr, exp_le_exp, neg_le_neg_iff, Int.ofNat_le,
      Ideal.dvd_span_singleton, ← Associates.le_singleton_iff,
      Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hr) v.associates_irreducible]
-- 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
r : R
n : ℕ
hr : ¬r = 0
neg :
  LE.le (α := WithZero (Multiplicative ℤ))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ)))
      (exp (-(↑n : ℤ))) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₁ :
  LE.le (α := ℤ)
      (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ))
      (-(↑n : ℤ)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₂ :
  LE.le (α := ℤ) (↑n : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₃ :
  n ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
have neg₄ : n ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))) ↔ r ∈ v.asIdeal ^ n
Tactic: rw [v.intValuation_if_neg hr, exp_le_exp, neg_le_neg_iff, Int.ofNat_le,
      Ideal.dvd_span_singleton, ← Associates.le_singleton_iff,
      Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hr) v.associates_irreducible]
-- 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
r : R
n : ℕ
hr : ¬r = 0
neg :
  LE.le (α := WithZero (Multiplicative ℤ))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ)))
      (exp (-(↑n : ℤ))) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₁ :
  LE.le (α := ℤ)
      (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ))
      (-(↑n : ℤ)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₂ :
  LE.le (α := ℤ) (↑n : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₃ :
  n ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₄ :
  n ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))) ↔
    r ∈ v.asIdeal ^ n
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
have neg₅ : n ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))) ↔
  HPow.hPow (α := Associates (Ideal R)) (Associates.mk v.asIdeal) n ≤ Associates.mk (Ideal.span {r})
Tactic: rw [v.intValuation_if_neg hr, exp_le_exp, neg_le_neg_iff, Int.ofNat_le,
      Ideal.dvd_span_singleton, ← Associates.le_singleton_iff,
      Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hr) v.associates_irreducible]
-- 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
r : R
n : ℕ
hr : ¬r = 0
neg :
  LE.le (α := WithZero (Multiplicative ℤ))
      (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ)))
      (exp (-(↑n : ℤ))) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₁ :
  LE.le (α := ℤ)
      (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ))
      (-(↑n : ℤ)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₂ :
  LE.le (α := ℤ) (↑n : ℤ)
      (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₃ :
  n ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
neg₄ :
  n ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))) ↔
    r ∈ v.asIdeal ^ n
neg₅ :
  n ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))) ↔
    HPow.hPow (α := Associates (Ideal R)) (Associates.mk v.asIdeal) n ≤ Associates.mk (Ideal.span {r})
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
have neg₆ : n ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r}))) ↔
  n ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))
Tactic: rw [v.intValuation_if_neg hr, exp_le_exp, neg_le_neg_iff, Int.ofNat_le,
      Ideal.dvd_span_singleton, ← Associates.le_singleton_iff,
      Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hr) v.associates_irreducible]
-- 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
r : R
n : ℕ
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
have pos : ∀ (hr : r = 0),
  LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
Tactic: classical
  by_cases hr : r = 0
  · simp_rw [hr, Valuation.map_zero, Ideal.dvd_span_singleton, zero_le', Submodule.zero_mem]
  · rw [v.intValuation_if_neg hr, exp_le_exp, neg_le_neg_iff, Int.ofNat_le,
      Ideal.dvd_span_singleton, ← Associates.le_singleton_iff,
      Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hr) v.associates_irreducible]
-- 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
r : R
n : ℕ
pos :
  ∀ (hr : r = 0),
    LE.le (α := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
        (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
      v.asIdeal ^ n ∣ Ideal.span {r}
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
have neg : ∀ (hr : ¬r = 0),
  LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}
Tactic: classical
  by_cases hr : r = 0
  · simp_rw [hr, Valuation.map_zero, Ideal.dvd_span_singleton, zero_le', Submodule.zero_mem]
  · rw [v.intValuation_if_neg hr, exp_le_exp, neg_le_neg_iff, Int.ofNat_le,
      Ideal.dvd_span_singleton, ← Associates.le_singleton_iff,
      Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hr) v.associates_irreducible]
-- 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
r : R
n : ℕ
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    r ∈ v.asIdeal ^ n
have rw : v.asIdeal ^ n ∣ Ideal.span {r} ↔ r ∈ v.asIdeal ^ n
Tactic: rw [intValuation_le_pow_iff_dvd, Ideal.dvd_span_singleton]
-- 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
r : R
n : ℕ
rw : v.asIdeal ^ n ∣ Ideal.span {r} ↔ r ∈ v.asIdeal ^ n
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    r ∈ v.asIdeal ^ n
have rw₁ : r ∈ v.asIdeal ^ n ↔ r ∈ v.asIdeal ^ n
Tactic: rw [intValuation_le_pow_iff_dvd, Ideal.dvd_span_singleton]
-- 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
r : R
n : ℕ
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    (↑n : ℕ∞) ≤ emultiplicity v.asIdeal (Ideal.span {r})
have rw : v.asIdeal ^ n ∣ Ideal.span {r} ↔ (↑n : ℕ∞) ≤ emultiplicity v.asIdeal (Ideal.span {r})
Tactic: rw [intValuation_le_pow_iff_dvd, pow_dvd_iff_le_emultiplicity]
-- 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
r : R
n : ℕ
rw : v.asIdeal ^ n ∣ Ideal.span {r} ↔ (↑n : ℕ∞) ≤ emultiplicity v.asIdeal (Ideal.span {r})
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (exp (-(↑n : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    (↑n : ℕ∞) ≤ emultiplicity v.asIdeal (Ideal.span {r})
have rw₁ : (↑n : ℕ∞) ≤ emultiplicity v.asIdeal (Ideal.span {r}) ↔ (↑n : ℕ∞) ≤ emultiplicity v.asIdeal (Ideal.span {r})
Tactic: rw [intValuation_le_pow_iff_dvd, pow_dvd_iff_le_emultiplicity]
-- 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
r : R
n : ℕ
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r) ↔
    emultiplicity v.asIdeal (Ideal.span {r}) ≤ (↑n : ℕ∞)
have rw : LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r) ↔
  exp (-(↑n : ℤ)) <
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ)) (exp 1)
Tactic: rw [← ENat.lt_coe_add_one_iff, ← ENat.coe_one, ← ENat.coe_add, emultiplicity_lt_iff_not_dvd,
    ← intValuation_le_pow_iff_dvd, not_le, Nat.cast_add, Nat.cast_one, neg_add, exp_add,
    exp_neg 1, mul_inv_lt_iff₀ (by simp)]
-- 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
r : R
n : ℕ
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r) ↔
    exp (-(↑n : ℤ)) <
      HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ)) (exp 1)
have pos : ∀
  (hv :
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))),
  LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r) ↔
    exp (-(↑n : ℤ)) <
      HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ)) (exp 1)
Tactic: by_cases hv : v.intValuation r = 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
r : R
n : ℕ
pos :
  ∀
    (hv :
      Eq (α := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
        (0 : WithZero (Multiplicative ℤ))),
    LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r) ↔
      exp (-(↑n : ℤ)) <
        HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
          ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ)) (exp 1)
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r) ↔
    exp (-(↑n : ℤ)) <
      HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ)) (exp 1)
have neg : ∀
  (hv :
    ¬Eq (α := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
        (0 : WithZero (Multiplicative ℤ))),
  LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r) ↔
    exp (-(↑n : ℤ)) <
      HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ)) (exp 1)
Tactic: by_cases hv : v.intValuation r = 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
r : R
n : ℕ
hv :
  ¬Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r) ↔
    exp (-(↑n : ℤ)) <
      HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ)) (exp 1)
have neg : LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r) ↔
  LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑n : ℤ)))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) r)
Tactic: rw [lt_mul_exp_iff_le hv]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
have hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
Tactic: have hv : Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible
-- 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
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
⊢ HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
have rw : DvdNotUnit v.asIdeal (HPow.hPow (β := ℕ) v.asIdeal 2)
Tactic: rw [← Ideal.dvdNotUnit_iff_lt]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
⊢ ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
have hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
Tactic: have hlt : v.asIdeal ^ 2 < v.asIdeal := by
    rw [← Ideal.dvdNotUnit_iff_lt]
    exact ⟨v.ne_bot, v.asIdeal, Ideal.isUnit_iff.not.mpr v.isPrime.ne_top, sq v.asIdeal⟩
-- 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
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
⊢ ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
have obtain : ∀ (π : R) (mem : π ∈ v.asIdeal) (notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2),
  ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
Tactic: obtain ⟨π, mem, notMem⟩ := SetLike.exists_of_lt hlt
-- 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
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2
⊢ Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0
have rw : π ≠ 0
Tactic: rw [Associates.mk_ne_zero']
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2
h : π = 0
⊢ False
have notMem₁ : 0 ∉ HPow.hPow (β := ℕ) v.asIdeal 2
Tactic: rw [h] at notMem
Cleared hypotheses: notMem, h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2
⊢ ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
have hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0
Tactic: have hπ : Associates.mk (Ideal.span {π}) ≠ 0 := by
    rw [Associates.mk_ne_zero']
    intro h
    rw [h] at notMem
    exact notMem (Submodule.zero_mem (v.asIdeal ^ 2))
-- 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
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2
hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0
⊢ ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))
have h : Eq (α := WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
  (exp (-1) : WithZero (Multiplicative ℤ))
Tactic: use π
-- 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
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2
hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
have h : Eq (α := ℤ) (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π})))) : ℤ))
  (-1)
Tactic: rw [intValuation_if_neg _ (Associates.mk_ne_zero'.mp hπ), exp_inj]
-- 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
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2
hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0
⊢ Eq (α := ℤ)
    (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π})))) : ℤ)) (-1)
have h : Eq (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π})))) : ℤ) 1
Tactic: apply congr_arg
-- 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
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2
hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0
⊢ Eq (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π})))) : ℤ)
    1
have h : Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) = 1
Tactic: rw [← Int.ofNat_one, Int.natCast_inj]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal)
hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ HPow.hPow (β := ℕ) v.asIdeal 2
hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0
⊢ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) = 1
have mem₁ : LE.le (α := Associates (Ideal R)) (Associates.mk v.asIdeal) (Associates.mk (Ideal.span {π}))
Tactic: rw [← Ideal.dvd_span_singleton, ← Associates.mk_le_mk_iff_dvd] at mem notMem
Cleared hypotheses: mem, notMem, hπ