Theorem: FltRegular.ex_fin_div
Proof 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])
Proof 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, ⋯⟩