-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
have have₁ have₂ :
  ∀ (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₃ :
  ∀ (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₄ :
  ∀ (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₅ :
  ∀ (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 ℤ))
h :
  ∀ (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 ℤ))
h₁ :
  ∀ (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)
h₂ :
  ∀ (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
h₃ :
  ∀ (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
h₄ :
  ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal))
    (hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal) (π : R)
    (mem : LE.le (α := Associates (Ideal R)) (Associates.mk v.asIdeal) (Associates.mk (Ideal.span {π})))
    (notMem :
      ¬LE.le (α := Associates (Ideal R)) (Associates.mk (HPow.hPow (β := ℕ) v.asIdeal 2))
          (Associates.mk (Ideal.span {π})))
    (hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0),
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) = 1
h₅ :
  ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal))
    (hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal) (π : R)
    (mem : 1 ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))))
    (notMem :
      ¬LE.le (α := Associates (Ideal R)) (Associates.mk (HPow.hPow (β := ℕ) v.asIdeal 2))
          (Associates.mk (Ideal.span {π})))
    (hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0),
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) = 1
h₆ :
  ∀ (hv : Irreducible (M := Associates (Ideal R)) (Associates.mk v.asIdeal))
    (hlt : HPow.hPow (β := ℕ) v.asIdeal 2 < v.asIdeal) (π : R)
    (mem : 1 ≤ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))))
    (notMem : Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) < 2)
    (hπ : Ne (α := Associates (Ideal R)) (Associates.mk (Ideal.span {π})) 0),
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {π}))) = 1
⊢ ∃ (π : R),
    Eq (α := WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) π : WithZero (Multiplicative ℤ))
      (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
classical
  have hv : 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, Ideal.isUnit_iff.not.mpr v.isPrime.ne_top, sq v.asIdeal⟩
  obtain ⟨π, mem, notMem⟩ := SetLike.exists_of_lt hlt
  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))
  use π
  rw [intValuation_if_neg _ (Associates.mk_ne_zero'.mp hπ), exp_inj]
  apply congr_arg
  rw [← Int.ofNat_one, Int.natCast_inj]
  rw [← Ideal.dvd_span_singleton, ← Associates.mk_le_mk_iff_dvd] at mem notMem
  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 notMem
  exact Nat.eq_of_le_of_lt_succ mem notMem

Premises used: not_le, WithZero.exp_inj, Associates.mk, Associates.mk_le_mk_iff_dvd, IsDedekindDomain.HeightOneSpectrum.asIdeal, Associates.mk_pow, congr_arg, Int.ofNat_one, pow_one, Ideal.dvd_span_singleton, Int.natCast_inj