exact hx.ne_zero
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
h✝ : (↑(↑I / ↑J)).IsPrincipal
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
⊢ ¬x = 0
no goals