[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite {v | v.asIdeal ∣ I}
[PROOFSTEP]
rw [← Set.finite_coe_iff, Set.coe_setOf]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Finite { x // x.asIdeal ∣ I }
[PROOFSTEP]
haveI h_fin := fintypeSubtypeDvd I hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
⊢ Finite { x // x.asIdeal ∣ I }
[PROOFSTEP]
refine' Finite.of_injective (fun v => (⟨(v : HeightOneSpectrum R).asIdeal, v.2⟩ : { x // x ∣ I })) _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
⊢ Injective fun v => { val := (↑v).asIdeal, property := (_ : (↑v).asIdeal ∣ I) }
[PROOFSTEP]
intro v w hvw
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
hvw :
  (fun v => { val := (↑v).asIdeal, property := (_ : (↑v).asIdeal ∣ I) }) v =
    (fun v => { val := (↑v).asIdeal, property := (_ : (↑v).asIdeal ∣ I) }) w
⊢ v = w
[PROOFSTEP]
simp at hvw 
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_fin : Fintype { x // x ∣ I }
v w : { x // x.asIdeal ∣ I }
hvw : (↑v).asIdeal = (↑w).asIdeal
⊢ v = w
[PROOFSTEP]
exact Subtype.coe_injective ((HeightOneSpectrum.ext_iff (R := R) ↑v ↑w).mpr hvw)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) = 0
[PROOFSTEP]
have h_supp :
  {v : HeightOneSpectrum R | ¬((Associates.mk v.asIdeal).count (Associates.mk I).factors : ℤ) = 0} =
    {v : HeightOneSpectrum R | v.asIdeal ∣ I} :=
  by
  ext v
  simp_rw [Int.coe_nat_eq_zero]
  exact Associates.count_ne_zero_iff_dvd hI v.irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ {v | ¬↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) = 0} = {v | v.asIdeal ∣ I}
[PROOFSTEP]
ext v
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
⊢ v ∈ {v | ¬↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) = 0} ↔ v ∈ {v | v.asIdeal ∣ I}
[PROOFSTEP]
simp_rw [Int.coe_nat_eq_zero]
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
⊢ v ∈ {v | ¬count (Associates.mk v.asIdeal) (factors (Associates.mk I)) = 0} ↔ v ∈ {v | v.asIdeal ∣ I}
[PROOFSTEP]
exact Associates.count_ne_zero_iff_dvd hI v.irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_supp : {v | ¬↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) = 0} = {v | v.asIdeal ∣ I}
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) = 0
[PROOFSTEP]
rw [Filter.eventually_cofinite, h_supp]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_supp : {v | ¬↑(count (Associates.mk v.asIdeal) (factors (Associates.mk I))) = 0} = {v | v.asIdeal ∣ I}
⊢ Set.Finite {v | v.asIdeal ∣ I}
[PROOFSTEP]
exact Ideal.finite_factors hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ {v | maxPowDividing v I ≠ 1} ⊆
    {v | ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≠ 0}
[PROOFSTEP]
intro v hv h_zero
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | maxPowDividing v I ≠ 1}
h_zero : ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) = 0
⊢ False
[PROOFSTEP]
have hv' : v.maxPowDividing I = 1 := by
  rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Int.coe_nat_eq_zero.mp h_zero, pow_zero _]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | maxPowDividing v I ≠ 1}
h_zero : ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) = 0
⊢ maxPowDividing v I = 1
[PROOFSTEP]
rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Int.coe_nat_eq_zero.mp h_zero, pow_zero _]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | maxPowDividing v I ≠ 1}
h_zero : ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) = 0
hv' : maxPowDividing v I = 1
⊢ False
[PROOFSTEP]
exact hv hv'
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    (mulSupport fun v =>
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))
[PROOFSTEP]
rw [mulSupport]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite {x | ↑x.asIdeal ^ ↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk I))) ≠ 1}
[PROOFSTEP]
simp_rw [Ne.def, zpow_ofNat, ← FractionalIdeal.coeIdeal_pow, FractionalIdeal.coeIdeal_eq_one]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite {x | ¬x.asIdeal ^ Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk I)) = 1}
[PROOFSTEP]
exact finite_mulSupport hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    (mulSupport fun v =>
      ↑v.asIdeal ^ (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
[PROOFSTEP]
rw [mulSupport]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    {x | ↑x.asIdeal ^ (-↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk I)))) ≠ 1}
[PROOFSTEP]
simp_rw [zpow_neg, Ne.def, inv_eq_one]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    {x | ¬↑x.asIdeal ^ ↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk I))) = 1}
[PROOFSTEP]
exact finite_mulSupport_coe hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ¬v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I
[PROOFSTEP]
have hf := finite_mulSupport hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ ¬v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I
[PROOFSTEP]
have h_ne_zero : v.maxPowDividing I ≠ 0 := pow_ne_zero _ v.ne_bot
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
⊢ ¬v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I
[PROOFSTEP]
rw [← mul_finprod_cond_ne v hf, pow_add, pow_one, finprod_cond_ne _ _ hf]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
⊢ ¬v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
      maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
[PROOFSTEP]
intro h_contr
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
h_contr :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
    maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
⊢ False
[PROOFSTEP]
have hv_prime : Prime v.asIdeal := Ideal.prime_of_isPrime v.ne_bot v.isPrime
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
h_contr :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
    maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
hv_prime : Prime v.asIdeal
⊢ False
[PROOFSTEP]
obtain ⟨w, hw, hvw'⟩ := Prime.exists_mem_finset_dvd hv_prime ((mul_dvd_mul_iff_left h_ne_zero).mp h_contr)
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
h_contr :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
    maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ Finset.erase (Finite.toFinset hf) v
hvw' : v.asIdeal ∣ maxPowDividing w I
⊢ False
[PROOFSTEP]
have hw_prime : Prime w.asIdeal := Ideal.prime_of_isPrime w.ne_bot w.isPrime
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
h_contr :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
    maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ Finset.erase (Finite.toFinset hf) v
hvw' : v.asIdeal ∣ maxPowDividing w I
hw_prime : Prime w.asIdeal
⊢ False
[PROOFSTEP]
have hvw := Prime.dvd_of_dvd_pow hv_prime hvw'
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
h_contr :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
    maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ Finset.erase (Finite.toFinset hf) v
hvw' : v.asIdeal ∣ maxPowDividing w I
hw_prime : Prime w.asIdeal
hvw : v.asIdeal ∣ w.asIdeal
⊢ False
[PROOFSTEP]
rw [Prime.dvd_prime_iff_associated hv_prime hw_prime, associated_iff_eq] at hvw 
[GOAL]
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : Set.Finite (mulSupport fun v => maxPowDividing v I)
h_ne_zero : maxPowDividing v I ≠ 0
h_contr :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) * v.asIdeal ∣
    maxPowDividing v I * ∏ i in Finset.erase (Finite.toFinset hf) v, maxPowDividing i I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ Finset.erase (Finite.toFinset hf) v
hvw' : v.asIdeal ∣ maxPowDividing w I
hw_prime : Prime w.asIdeal
hvw : v.asIdeal = w.asIdeal
⊢ False
[PROOFSTEP]
exact (Finset.mem_erase.mp hw).1 (HeightOneSpectrum.ext w v (Eq.symm hvw))
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
⊢ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
[PROOFSTEP]
rw [Associates.mk_ne_zero, finprod_def]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
⊢ (if h : Set.Finite (mulSupport fun v => maxPowDividing v I) then ∏ i in Finite.toFinset h, maxPowDividing i I
    else 1) ≠
    0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
h✝ : Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ ∏ v in Finite.toFinset h✝, maxPowDividing v I ≠ 0
[PROOFSTEP]
rw [Finset.prod_ne_zero_iff]
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
h✝ : Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ ∀ (a : HeightOneSpectrum R), a ∈ Finite.toFinset h✝ → maxPowDividing a I ≠ 0
[PROOFSTEP]
intro v _
[GOAL]
case pos
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
h✝ : Set.Finite (mulSupport fun v => maxPowDividing v I)
v : HeightOneSpectrum R
a✝ : v ∈ Finite.toFinset h✝
⊢ maxPowDividing v I ≠ 0
[PROOFSTEP]
apply pow_ne_zero _ v.ne_bot
[GOAL]
case neg
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
h✝ : ¬Set.Finite (mulSupport fun v => maxPowDividing v I)
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
have h_ne_zero := Associates.finprod_ne_zero I
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
have hv : Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
have h_dvd := finprod_mem_dvd v (Ideal.finite_mulSupport hI)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd : maxPowDividing v I ∣ ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
have h_not_dvd := Ideal.finprod_not_dvd v I hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd : maxPowDividing v I ∣ ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I
h_not_dvd :
  ¬v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
simp only [IsDedekindDomain.HeightOneSpectrum.maxPowDividing] at h_dvd h_ne_zero h_not_dvd 
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) ∣
    ∏ᶠ (v : HeightOneSpectrum R),
      v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
h_not_dvd :
  ¬v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
rw [← Associates.mk_dvd_mk] at h_dvd h_not_dvd 
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  Associates.mk (v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ∣
    Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))
h_not_dvd :
  ¬Associates.mk (v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1)) ∣
      Associates.mk
        (∏ᶠ (v : HeightOneSpectrum R),
          v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
simp only [Associates.dvd_eq_le] at h_dvd h_not_dvd 
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  Associates.mk (v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≤
    Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))
h_not_dvd :
  ¬Associates.mk (v.asIdeal ^ (Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1)) ≤
      Associates.mk
        (∏ᶠ (v : HeightOneSpectrum R),
          v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le h_ne_zero hv] at h_dvd h_not_dvd 
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) ≤
    Associates.count (Associates.mk v.asIdeal)
      (Associates.factors
        (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
h_not_dvd :
  ¬Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1 ≤
      Associates.count (Associates.mk v.asIdeal)
        (Associates.factors
          (Associates.mk
            (∏ᶠ (v : HeightOneSpectrum R),
              v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
rw [not_le] at h_not_dvd 
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk
      (∏ᶠ (v : HeightOneSpectrum R),
        v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) ≤
    Associates.count (Associates.mk v.asIdeal)
      (Associates.factors
        (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
h_not_dvd :
  Associates.count (Associates.mk v.asIdeal)
      (Associates.factors
        (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))))) <
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)) + 1
⊢ Associates.count (Associates.mk v.asIdeal)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))
[PROOFSTEP]
apply Nat.eq_of_le_of_lt_succ h_dvd h_not_dvd
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I = I
[PROOFSTEP]
rw [← associated_iff_eq, ← Associates.mk_eq_mk_iff_associated]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) = Associates.mk I
[PROOFSTEP]
apply Associates.eq_of_eq_counts
[GOAL]
case ha
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I) ≠ 0
[PROOFSTEP]
apply Associates.finprod_ne_zero I
[GOAL]
case hb
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Associates.mk I ≠ 0
[PROOFSTEP]
apply Associates.mk_ne_zero.mpr hI
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ∀ (p : Associates (Ideal R)),
    Irreducible p →
      Associates.count p (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
        Associates.count p (Associates.factors (Associates.mk I))
[PROOFSTEP]
intro v hv
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
hv : Irreducible v
⊢ Associates.count v (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count v (Associates.factors (Associates.mk I))
[PROOFSTEP]
obtain ⟨J, hJv⟩ := Associates.exists_rep v
[GOAL]
case h.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
hv : Irreducible v
J : Ideal R
hJv : Associates.mk J = v
⊢ Associates.count v (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count v (Associates.factors (Associates.mk I))
[PROOFSTEP]
rw [← hJv, Associates.irreducible_mk] at hv 
[GOAL]
case h.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
J : Ideal R
hv : Irreducible J
hJv : Associates.mk J = v
⊢ Associates.count v (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count v (Associates.factors (Associates.mk I))
[PROOFSTEP]
rw [← hJv]
[GOAL]
case h.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
v : Associates (Ideal R)
J : Ideal R
hv : Irreducible J
hJv : Associates.mk J = v
⊢ Associates.count (Associates.mk J)
      (Associates.factors (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I))) =
    Associates.count (Associates.mk J) (Associates.factors (Associates.mk I))
[PROOFSTEP]
apply Ideal.finprod_count ⟨J, Ideal.isPrime_of_prime (irreducible_iff_prime.mp hv), Irreducible.ne_zero hv⟩ I hI
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) =
    ↑I
[PROOFSTEP]
conv_rhs => rw [← Ideal.finprod_heightOneSpectrum_factorization I hI]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
| ↑I
[PROOFSTEP]
rw [← Ideal.finprod_heightOneSpectrum_factorization I hI]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
| ↑I
[PROOFSTEP]
rw [← Ideal.finprod_heightOneSpectrum_factorization I hI]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
| ↑I
[PROOFSTEP]
rw [← Ideal.finprod_heightOneSpectrum_factorization I hI]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) =
    ↑(∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I)
[PROOFSTEP]
rw [FractionalIdeal.coeIdeal_finprod R⁰ K (le_refl _)]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I))) =
    ∏ᶠ (a : HeightOneSpectrum R), ↑(maxPowDividing a I)
[PROOFSTEP]
simp_rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, FractionalIdeal.coeIdeal_pow, zpow_ofNat]
