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
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ gcd (Ideal.span {x ^ n'}) J = 1
Tactic:
rwa [← Ideal.isCoprime_iff_gcd, ← Ideal.span_singleton_pow,
  IsCoprime.pow_left_iff, Ideal.isCoprime_iff_gcd, 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
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ Irreducible (Ideal.span {x})

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}
⊢ 0 < n'
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
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ 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
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ 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
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ 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
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ 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
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ 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
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ ¬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
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ ¬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
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ 0 < n'
Tactic:
rwa [Nat.pos_iff_ne_zero, ← Nat.one_le_iff_ne_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
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
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ (IsLocalization.mk' K s t)
h : s = 0
⊢ False
Tactic:
rw [div_eq_iff hJ', h, IsLocalization.mk'_zero, spanSingleton_zero, zero_mul] at ha
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
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
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I = 0
h : s = 0
⊢ 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
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
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I = 0
h : s = 0
⊢ False
Tactic:
exact hI' ha
Proof state after:
no goals
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg.intro.intro.refine_1
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
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
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ ((algebraMap R K) s / (algebraMap R K) ↑t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
⊢ ¬x ^ (n + m + 1) ∣ s
Tactic:
intro hs
Proof state after:
case neg.intro.intro.refine_1
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
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
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ ((algebraMap R K) s / (algebraMap R K) ↑t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
hs : x ^ (n + m + 1) ∣ s
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg.intro.intro.refine_1
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
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
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ ((algebraMap R K) s / (algebraMap R K) ↑t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
hs : x ^ (n + m + 1) ∣ s
⊢ False
Tactic:
refine hn (dvd_trans (pow_dvd_pow _ ?_) hs)
Proof state after:
case neg.intro.intro.refine_1
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
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
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ ((algebraMap R K) s / (algebraMap R K) ↑t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
hs : x ^ (n + m + 1) ∣ s
⊢ n + 1 ≤ n + m + 1
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg.intro.intro.refine_1
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
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
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ ((algebraMap R K) s / (algebraMap R K) ↑t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
hs : x ^ (n + m + 1) ∣ s
⊢ n + 1 ≤ n + m + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg.intro.intro.refine_2
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
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
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ ((algebraMap R K) s / (algebraMap R K) ↑t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
⊢ ¬x ^ (n + m + 1) ∣ ↑t
Tactic:
intro ht
Proof state after:
case neg.intro.intro.refine_2
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
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
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ ((algebraMap R K) s / (algebraMap R K) ↑t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
ht : x ^ (n + m + 1) ∣ ↑t
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg.intro.intro.refine_2
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
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
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ ((algebraMap R K) s / (algebraMap R K) ↑t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
ht : x ^ (n + m + 1) ∣ ↑t
⊢ False
Tactic:
refine hm (dvd_trans (pow_dvd_pow _ (Nat.le_add_left _ _)) ht)
Proof state after:
no goals
Theorem: flt_regular
Proof state before:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
⊢ FermatLastTheoremFor p
Tactic:
apply fermatLastTheoremFor_iff_int.mpr
Proof state after:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
⊢ FermatLastTheoremWith ℤ p
Theorem: flt_regular
Proof state before:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
⊢ FermatLastTheoremWith ℤ p
Tactic:
intro a b c ha hb hc e
Proof state after:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
⊢ False
Theorem: flt_regular
Proof state before:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
⊢ False
Tactic:
have hprod := mul_ne_zero (mul_ne_zero ha hb) hc
Proof state after:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
⊢ False
Theorem: flt_regular
Proof state before:
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
⊢ False
Tactic:
obtain ⟨e', hgcd, hprod'⟩ := MayAssume.coprime e hprod
Proof state after:
case intro.intro
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
⊢ False
Theorem: flt_regular
Proof state before:
case intro.intro
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
⊢ False
Tactic:
let d := ({a, b, c} : Finset ℤ).gcd id
Proof state after:
case intro.intro
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
⊢ False