R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.7591
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
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.7591
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
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
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.7591
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}
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.7591
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
rw [Filter.eventually_cofinite, h_supp]
no goals
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.7591
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}
exact Ideal.finite_factors hI
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.7591
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}
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.7591
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}
ext v
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.7591
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}
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.7591
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}
simp_rw [Int.coe_nat_eq_zero]
no goals
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.7591
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}
exact Associates.count_ne_zero_iff_dvd hI v.irreducible