R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.12131
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
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.12131
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}
intro v hv h_zero
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.12131
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
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.12131
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
have hv' : v.maxPowDividing I = 1 := by
  rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Int.coe_nat_eq_zero.mp h_zero,
    pow_zero _]
no goals
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.12131
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
exact hv hv'
no goals
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type ?u.12131
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
rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Int.coe_nat_eq_zero.mp h_zero,
  pow_zero _]