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

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
let ζ' := (ζ : K)
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
have hζ' : IsPrimitiveRoot ζ' P := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
have h : ζ = (hζ'.unit' : R) := by rfl
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
have hP : P ≠ (2 : ℕ+) := by
  intro hP
  rw [← PNat.coe_inj, PNat.mk_coe] at hP
  rw [hP] at hp5
  contradiction
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
haveI := (⟨hpri.out⟩ : Fact (P : ℕ).Prime)
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
obtain ⟨u, α, hu⟩ := is_principal hreg hp5 hgcd caseI H hζ
State after:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ζ * ↑b
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂

State before:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ζ * ↑b
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
rw [h, mul_comm _ (↑b : R), ← pow_one hζ'.unit'] at hu
State after:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂

State before:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
obtain ⟨k, hk⟩ := FltRegular.CaseI.exists_int_sum_eq_zero hζ' hP hpri.out a b 1 hu.symm
State after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑a + ↑b * ↑(hζ'.unit' ^ 1) - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑(hζ'.unit' ^ (-1))) ∈ span {↑↑⟨p, ⋯⟩}
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂

State before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑a + ↑b * ↑(hζ'.unit' ^ 1) - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑(hζ'.unit' ^ (-1))) ∈ span {↑↑⟨p, ⋯⟩}
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
simp only [zpow_one, zpow_neg, PNat.mk_coe, mem_span_singleton, ← h] at hk
State after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂

State before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
have hpcoe : (p : ℤ) ≠ 0 := by simp [hpri.out.ne_zero]
State after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂

State before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
refine' ⟨⟨(2 * k % p).natAbs, _⟩, ⟨((2 * k - 1) % p).natAbs, _⟩, _, _⟩
State after:
case intro.intro.intro.refine'_1
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ (2 * k % ↑p).natAbs < p

case intro.intro.intro.refine'_2
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ((2 * k - 1) % ↑p).natAbs < p

case intro.intro.intro.refine'_3
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ↑↑⟨((2 * k - 1) % ↑p).natAbs, ?intro.intro.intro.refine'_2⟩ ≡
    ↑↑⟨(2 * k % ↑p).natAbs, ?intro.intro.intro.refine'_1⟩ - 1 [ZMOD ↑p]

case intro.intro.intro.refine'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ↑p ∣
    ↑a + ↑b * ζ - ↑a * ζ ^ ↑⟨(2 * k % ↑p).natAbs, ?intro.intro.intro.refine'_1⟩ -
      ↑b * ζ ^ ↑⟨((2 * k - 1) % ↑p).natAbs, ?intro.intro.intro.refine'_2⟩

State before:
case intro.intro.intro.refine'_1
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ (2 * k % ↑p).natAbs < p

case intro.intro.intro.refine'_2
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ((2 * k - 1) % ↑p).natAbs < p

case intro.intro.intro.refine'_3
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ↑↑⟨((2 * k - 1) % ↑p).natAbs, ?intro.intro.intro.refine'_2⟩ ≡
    ↑↑⟨(2 * k % ↑p).natAbs, ?intro.intro.intro.refine'_1⟩ - 1 [ZMOD ↑p]

case intro.intro.intro.refine'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ↑p ∣
    ↑a + ↑b * ζ - ↑a * ζ ^ ↑⟨(2 * k % ↑p).natAbs, ?intro.intro.intro.refine'_1⟩ -
      ↑b * ζ ^ ↑⟨((2 * k - 1) % ↑p).natAbs, ?intro.intro.intro.refine'_2⟩
Tactic:
repeat'
  rw [← natAbs_ofNat p]
  refine' natAbs_lt_natAbs_of_nonneg_of_lt (emod_nonneg _ hpcoe) _
  rw [natAbs_ofNat]
  exact emod_lt_of_pos _ (by simp [hpri.out.pos])
State after:
case intro.intro.intro.refine'_3
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ↑↑⟨((2 * k - 1) % ↑p).natAbs, ⋯⟩ ≡ ↑↑⟨(2 * k % ↑p).natAbs, ⋯⟩ - 1 [ZMOD ↑p]

case intro.intro.intro.refine'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑⟨(2 * k % ↑p).natAbs, ⋯⟩ - ↑b * ζ ^ ↑⟨((2 * k - 1) % ↑p).natAbs, ⋯⟩

State before:
case intro.intro.intro.refine'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑⟨(2 * k % ↑p).natAbs, ⋯⟩ - ↑b * ζ ^ ↑⟨((2 * k - 1) % ↑p).natAbs, ⋯⟩
Tactic:
simp only [add_sub_assoc, sub_sub] at hk ⊢
State after:
case intro.intro.intro.refine'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑p ∣ ↑a + (↑b * ζ - (↑a * ζ ^ (2 * k % ↑p).natAbs + ↑b * ζ ^ ((2 * k - 1) % ↑p).natAbs))

State before:
case intro.intro.intro.refine'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑p ∣ ↑a + (↑b * ζ - (↑a * ζ ^ (2 * k % ↑p).natAbs + ↑b * ζ ^ ((2 * k - 1) % ↑p).natAbs))
Tactic:
convert hk using 3
State after:
case h.e'_4.h.e'_6.h.e'_6
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑a * ζ ^ (2 * k % ↑p).natAbs + ↑b * ζ ^ ((2 * k - 1) % ↑p).natAbs = ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)

State before:
case h.e'_4.h.e'_6.h.e'_6
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑a * ζ ^ (2 * k % ↑p).natAbs + ↑b * ζ ^ ((2 * k - 1) % ↑p).natAbs = ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
Tactic:
rw [mul_add, mul_comm (↑a : R), ← mul_assoc _ (↑b : R), mul_comm _ (↑b : R), mul_assoc (↑b : R)]
State after:
case h.e'_4.h.e'_6.h.e'_6
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ζ ^ (2 * k % ↑p).natAbs * ↑a + ↑b * ζ ^ ((2 * k - 1) % ↑p).natAbs =
    ↑(hζ'.unit' ^ (2 * k)) * ↑a + ↑b * (↑(hζ'.unit' ^ (2 * k)) * ↑hζ'.unit'⁻¹)

State before:
case h.e'_4.h.e'_6.h.e'_6
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ζ ^ (2 * k % ↑p).natAbs * ↑a + ↑b * ζ ^ ((2 * k - 1) % ↑p).natAbs =
    ↑(hζ'.unit' ^ (2 * k)) * ↑a + ↑b * (↑(hζ'.unit' ^ (2 * k)) * ↑hζ'.unit'⁻¹)
Tactic:
congr 2
State after:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ζ ^ (2 * k % ↑p).natAbs = ↑(hζ'.unit' ^ (2 * k))

case h.e'_4.h.e'_6.h.e'_6.e_a.e_a
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ζ ^ ((2 * k - 1) % ↑p).natAbs = ↑(hζ'.unit' ^ (2 * k)) * ↑hζ'.unit'⁻¹

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
⊢ ζ = ↑hζ'.unit'
Tactic:
rfl
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
⊢ ⟨p, ⋯⟩ ≠ 2
Tactic:
intro hP
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ = 2
⊢ False

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ = 2
⊢ False
Tactic:
rw [← PNat.coe_inj, PNat.mk_coe] at hP
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : p = ↑2
⊢ False

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : p = ↑2
⊢ False
Tactic:
rw [hP] at hp5
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ ↑2
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : p = ↑2
⊢ False

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ ↑2
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : p = ↑2
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
⊢ ↑p ≠ 0
Tactic:
simp [hpri.out.ne_zero]
State after:
no goals

State before:
case intro.intro.intro.refine'_2
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ((2 * k - 1) % ↑p).natAbs < p
Tactic:
rw [← natAbs_ofNat p]
State after:
case intro.intro.intro.refine'_2
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ((2 * k - 1) % ↑(↑p).natAbs).natAbs < (↑p).natAbs

State before:
case intro.intro.intro.refine'_2
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ((2 * k - 1) % ↑(↑p).natAbs).natAbs < (↑p).natAbs
Tactic:
refine' natAbs_lt_natAbs_of_nonneg_of_lt (emod_nonneg _ hpcoe) _
State after:
case intro.intro.intro.refine'_2
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ (2 * k - 1) % ↑(↑p).natAbs < ↑p

State before:
case intro.intro.intro.refine'_2
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ (2 * k - 1) % ↑(↑p).natAbs < ↑p
Tactic:
rw [natAbs_ofNat]
State after:
case intro.intro.intro.refine'_2
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ (2 * k - 1) % ↑p < ↑p

State before:
case intro.intro.intro.refine'_2
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ (2 * k - 1) % ↑p < ↑p
Tactic:
exact emod_lt_of_pos _ (by simp [hpri.out.pos])
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ 0 < ↑p
Tactic:
simp [hpri.out.pos]
State after:
no goals

State before:
case intro.intro.intro.refine'_3
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ↑↑⟨((2 * k - 1) % ↑p).natAbs, ⋯⟩ ≡ ↑↑⟨(2 * k % ↑p).natAbs, ⋯⟩ - 1 [ZMOD ↑p]
Tactic:
simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_eq_intCast_iff,
  ZMod.intCast_mod, Int.cast_sub, Int.cast_mul, Int.cast_natCast, Int.cast_one]
State after:
no goals

State before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ζ ^ (2 * k % ↑p).natAbs = ↑(hζ'.unit' ^ (2 * k))
Tactic:
ext
State after:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑(ζ ^ (2 * k % ↑p).natAbs) = ↑↑(hζ'.unit' ^ (2 * k))

State before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑(ζ ^ (2 * k % ↑p).natAbs) = ↑↑(hζ'.unit' ^ (2 * k))
Tactic:
simp only [Fin.val_mk, map_pow, NumberField.Units.coe_zpow, IsPrimitiveRoot.coe_unit'_coe]
State after:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ (2 * k % ↑p).natAbs = ζ' ^ (2 * k)

State before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ (2 * k % ↑p).natAbs = ζ' ^ (2 * k)
Tactic:
refine eq_of_div_eq_one ?_
State after:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ (2 * k % ↑p).natAbs / ζ' ^ (2 * k) = 1

State before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ (2 * k % ↑p).natAbs / ζ' ^ (2 * k) = 1
Tactic:
rw [← zpow_natCast, ← zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]
State after:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑↑⟨p, ⋯⟩ ∣ ↑(2 * k % ↑p).natAbs - 2 * k

State before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑↑⟨p, ⋯⟩ ∣ ↑(2 * k % ↑p).natAbs - 2 * k
Tactic:
simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_zmod_eq_zero_iff_dvd,
  Int.cast_sub, ZMod.intCast_mod, Int.cast_mul, Int.cast_natCast, sub_self]
State after:
no goals

State before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ζ ^ ((2 * k - 1) % ↑p).natAbs = ↑(hζ'.unit' ^ (2 * k)) * ↑hζ'.unit'⁻¹
Tactic:
ext
State after:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑(ζ ^ ((2 * k - 1) % ↑p).natAbs) = ↑(↑(hζ'.unit' ^ (2 * k)) * ↑hζ'.unit'⁻¹)

State before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑(ζ ^ ((2 * k - 1) % ↑p).natAbs) = ↑(↑(hζ'.unit' ^ (2 * k)) * ↑hζ'.unit'⁻¹)
Tactic:
simp only [Fin.val_mk, map_pow, _root_.map_mul, NumberField.Units.coe_zpow,
  IsPrimitiveRoot.coe_unit'_coe, IsPrimitiveRoot.coe_inv_unit'_coe]
State after:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ ((2 * k - 1) % ↑p).natAbs =
    ζ' ^ (2 * k) * ζ'⁻¹

State before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ ((2 * k - 1) % ↑p).natAbs =
    ζ' ^ (2 * k) * ζ'⁻¹
Tactic:
refine eq_of_div_eq_one ?_
State after:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ ((2 * k - 1) % ↑p).natAbs /
      (ζ' ^ (2 * k) * ζ'⁻¹) =
    1

State before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ ((2 * k - 1) % ↑p).natAbs /
      (ζ' ^ (2 * k) * ζ'⁻¹) =
    1
Tactic:
rw [← zpow_natCast, ← zpow_sub_one₀ (hζ'.ne_zero hpri.out.ne_zero), ←
  zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]
State after:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑↑⟨p, ⋯⟩ ∣ ↑((2 * k - 1) % ↑p).natAbs - (2 * k - 1)

State before:
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑↑⟨p, ⋯⟩ ∣ ↑((2 * k - 1) % ↑p).natAbs - (2 * k - 1)
Tactic:
simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_zmod_eq_zero_iff_dvd,
  Int.cast_sub, ZMod.intCast_mod, Int.cast_mul, Int.cast_natCast, Int.cast_one, sub_self]
State after:
no goals