internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_3.intro
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : b ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
n : ℤ
hn : c = ↑p * n
⊢ False
Tactic:
refine' caseI ⟨a * b * n, _⟩
Proof state after:
case pos.refine'_3.intro
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : b ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
n : ℤ
hn : c = ↑p * n
⊢ a * b * c = ↑p * (a * b * n)
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_3.intro
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : b ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
n : ℤ
hn : c = ↑p * n
⊢ a * b * c = ↑p * (a * b * n)
Tactic:
rw [hn]
Proof state after:
case pos.refine'_3.intro
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : b ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
n : ℤ
hn : c = ↑p * n
⊢ a * b * (↑p * n) = ↑p * (a * b * n)
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_3.intro
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : b ≡ -c [ZMOD ↑p]
hp3 : p ≠ 3
n : ℤ
hn : c = ↑p * n
⊢ a * b * (↑p * n) = ↑p * (a * b * n)
Tactic:
ring
Proof state after:
no goals
Theorem: FltRegular.a_not_cong_b
Proof state before:
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
habs : a ≡ -c [ZMOD ↑p]
⊢ p ≠ 3
Tactic:
linarith
Proof state after:
no goals
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_4
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ a * -c * -b ≠ 0
Tactic:
convert hprod using 1
Proof state after:
case h.e'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ a * -c * -b = a * b * c
Theorem: FltRegular.a_not_cong_b
Proof state before:
case h.e'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ a * -c * -b = a * b * c
Tactic:
ring
Proof state after:
no goals
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_5
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ ¬↑p ∣ a * -c * -b
Tactic:
ring_nf at caseI ⊢
Proof state after:
case pos.refine'_5
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ ¬↑p ∣ a * b * c
Theorem: FltRegular.a_not_cong_b
Proof state before:
case pos.refine'_5
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
⊢ ¬↑p ∣ a * b * c
Tactic:
exact caseI
Proof state after:
no goals
Theorem: FltRegular.not_exists_solution
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
m : ℕ
hm : 1 ≤ m
⊢ ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ m * z') ^ ↑p
Tactic:
induction' m, hm using Nat.le_induction with m' _ IH
Proof state after:
case base
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
m : ℕ
⊢ ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ 1 * z') ^ ↑p

case succ
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
m m' : ℕ
hmn✝ : 1 ≤ m'
IH :
  ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ m' * z') ^ ↑p
⊢ ¬∃ x' y' z' ε₃,
      ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ (m' + 1) * z') ^ ↑p
Theorem: FltRegular.not_exists_solution
Proof state before:
case base
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
m : ℕ
⊢ ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ 1 * z') ^ ↑p
Tactic:
rintro ⟨x, y, z, ε₃, hy, hz, e⟩
Proof state after:
case base.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
m : ℕ
x y z : 𝓞 K
ε₃ : (𝓞 K)ˣ
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ¬↑hζ.unit' - 1 ∣ z
e : x ^ ↑p + y ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ 1 * z) ^ ↑p
⊢ False
Theorem: FltRegular.not_exists_solution
Proof state before:
case base.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
m : ℕ
x y z : 𝓞 K
ε₃ : (𝓞 K)ˣ
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ¬↑hζ.unit' - 1 ∣ z
e : x ^ ↑p + y ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ 1 * z) ^ ↑p
⊢ False
Tactic:
exact zero_lt_one.not_le (one_le_m hp hζ e hy hz)
Proof state after:
no goals
Theorem: FltRegular.not_exists_solution
Proof state before:
case succ
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
m m' : ℕ
hmn✝ : 1 ≤ m'
IH :
  ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ m' * z') ^ ↑p
⊢ ¬∃ x' y' z' ε₃,
      ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ (m' + 1) * z') ^ ↑p
Tactic:
rintro ⟨x, y, z, ε₃, hy, hz, e⟩
Proof state after:
case succ.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
m m' : ℕ
hmn✝ : 1 ≤ m'
IH :
  ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ m' * z') ^ ↑p
x y z : 𝓞 K
ε₃ : (𝓞 K)ˣ
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ¬↑hζ.unit' - 1 ∣ z
e : x ^ ↑p + y ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ (m' + 1) * z) ^ ↑p
⊢ False
Theorem: FltRegular.not_exists_solution
Proof state before:
case succ.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
m m' : ℕ
hmn✝ : 1 ≤ m'
IH :
  ¬∃ x' y' z' ε₃, ¬↑hζ.unit' - 1 ∣ y' ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ m' * z') ^ ↑p
x y z : 𝓞 K
ε₃ : (𝓞 K)ˣ
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ¬↑hζ.unit' - 1 ∣ z
e : x ^ ↑p + y ^ ↑p = ↑ε₃ * ((↑hζ.unit' - 1) ^ (m' + 1) * z) ^ ↑p
⊢ False
Tactic:
exact IH (exists_solution' hp hreg hζ e hy hz)
Proof state after:
no goals
Theorem: FltRegular.not_exists_solution'
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ¬∃ x y z, ¬↑hζ.unit' - 1 ∣ y ∧ ↑hζ.unit' - 1 ∣ z ∧ z ≠ 0 ∧ x ^ ↑p + y ^ ↑p = z ^ ↑p
Tactic:
letI : Fact (Nat.Prime p) := hpri
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this : Fact (↑p).Prime := hpri
⊢ ¬∃ x y z, ¬↑hζ.unit' - 1 ∣ y ∧ ↑hζ.unit' - 1 ∣ z ∧ z ≠ 0 ∧ x ^ ↑p + y ^ ↑p = z ^ ↑p
Theorem: FltRegular.not_exists_solution'
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this : Fact (↑p).Prime := hpri
⊢ ¬∃ x y z, ¬↑hζ.unit' - 1 ∣ y ∧ ↑hζ.unit' - 1 ∣ z ∧ z ≠ 0 ∧ x ^ ↑p + y ^ ↑p = z ^ ↑p
Tactic:
letI : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
⊢ ¬∃ x y z, ¬↑hζ.unit' - 1 ∣ y ∧ ↑hζ.unit' - 1 ∣ z ∧ z ≠ 0 ∧ x ^ ↑p + y ^ ↑p = z ^ ↑p
Theorem: FltRegular.not_exists_solution'
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
⊢ ¬∃ x y z, ¬↑hζ.unit' - 1 ∣ y ∧ ↑hζ.unit' - 1 ∣ z ∧ z ≠ 0 ∧ x ^ ↑p + y ^ ↑p = z ^ ↑p
Tactic:
rintro ⟨x, y, z, hy, hz, hz', e⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
⊢ False
Theorem: FltRegular.not_exists_solution'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
m : ℕ
z : 𝓞 K
hm : 1 ≤ m
hz'' : ¬↑hζ.unit' - 1 ∣ z
hz : ↑hζ.unit' - 1 ∣ (↑hζ.unit' - 1) ^ m * z
hz' : (↑hζ.unit' - 1) ^ m * z ≠ 0
e : x ^ ↑p + y ^ ↑p = ((↑hζ.unit' - 1) ^ m * z) ^ ↑p
⊢ False
Tactic:
refine not_exists_solution hp hreg hζ hm ⟨x, y, z, 1, hy, hz'', ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
m : ℕ
z : 𝓞 K
hm : 1 ≤ m
hz'' : ¬↑hζ.unit' - 1 ∣ z
hz : ↑hζ.unit' - 1 ∣ (↑hζ.unit' - 1) ^ m * z
hz' : (↑hζ.unit' - 1) ^ m * z ≠ 0
e : x ^ ↑p + y ^ ↑p = ((↑hζ.unit' - 1) ^ m * z) ^ ↑p
⊢ x ^ ↑p + y ^ ↑p = ↑1 * ((↑hζ.unit' - 1) ^ m * z) ^ ↑p
Theorem: FltRegular.not_exists_solution'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
m : ℕ
z : 𝓞 K
hm : 1 ≤ m
hz'' : ¬↑hζ.unit' - 1 ∣ z
hz : ↑hζ.unit' - 1 ∣ (↑hζ.unit' - 1) ^ m * z
hz' : (↑hζ.unit' - 1) ^ m * z ≠ 0
e : x ^ ↑p + y ^ ↑p = ((↑hζ.unit' - 1) ^ m * z) ^ ↑p
⊢ x ^ ↑p + y ^ ↑p = ↑1 * ((↑hζ.unit' - 1) ^ m * z) ^ ↑p
Tactic:
rwa [Units.val_one, one_mul]
Proof state after:
no goals
Theorem: FltRegular.not_exists_solution'
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
⊢ ∃ m z', 1 ≤ m ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ z = (↑hζ.unit' - 1) ^ m * z'
Tactic:
have H : multiplicity.Finite ((hζ.unit' : 𝓞 K) - 1) z := WfDvdMonoid.multiplicity_finite
  (M := 𝓞 K) hζ.zeta_sub_one_prime'.not_unit hz'
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
⊢ ∃ m z', 1 ≤ m ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ z = (↑hζ.unit' - 1) ^ m * z'
Theorem: FltRegular.not_exists_solution'
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
⊢ ∃ m z', 1 ≤ m ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ z = (↑hζ.unit' - 1) ^ m * z'
Tactic:
obtain ⟨z', h⟩ := multiplicity.pow_multiplicity_dvd H
Proof state after:
case intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ ∃ m z', 1 ≤ m ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ z = (↑hζ.unit' - 1) ^ m * z'
Theorem: FltRegular.not_exists_solution'
Proof state before:
case intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ ∃ m z', 1 ≤ m ∧ ¬↑hζ.unit' - 1 ∣ z' ∧ z = (↑hζ.unit' - 1) ^ m * z'
Tactic:
refine ⟨_, _, ?_, ?_, h⟩
Proof state after:
case intro.refine_1
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ 1 ≤ (multiplicity (↑hζ.unit' - 1) z).get H

case intro.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ ¬↑hζ.unit' - 1 ∣ z'
Theorem: FltRegular.not_exists_solution'
Proof state before:
case intro.refine_1
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ 1 ≤ (multiplicity (↑hζ.unit' - 1) z).get H
Tactic:
rwa [← PartENat.coe_le_coe, PartENat.natCast_get, ← multiplicity.pow_dvd_iff_le_multiplicity,
  pow_one]
Proof state after:
no goals
Theorem: FltRegular.not_exists_solution'
Proof state before:
case intro.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ ¬↑hζ.unit' - 1 ∣ z'
Tactic:
intro h'
Proof state after:
case intro.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
h' : ↑hζ.unit' - 1 ∣ z'
⊢ False
Theorem: FltRegular.not_exists_solution'
Proof state before:
case intro.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝ : Fact (↑p).Prime := hpri
this : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
h' : ↑hζ.unit' - 1 ∣ z'
⊢ False
Tactic:
have := mul_dvd_mul_left (((hζ.unit' : 𝓞 K) - 1) ^ Part.get (multiplicity _ z) H) h'
Proof state after:
case intro.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝¹ : Fact (↑p).Prime := hpri
this✝ : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
h' : ↑hζ.unit' - 1 ∣ z'
this :
  (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * (↑hζ.unit' - 1) ∣
    (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ False
Theorem: FltRegular.not_exists_solution'
Proof state before:
case intro.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝¹ : Fact (↑p).Prime := hpri
this✝ : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
h' : ↑hζ.unit' - 1 ∣ z'
this :
  (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * (↑hζ.unit' - 1) ∣
    (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
⊢ False
Tactic:
rw [← pow_succ, ← h] at this
Proof state after:
case intro.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝¹ : Fact (↑p).Prime := hpri
this✝ : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
h' : ↑hζ.unit' - 1 ∣ z'
this : (↑hζ.unit' - 1) ^ ((multiplicity (↑hζ.unit' - 1) z).get H + 1) ∣ z
⊢ False
Theorem: FltRegular.not_exists_solution'
Proof state before:
case intro.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
this✝¹ : Fact (↑p).Prime := hpri
this✝ : WfDvdMonoid (𝓞 K) := IsNoetherianRing.wfDvdMonoid
x y z : 𝓞 K
hy : ¬↑hζ.unit' - 1 ∣ y
hz : ↑hζ.unit' - 1 ∣ z
hz' : z ≠ 0
e : x ^ ↑p + y ^ ↑p = z ^ ↑p
H : multiplicity.Finite (↑hζ.unit' - 1) z
z' : 𝓞 K
h : z = (↑hζ.unit' - 1) ^ (multiplicity (↑hζ.unit' - 1) z).get H * z'
h' : ↑hζ.unit' - 1 ∣ z'
this : (↑hζ.unit' - 1) ^ ((multiplicity (↑hζ.unit' - 1) z).get H + 1) ∣ z
⊢ False
Tactic:
exact multiplicity.is_greatest' H (Nat.lt_succ_self _) this
Proof state after:
no goals