internlm/Lean-Github huggingface dataset:
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
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
⊢ gcd (Ideal.span {x}) I = 1
Tactic:
rwa [Irreducible.gcd_eq_one_iff]
Proof state after:
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
⊢ Irreducible (Ideal.span {x})
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
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
⊢ Irreducible (Ideal.span {x})
Tactic:
rwa [irreducible_iff_prime, Ideal.prime_iff_isPrime, Ideal.span_singleton_prime]
Proof state after:
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

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
⊢ Ideal.span {x} ≠ ⊥
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
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
Tactic:
exact hx.ne_zero
Proof state after:
no goals
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
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
⊢ Ideal.span {x} ≠ ⊥
Tactic:
rw [Ne, Ideal.span_singleton_eq_bot]
Proof state after:
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
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
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
Tactic:
exact hx.ne_zero
Proof state after:
no goals
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case pos.intro.intro
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' : R
ha : ¬x ^ n' ∣ a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ n' ∣ b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) a' / (algebraMap R K) b') = ↑I / ↑J
⊢ False
Tactic:
exact IH ⟨a', b', ha, hb, e₀⟩
Proof state after:
no goals
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case pos.intro.intro.hc
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' : R
ha : ¬x ^ n' ∣ a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ n' ∣ b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) x * (algebraMap R K) a' / ((algebraMap R K) x * (algebraMap R K) b')) = ↑I / ↑J
⊢ (algebraMap R K) x ≠ 0
Tactic:
rw [Ne, ← (algebraMap R K).map_zero, (IsFractionRing.injective R K).eq_iff]
Proof state after:
case pos.intro.intro.hc
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' : R
ha : ¬x ^ n' ∣ a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ n' ∣ b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) x * (algebraMap R K) a' / ((algebraMap R K) x * (algebraMap R K) b')) = ↑I / ↑J
⊢ ¬x = 0
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case pos.intro.intro.hc
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' : R
ha : ¬x ^ n' ∣ a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ n' ∣ b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) x * (algebraMap R K) a' / ((algebraMap R K) x * (algebraMap R K) b')) = ↑I / ↑J
⊢ ¬x = 0
Tactic:
exact hx.ne_zero
Proof state after:
no goals
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg
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
⊢ False
Tactic:
refine IH ⟨a, b, h, ?_, e₀⟩
Proof state after:
case neg
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
⊢ ¬x ^ n' ∣ b
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg
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
⊢ ¬x ^ n' ∣ b
Tactic:
intro hb
Proof state after:
case neg
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
hb : x ^ n' ∣ b
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg
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
hb : x ^ n' ∣ b
⊢ False
Tactic:
apply h
Proof state after:
case neg
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
hb : x ^ n' ∣ b
⊢ x ^ n' ∣ a
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg
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
hb : x ^ n' ∣ b
⊢ x ^ n' ∣ a
Tactic:
rw [← Ideal.mem_span_singleton, ← Ideal.dvd_span_singleton] at hb ⊢
Proof state after:
case neg
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
hb : Ideal.span {x ^ n'} ∣ Ideal.span {b}
⊢ Ideal.span {x ^ n'} ∣ Ideal.span {a}
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg
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
hb : Ideal.span {x ^ n'} ∣ Ideal.span {b}
⊢ Ideal.span {x ^ n'} ∣ Ideal.span {a}
Tactic:
replace hb := hb.trans (dvd_mul_left _ I)
Proof state after:
case neg
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
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ Ideal.span {x ^ n'} ∣ Ideal.span {a}
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg
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
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
this : gcd (Ideal.span {x ^ n'}) J = 1
⊢ Ideal.span {x ^ n'} ∣ Ideal.span {a}
Tactic:
rwa [← e, mul_comm, ← dvd_gcd_mul_iff_dvd_mul, this, one_mul] at hb
Proof state after:
no goals