-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finprod_not_dvd (I : Ideal R) (hI : I ≠ 0) :
    ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
        ∏ᶠ v : HeightOneSpectrum R, v.maxPowDividing I

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I

Tactic:
have hf := finite_mulSupport hI

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
⊢ ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
⊢ False

Tactic:
have hv_prime : Prime v.asIdeal := Ideal.prime_of_isPrime v.ne_bot v.isPrime

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
⊢ False

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ hf.toFinset.erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
hw_prime : Prime w.asIdeal
hvw : v.asIdeal ∣ w.asIdeal
⊢ False

Tactic:
rw [Prime.dvd_prime_iff_associated hv_prime hw_prime, associated_iff_eq] at hvw

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ hf.toFinset.erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
hw_prime : Prime w.asIdeal
hvw : v.asIdeal = w.asIdeal
⊢ False

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ hf.toFinset.erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
hw_prime : Prime w.asIdeal
hvw : v.asIdeal = w.asIdeal
⊢ False

Tactic:
exact (Finset.mem_erase.mp hw).1 (HeightOneSpectrum.ext hvw.symm)

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ hf.toFinset.erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
⊢ False

Tactic:
have hw_prime : Prime w.asIdeal := Ideal.prime_of_isPrime w.ne_bot w.isPrime

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ hf.toFinset.erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
hw_prime : Prime w.asIdeal
⊢ False

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ hf.toFinset.erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
hw_prime : Prime w.asIdeal
⊢ False

Tactic:
have hvw := Prime.dvd_of_dvd_pow hv_prime hvw'

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ hf.toFinset.erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
hw_prime : Prime w.asIdeal
hvw : v.asIdeal ∣ w.asIdeal
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
⊢ ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I

Tactic:
rw [← mul_finprod_cond_ne v hf, pow_add, pow_one, finprod_cond_ne _ _ hf]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
⊢ ¬v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
      v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
⊢ False

Tactic:
obtain ⟨w, hw, hvw'⟩ :=
  Prime.exists_mem_finset_dvd hv_prime ((mul_dvd_mul_iff_left h_ne_zero).mp h_contr)

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ hf.toFinset.erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
⊢ False