internlm/Lean-Github huggingface dataset:
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case succ.intro.intro.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 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
⊢ False
Tactic:
by_cases h : x ^ n' ∣ a
Proof state after:
case pos
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

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
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case succ.intro.intro.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 b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : spanSingleton R⁰ ((algebraMap R K) a) / spanSingleton R⁰ ((algebraMap R K) b) = ↑I / ↑J
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ spanSingleton R⁰ ((algebraMap R K) b) ≠ 0
Tactic:
rw [Ne, spanSingleton_eq_zero_iff, ← (algebraMap R K).map_zero,
  (IsFractionRing.injective R K).eq_iff]
Proof state after:
case succ.intro.intro.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 b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : spanSingleton R⁰ ((algebraMap R K) a) / spanSingleton R⁰ ((algebraMap R K) b) = ↑I / ↑J
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ ¬b = 0
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case succ.intro.intro.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 b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : spanSingleton R⁰ ((algebraMap R K) a) / spanSingleton R⁰ ((algebraMap R K) b) = ↑I / ↑J
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ ¬b = 0
Tactic:
rintro rfl
Proof state after:
case succ.intro.intro.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' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ 0
e : spanSingleton R⁰ ((algebraMap R K) a) / spanSingleton R⁰ ((algebraMap R K) 0) = ↑I / ↑J
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) 0) = ↑I / ↑J
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case succ.intro.intro.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' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ 0
e : spanSingleton R⁰ ((algebraMap R K) a) / spanSingleton R⁰ ((algebraMap R K) 0) = ↑I / ↑J
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) 0) = ↑I / ↑J
⊢ False
Tactic:
apply hb (dvd_zero _)
Proof state after:
no goals
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case pos
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:
have ha' : x ∣ a := (dvd_pow_self _ (Nat.one_le_iff_ne_zero.mp hn')).trans h
Proof state after:
case pos
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
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case pos
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
hb' : x ∣ b
⊢ False
Tactic:
obtain ⟨a', rfl⟩ := ha'
Proof state after:
case pos.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
b : R
hb : ¬x ^ (n' + 1) ∣ b
hb' : x ∣ b
a' : R
ha : ¬x ^ (n' + 1) ∣ x * a'
e : Ideal.span {x * a'} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) (x * a') / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ x * a'
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case pos.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
b : R
hb : ¬x ^ (n' + 1) ∣ b
hb' : x ∣ b
a' : R
ha : ¬x ^ (n' + 1) ∣ x * a'
e : Ideal.span {x * a'} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) (x * a') / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ x * a'
⊢ False
Tactic:
obtain ⟨b', rfl⟩ := hb'
Proof state after:
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' + 1) ∣ x * a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ (n' + 1) ∣ x * b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) (x * a') / (algebraMap R K) (x * b')) = ↑I / ↑J
⊢ False
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' + 1) ∣ x * a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ (n' + 1) ∣ x * b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) (x * a') / (algebraMap R K) (x * b')) = ↑I / ↑J
⊢ False
Tactic:
rw [pow_succ', mul_dvd_mul_iff_left hx.ne_zero] at ha hb
Proof state after:
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) (x * a') / (algebraMap R K) (x * b')) = ↑I / ↑J
⊢ False
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) (x * a') / (algebraMap R K) (x * b')) = ↑I / ↑J
⊢ False
Tactic:
rw [_root_.map_mul, _root_.map_mul, mul_div_mul_left] at e₀
Proof state after:
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

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
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
this : gcd (Ideal.span {x}) I = 1
⊢ x ∣ b
Tactic:
rw [← Ideal.mem_span_singleton, ← Ideal.dvd_span_singleton] at ha' ⊢
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' : Ideal.span {x} ∣ Ideal.span {a}
this : gcd (Ideal.span {x}) I = 1
⊢ Ideal.span {x} ∣ Ideal.span {b}
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' : Ideal.span {x} ∣ Ideal.span {a}
this : gcd (Ideal.span {x}) I = 1
⊢ Ideal.span {x} ∣ Ideal.span {b}
Tactic:
replace h := ha'.trans (dvd_mul_right _ J)
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
ha' : Ideal.span {x} ∣ Ideal.span {a}
this : gcd (Ideal.span {x}) I = 1
h : Ideal.span {x} ∣ Ideal.span {a} * J
⊢ Ideal.span {x} ∣ Ideal.span {b}
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
ha' : Ideal.span {x} ∣ Ideal.span {a}
this : gcd (Ideal.span {x}) I = 1
h : Ideal.span {x} ∣ Ideal.span {a} * J
⊢ Ideal.span {x} ∣ Ideal.span {b}
Tactic:
rwa [e, ← dvd_gcd_mul_iff_dvd_mul, this, one_mul] at h
Proof state after:
no goals