Theorem: FltRegular.exists_ideal (FltRegular/CaseI/Statement.lean)

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
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

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₁
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

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
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

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₁
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

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₁
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

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₁
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

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ζ
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})

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
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, ⋯⟩

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals