internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.ab_coprime
Proof state before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
⊢ False
Tactic:
have Hq : ↑q ∣ ({a, b, c} : Finset ℤ).gcd id := by
  refine' dvd_gcd fun x hx => _
  simp only [mem_insert, mem_singleton] at hx
  rcases hx with (H | H | H) <;> simpa [H]
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
Hq : ↑q ∣ {a, b, c}.gcd id
⊢ False
Theorem: FltRegular.ab_coprime
Proof state before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
Hq : ↑q ∣ {a, b, c}.gcd id
⊢ False
Tactic:
rw [hgcd] at Hq
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
Hq : ↑q ∣ 1
⊢ False
Theorem: FltRegular.ab_coprime
Proof state before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
Hq : ↑q ∣ 1
⊢ False
Tactic:
exact hqpri.not_unit (isUnit_of_dvd_one Hq)
Proof state after:
no goals
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : q.Prime
hq : q ∣ a.gcd b
⊢ (↑q).natAbs.Prime
Tactic:
simp [hqpri]
Proof state after:
no goals
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
⊢ ↑q ∣ a
Tactic:
obtain ⟨m, hm⟩ := @Int.gcd_dvd_left a b
Proof state after:
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
m : ℤ
hm : a = ↑(a.gcd b) * m
⊢ ↑q ∣ a
Theorem: FltRegular.ab_coprime
Proof state before:
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
m : ℤ
hm : a = ↑(a.gcd b) * m
⊢ ↑q ∣ a
Tactic:
exact ⟨n * m, by rw [hm, hn]; simp [mul_assoc]⟩
Proof state after:
no goals
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
m : ℤ
hm : a = ↑(a.gcd b) * m
⊢ a = ↑q * (↑n * m)
Tactic:
rw [hm, hn]
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
m : ℤ
hm : a = ↑(a.gcd b) * m
⊢ ↑(q * n) * m = ↑q * (↑n * m)
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
m : ℤ
hm : a = ↑(a.gcd b) * m
⊢ ↑(q * n) * m = ↑q * (↑n * m)
Tactic:
simp [mul_assoc]
Proof state after:
no goals
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
⊢ ↑q ∣ b
Tactic:
obtain ⟨m, hm⟩ := @Int.gcd_dvd_right a b
Proof state after:
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
m : ℤ
hm : b = ↑(a.gcd b) * m
⊢ ↑q ∣ b
Theorem: FltRegular.ab_coprime
Proof state before:
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
m : ℤ
hm : b = ↑(a.gcd b) * m
⊢ ↑q ∣ b
Tactic:
exact ⟨n * m, by rw [hm, hn]; simp [mul_assoc]⟩
Proof state after:
no goals
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
m : ℤ
hm : b = ↑(a.gcd b) * m
⊢ b = ↑q * (↑n * m)
Tactic:
rw [hm, hn]
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
m : ℤ
hm : b = ↑(a.gcd b) * m
⊢ ↑(q * n) * m = ↑q * (↑n * m)
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
m : ℤ
hm : b = ↑(a.gcd b) * m
⊢ ↑(q * n) * m = ↑q * (↑n * m)
Tactic:
simp [mul_assoc]
Proof state after:
no goals
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ ↑q ∣ c
Tactic:
suffices ↑q ∣ c ^ p by exact hqpri.dvd_of_dvd_pow this
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ ↑q ∣ c ^ p
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ ↑q ∣ c ^ p
Tactic:
rw [← H]
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ ↑q ∣ a ^ p + b ^ p
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
⊢ ↑q ∣ a ^ p + b ^ p
Tactic:
exact dvd_add (dvd_pow haq hpzero) (dvd_pow hbq hpzero)
Proof state after:
no goals
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
this : ↑q ∣ c ^ p
⊢ ↑q ∣ c
Tactic:
exact hqpri.dvd_of_dvd_pow this
Proof state after:
no goals
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
⊢ ↑q ∣ {a, b, c}.gcd id
Tactic:
refine' dvd_gcd fun x hx => _
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
x : ℤ
hx : x ∈ {a, b, c}
⊢ ↑q ∣ id x
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
x : ℤ
hx : x ∈ {a, b, c}
⊢ ↑q ∣ id x
Tactic:
simp only [mem_insert, mem_singleton] at hx
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ ↑q ∣ id x
Theorem: FltRegular.ab_coprime
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ ↑q ∣ id x
Tactic:
rcases hx with (H | H | H) <;> simpa [H]
Proof state after:
no goals
Theorem: FltRegular.exists_ideal
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Tactic:
have H₁ := congr_arg (algebraMap ℤ R) H
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
H₁ :
  (algebraMap ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) (a ^ p + b ^ p) = (algebraMap ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) (c ^ p)
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Theorem: FltRegular.exists_ideal
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
H₁ :
  (algebraMap ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) (a ^ p + b ^ p) = (algebraMap ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) (c ^ p)
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Tactic:
simp only [eq_intCast, Int.cast_add, Int.cast_pow] at H₁
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
H₁ : ↑a ^ p + ↑b ^ p = ↑c ^ p
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Theorem: FltRegular.exists_ideal
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
H₁ : ↑a ^ p + ↑b ^ p = ↑c ^ p
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Tactic:
have hζ' := (zeta_spec P ℚ K).unit'_coe
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
H₁ : ↑a ^ p + ↑b ^ p = ↑c ^ p
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Theorem: FltRegular.exists_ideal
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
H₁ : ↑a ^ p + ↑b ^ p = ↑c ^ p
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Tactic:
rw [pow_add_pow_eq_prod_add_zeta_runity_mul
  (hpri.out.eq_two_or_odd.resolve_left fun h => by simp [h] at h5p) hζ'] at H₁
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
H₁ : ∏ ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), (↑a + ζ * ↑b) = ↑c ^ p
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Theorem: FltRegular.exists_ideal
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
H₁ : ∏ ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), (↑a + ζ * ↑b) = ↑c ^ p
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Tactic:
replace H₁ := congr_arg (fun x => span ({ x } : Set R)) H₁
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
H₁ :
  (fun x => span {x}) (∏ ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), (↑a + ζ * ↑b)) =
    (fun x => span {x}) (↑c ^ p)
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Theorem: FltRegular.exists_ideal
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
H₁ :
  (fun x => span {x}) (∏ ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), (↑a + ζ * ↑b)) =
    (fun x => span {x}) (↑c ^ p)
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Tactic:
simp only [← prod_span_singleton, ← span_singleton_pow] at H₁
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
H₁ : ∏ i ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), span {↑a + i * ↑b} = span {↑c} ^ p
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Theorem: FltRegular.exists_ideal
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
H₁ : ∏ i ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), span {↑a + i * ↑b} = span {↑c} ^ p
⊢ ∃ I, span {↑a + ζ * ↑b} = I ^ p
Tactic:
refine' Finset.exists_eq_pow_of_mul_eq_pow_of_coprime (fun η₁ hη₁ η₂ hη₂ hη => ?_) H₁ ζ hζ
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
H₁ : ∏ i ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), span {↑a + i * ↑b} = span {↑c} ^ p
η₁ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₁ : η₁ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
η₂ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₂ : η₂ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hη : η₁ ≠ η₂
⊢ IsCoprime (span {↑a + η₁ * ↑b}) (span {↑a + η₂ * ↑b})
Theorem: FltRegular.exists_ideal
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
H₁ : ∏ i ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), span {↑a + i * ↑b} = span {↑c} ^ p
η₁ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₁ : η₁ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
η₂ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₂ : η₂ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hη : η₁ ≠ η₂
⊢ IsCoprime (span {↑a + η₁ * ↑b}) (span {↑a + η₂ * ↑b})
Tactic:
refine' fltIdeals_coprime _ _ H (ab_coprime H hpri.out.ne_zero hgcd) hη₁ hη₂ hη caseI
Proof state after:
case refine'_1
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
H₁ : ∏ i ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), span {↑a + i * ↑b} = span {↑c} ^ p
η₁ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₁ : η₁ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
η₂ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₂ : η₂ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hη : η₁ ≠ η₂
⊢ (↑⟨p, ⋯⟩).Prime

case refine'_2
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
H₁ : ∏ i ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), span {↑a + i * ↑b} = span {↑c} ^ p
η₁ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₁ : η₁ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
η₂ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₂ : η₂ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hη : η₁ ≠ η₂
⊢ 5 ≤ ⟨p, ⋯⟩
Theorem: FltRegular.exists_ideal
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
H₁ : ↑a ^ p + ↑b ^ p = ↑c ^ p
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
h : p = 2
⊢ False
Tactic:
simp [h] at h5p
Proof state after:
no goals
Theorem: FltRegular.exists_ideal
Proof state before:
case refine'_1
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
H₁ : ∏ i ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), span {↑a + i * ↑b} = span {↑c} ^ p
η₁ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₁ : η₁ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
η₂ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₂ : η₂ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hη : η₁ ≠ η₂
⊢ (↑⟨p, ⋯⟩).Prime
Tactic:
exact hpri.out
Proof state after:
no goals
Theorem: FltRegular.exists_ideal
Proof state before:
case refine'_2
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
h5p : 5 ≤ p
H : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ' : IsPrimitiveRoot ↑⋯.unit' ↑⟨p, ⋯⟩
H₁ : ∏ i ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)), span {↑a + i * ↑b} = span {↑c} ^ p
η₁ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₁ : η₁ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
η₂ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hη₂ : η₂ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hη : η₁ ≠ η₂
⊢ 5 ≤ ⟨p, ⋯⟩
Tactic:
exact h5p
Proof state after:
no goals
Theorem: FltRegular.is_principal_aux
Proof state before:
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
letI : NumberField K' := IsCyclotomicExtension.numberField { P } ℚ K'
Proof state after:
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Theorem: FltRegular.is_principal_aux
Proof state before:
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
obtain ⟨α, hα⟩ : I.IsPrincipal := by
  apply IsPrincipal_of_IsPrincipal_pow_of_Coprime (𝓞 K') _ hreg I
  constructor
  use ↑a + ζ * ↑b
  rw [submodule_span_eq, hI]
Proof state after:
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : I = Submodule.span (𝓞 K') {α}
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Theorem: FltRegular.is_principal_aux
Proof state before:
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : I = Submodule.span (𝓞 K') {α}
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
replace hα := congr_arg (fun (J : Submodule _ _) => J ^ p) hα
Proof state after:
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : (fun J => J ^ p) I = (fun J => J ^ p) (Submodule.span (𝓞 K') {α})
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Theorem: FltRegular.is_principal_aux
Proof state before:
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : (fun J => J ^ p) I = (fun J => J ^ p) (Submodule.span (𝓞 K') {α})
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
simp only [← hI, submodule_span_eq, span_singleton_pow, span_singleton_eq_span_singleton] at hα
Proof state after:
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : Associated (↑a + ζ * ↑b) (α ^ p)
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Theorem: FltRegular.is_principal_aux
Proof state before:
case mk.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
hα : Associated (↑a + ζ * ↑b) (α ^ p)
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
obtain ⟨u, hu⟩ := hα
Proof state after:
case mk.intro.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b