internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.caseI_easier
Proof state before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
key : ↑↑p ∣ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j
⊢ False
Tactic:
rw [sum_range] at key
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
key : ↑↑p ∣ ∑ i : Fin p, f a b ↑k₁ ↑k₂ ↑i • ζ ^ ↑i
⊢ False
Theorem: FltRegular.caseI_easier
Proof state before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
key : ↑↑p ∣ ∑ i : Fin p, f a b ↑k₁ ↑k₂ ↑i • ζ ^ ↑i
⊢ False
Tactic:
refine' caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right _ _) _)
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
key : ↑↑p ∣ ∑ i : Fin p, f a b ↑k₁ ↑k₂ ↑i • ζ ^ ↑i
⊢ ↑p ∣ a
Theorem: FltRegular.caseI_easier
Proof state before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
key : ↑↑p ∣ ∑ i : Fin p, f a b ↑k₁ ↑k₂ ↑i • ζ ^ ↑i
⊢ ↑p ∣ a
Tactic:
simpa [f] using dvd_coeff_cycl_integer (by exact hpri.out) hζ (auxf hp5 a b k₁ k₂) key
  ⟨0, hpri.out.pos⟩
Proof state after:
no goals
Theorem: FltRegular.caseI_easier
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
⊢ IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
Tactic:
apply @IsCyclotomicExtension.ring_of_integers' _ _ _ _ (by exact hpri) _
Proof state after:
no goals
Theorem: FltRegular.caseI_easier
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
⊢ Fact (↑⟨p, ⋯⟩).Prime
Tactic:
exact hpri
Proof state after:
no goals
Theorem: FltRegular.caseI_easier
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
⊢ ↑↑p ∣ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j
Tactic:
convert hdiv using 1
Proof state after:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Theorem: FltRegular.caseI_easier
Proof state before:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Tactic:
have h01 : 0 ≠ 1 := zero_ne_one
Proof state after:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Theorem: FltRegular.caseI_easier
Proof state before:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Tactic:
have h0k₁ := aux0k₁ hpri.out hp5 hζ caseI hcong hdiv
Proof state after:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Theorem: FltRegular.caseI_easier
Proof state before:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Tactic:
have h0k₂ := aux0k₂ hpri.out hp5 hζ hab hcong hdiv
Proof state after:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Theorem: FltRegular.caseI_easier
Proof state before:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Tactic:
have h1k₁ := aux1k₁ hpri.out hp5 hζ hab hcong hdiv
Proof state after:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
h1k₁ : 1 ≠ ↑k₁
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Theorem: FltRegular.caseI_easier
Proof state before:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
h1k₁ : 1 ≠ ↑k₁
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Tactic:
have h1k₂ := aux1k₂ hpri.out hp5 hζ caseI hcong hdiv
Proof state after:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
h1k₁ : 1 ≠ ↑k₁
h1k₂ : 1 ≠ ↑k₂
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Theorem: FltRegular.caseI_easier
Proof state before:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
h1k₁ : 1 ≠ ↑k₁
h1k₂ : 1 ≠ ↑k₂
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Tactic:
have hk₁k₂ : (k₁ : ℕ) ≠ (k₂ : ℕ) := auxk₁k₂ hpri.out hcong
Proof state after:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
h1k₁ : 1 ≠ ↑k₁
h1k₂ : 1 ≠ ↑k₂
hk₁k₂ : ↑k₁ ≠ ↑k₂
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Theorem: FltRegular.caseI_easier
Proof state before:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
h1k₁ : 1 ≠ ↑k₁
h1k₂ : 1 ≠ ↑k₂
hk₁k₂ : ↑k₁ ≠ ↑k₂
⊢ ∑ j ∈ range p, f a b (↑k₁) (↑k₂) j • ζ ^ j =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Tactic:
simp_rw [f, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right h01, and_assoc,
  ne_and_eq_iff_right h1k₁, ne_and_eq_iff_right h0k₁, ne_and_eq_iff_right hk₁k₂,
  ne_and_eq_iff_right h1k₂, ne_and_eq_iff_right h0k₂, Finset.range_filter_eq]
Proof state after:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
h1k₁ : 1 ≠ ↑k₁
h1k₂ : 1 ≠ ↑k₂
hk₁k₂ : ↑k₁ ≠ ↑k₂
⊢ ∑ x ∈ if 0 < p then {0} else ∅, a • ζ ^ x +
      (∑ x ∈ if 1 < p then {1} else ∅, b • ζ ^ x +
        (∑ x ∈ if ↑k₁ < p then {↑k₁} else ∅, -a • ζ ^ x +
          (∑ x ∈ if ↑k₂ < p then {↑k₂} else ∅, -b • ζ ^ x +
            ∑ x ∈ filter (fun a => a ≠ 0 ∧ a ≠ 1 ∧ a ≠ ↑k₁ ∧ a ≠ ↑k₂) (range p), 0 • ζ ^ x))) =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Theorem: FltRegular.caseI_easier
Proof state before:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
h1k₁ : 1 ≠ ↑k₁
h1k₂ : 1 ≠ ↑k₂
hk₁k₂ : ↑k₁ ≠ ↑k₂
⊢ ∑ x ∈ if 0 < p then {0} else ∅, a • ζ ^ x +
      (∑ x ∈ if 1 < p then {1} else ∅, b • ζ ^ x +
        (∑ x ∈ if ↑k₁ < p then {↑k₁} else ∅, -a • ζ ^ x +
          (∑ x ∈ if ↑k₂ < p then {↑k₂} else ∅, -b • ζ ^ x +
            ∑ x ∈ filter (fun a => a ≠ 0 ∧ a ≠ 1 ∧ a ≠ ↑k₁ ∧ a ≠ ↑k₂) (range p), 0 • ζ ^ x))) =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Tactic:
simp only [hpri.out.pos, hpri.out.one_lt, if_true, zsmul_eq_mul, sum_singleton, _root_.pow_zero,
  mul_one, pow_one, Fin.is_lt, neg_smul, sum_neg_distrib, Ne, zero_smul, sum_const_zero,
  add_zero]
Proof state after:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
h1k₁ : 1 ≠ ↑k₁
h1k₂ : 1 ≠ ↑k₂
hk₁k₂ : ↑k₁ ≠ ↑k₂
⊢ ↑a + (↑b * ζ + (-(↑a * ζ ^ ↑k₁) + -(↑b * ζ ^ ↑k₂))) =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Theorem: FltRegular.caseI_easier
Proof state before:
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
h1k₁ : 1 ≠ ↑k₁
h1k₂ : 1 ≠ ↑k₂
hk₁k₂ : ↑k₁ ≠ ↑k₂
⊢ ↑a + (↑b * ζ + (-(↑a * ζ ^ ↑k₁) + -(↑b * ζ ^ ↑k₂))) =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
Tactic:
ring
Proof state after:
no goals