-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem intValuation_exists_uniformizer :
    ∃ π : R, v.intValuationDef π = Multiplicative.ofAdd (-1 : ℤ)

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : π ∉ v.asIdeal ^ 2
⊢ ∃ π, v.intValuationDef π = ↑(ofAdd (-1))

Tactic:
have hπ : Associates.mk (Ideal.span {π}) ≠ 0 := by
  rw [Associates.mk_ne_zero']
  intro h
  rw [h] at nmem
  exact nmem (Submodule.zero_mem (v.asIdeal ^ 2))

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ ∃ π, v.intValuationDef π = ↑(ofAdd (-1))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
⊢ DvdNotUnit v.asIdeal (v.asIdeal ^ 2)

Tactic:
exact
  ⟨v.ne_bot, v.asIdeal, (not_congr Ideal.isUnit_iff).mpr (Ideal.IsPrime.ne_top v.isPrime),
    sq v.asIdeal⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ ∃ π, v.intValuationDef π = ↑(ofAdd (-1))

Tactic:
classical
have hv : _root_.Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible
have hlt : v.asIdeal ^ 2 < v.asIdeal := by
  rw [← Ideal.dvdNotUnit_iff_lt]
  exact
    ⟨v.ne_bot, v.asIdeal, (not_congr Ideal.isUnit_iff).mpr (Ideal.IsPrime.ne_top v.isPrime),
      sq v.asIdeal⟩
obtain ⟨π, mem, nmem⟩ := SetLike.exists_of_lt hlt
have hπ : Associates.mk (Ideal.span {π}) ≠ 0 := by
  rw [Associates.mk_ne_zero']
  intro h
  rw [h] at nmem
  exact nmem (Submodule.zero_mem (v.asIdeal ^ 2))
use π
rw [intValuationDef, if_neg (Associates.mk_ne_zero'.mp hπ), WithZero.coe_inj]
apply congr_arg
rw [neg_inj, ← Int.ofNat_one, Int.natCast_inj]
rw [← Ideal.dvd_span_singleton, ← Associates.mk_le_mk_iff_dvd] at mem nmem
rw [← pow_one (Associates.mk v.asIdeal), Associates.prime_pow_dvd_iff_le hπ hv] at mem
rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le hπ hv, not_le] at nmem
exact Nat.eq_of_le_of_lt_succ mem nmem

Result:
no goals

Proof state:
case h.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : 1 ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors
nmem : ¬Associates.mk (v.asIdeal ^ 2) ≤ Associates.mk (Ideal.span {π})
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1

Tactic:
rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le hπ hv, not_le] at nmem

Result:
case h.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : 1 ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors
nmem : (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors < 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
⊢ ∃ π, v.intValuationDef π = ↑(ofAdd (-1))

Tactic:
obtain ⟨π, mem, nmem⟩ := SetLike.exists_of_lt hlt

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : π ∉ v.asIdeal ^ 2
⊢ ∃ π, v.intValuationDef π = ↑(ofAdd (-1))

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors)) = ofAdd (-1)

Tactic:
apply congr_arg

Result:
case h.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ -↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors) = -1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : π ∉ v.asIdeal ^ 2
⊢ π ≠ 0

Tactic:
intro h

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : π ∉ v.asIdeal ^ 2
h : π = 0
⊢ False

Proof state:
case h.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ -↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors) = -1

Tactic:
rw [neg_inj, ← Int.ofNat_one, Int.natCast_inj]

Result:
case h.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1

Proof state:
case h.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : Associates.mk v.asIdeal ≤ Associates.mk (Ideal.span {π})
nmem : ¬Associates.mk (v.asIdeal ^ 2) ≤ Associates.mk (Ideal.span {π})
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1

Tactic:
rw [← pow_one (Associates.mk v.asIdeal), Associates.prime_pow_dvd_iff_le hπ hv] at mem

Result:
case h.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : 1 ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors
nmem : ¬Associates.mk (v.asIdeal ^ 2) ≤ Associates.mk (Ideal.span {π})
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ v.intValuationDef π = ↑(ofAdd (-1))

Tactic:
rw [intValuationDef, if_neg (Associates.mk_ne_zero'.mp hπ), WithZero.coe_inj]

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
nmem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors)) = ofAdd (-1)