-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem intValuation_lt_one_iff_dvd (r : R) :
    v.intValuationDef r < 1 ↔ v.asIdeal ∣ Ideal.span {r}

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))) < 1 ↔
    v.asIdeal ∣ Ideal.span {r}

Tactic:
rw [← WithZero.coe_one, ← ofAdd_zero, WithZero.coe_lt_coe, ofAdd_lt, neg_lt_zero, ←
  Int.ofNat_zero, Int.ofNat_lt, zero_lt_iff]

Result:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors ≠ 0 ↔ v.asIdeal ∣ Ideal.span {r}

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
h : Ideal.span {r} ≠ 0
⊢ Irreducible v.asIdeal

Tactic:
apply v.irreducible

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r = 0
⊢ 0 < 1 ↔ v.asIdeal ∣ Ideal.span {r}

Tactic:
simp [hr]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
⊢ v.intValuationDef r < 1 ↔ v.asIdeal ∣ Ideal.span {r}

Tactic:
rw [intValuationDef]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
⊢ (if r = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors)))) < 1 ↔
    v.asIdeal ∣ Ideal.span {r}

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors ≠ 0 ↔ v.asIdeal ∣ Ideal.span {r}

Tactic:
have h : (Ideal.span {r} : Ideal R) ≠ 0 := by
  rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
  exact hr

Result:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
h : Ideal.span {r} ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors ≠ 0 ↔ v.asIdeal ∣ Ideal.span {r}

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
⊢ (if r = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors)))) < 1 ↔
    v.asIdeal ∣ Ideal.span {r}

Tactic:
split_ifs with hr

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r = 0
⊢ 0 < 1 ↔ v.asIdeal ∣ Ideal.span {r}

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors))) < 1 ↔
    v.asIdeal ∣ Ideal.span {r}

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
h : Ideal.span {r} ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors ≠ 0 ↔ v.asIdeal ∣ Ideal.span {r}

Tactic:
apply Associates.count_ne_zero_iff_dvd h (by apply v.irreducible)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ Ideal.span {r} ≠ 0

Tactic:
rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ ¬r = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ ¬r = 0

Tactic:
exact hr

Result:
no goals