internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
⊢ False
Tactic:
refine' hab _
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
⊢ a ≡ b [ZMOD ↑p]
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
⊢ a ≡ b [ZMOD ↑p]
Tactic:
symm
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
⊢ b ≡ a [ZMOD ↑p]
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
⊢ b ≡ a [ZMOD ↑p]
Tactic:
rw [← ZMod.intCast_eq_intCast_iff, ZMod.intCast_eq_intCast_iff_dvd_sub]
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
⊢ ↑p ∣ a - b
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
⊢ ↑p ∣ a - b
Tactic:
have hpri₁ : (P : ℕ).Prime := hpri
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
hpri₁ : (↑⟨p, ⋯⟩).Prime
⊢ ↑p ∣ a - b
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
hpri₁ : (↑⟨p, ⋯⟩).Prime
⊢ ↑p ∣ a - b
Tactic:
simpa [f0k₂] using dvd_coeff_cycl_integer hpri₁ hζ (auxf0k₂ hpri hp5 a b) key ⟨0, hpri.pos⟩
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ - 1 ≡ ↑↑k₂ [ZMOD ↑p]
⊢ ↑↑k₂ = 0
Tactic:
simpa using habs
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
⊢ ζ = ζ ^ ↑⟨1, ⋯⟩
Tactic:
simp
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
⊢ ↑↑p ∣ ∑ j ∈ range p, f0k₂ a b j • ζ ^ j
Tactic:
convert hdiv using 1
Proof state after:
case h.e'_4
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
⊢ ∑ j ∈ range p, f0k₂ a b j • ζ ^ j = ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
case h.e'_4
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
⊢ ∑ j ∈ range p, f0k₂ a b j • ζ ^ j = ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
Tactic:
simp_rw [f0k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right zero_ne_one,
  Finset.range_filter_eq]
Proof state after:
case h.e'_4
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
⊢ ∑ x ∈ if 0 < p then {0} else ∅, (a - b) • ζ ^ x +
      (∑ x ∈ if 1 < p then {1} else ∅, (b - a) • ζ ^ x + ∑ x ∈ filter (fun a => a ≠ 0 ∧ a ≠ 1) (range p), 0 • ζ ^ x) =
    ↑a - ↑b + (↑b - ↑a) * ζ ^ 1
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
case h.e'_4
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
⊢ ∑ x ∈ if 0 < p then {0} else ∅, (a - b) • ζ ^ x +
      (∑ x ∈ if 1 < p then {1} else ∅, (b - a) • ζ ^ x + ∑ x ∈ filter (fun a => a ≠ 0 ∧ a ≠ 1) (range p), 0 • ζ ^ x) =
    ↑a - ↑b + (↑b - ↑a) * ζ ^ 1
Tactic:
simp only [hpri.pos, hpri.one_lt, if_true, zsmul_eq_mul, Int.cast_sub, sum_singleton,
  _root_.pow_zero, mul_one, pow_one, Ne, zero_smul, sum_const_zero, add_zero, Fin.val_mk]
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux_cong1k₁
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 0 [ZMOD ↑p]
⊢ k = ⟨0, ⋯⟩
Tactic:
refine' Fin.ext _
Proof state after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 0 [ZMOD ↑p]
⊢ ↑k = ↑⟨0, ⋯⟩
Theorem: FltRegular.CaseI.aux_cong1k₁
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 0 [ZMOD ↑p]
⊢ ↑k = ↑⟨0, ⋯⟩
Tactic:
rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
Proof state after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 0 [ZMOD ↑p]
⊢ (↑↑k).val = ↑⟨0, ⋯⟩
Theorem: FltRegular.CaseI.aux_cong1k₁
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 0 [ZMOD ↑p]
⊢ (↑↑k).val = ↑⟨0, ⋯⟩
Tactic:
suffices ((k : ℤ) : ZMod p).val = 0 by simpa
Proof state after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 0 [ZMOD ↑p]
⊢ (↑↑↑k).val = 0
Theorem: FltRegular.CaseI.aux_cong1k₁
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 0 [ZMOD ↑p]
⊢ (↑↑↑k).val = 0
Tactic:
rw [← ZMod.intCast_eq_intCast_iff] at hcong
Proof state after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑0
⊢ (↑↑↑k).val = 0
Theorem: FltRegular.CaseI.aux_cong1k₁
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑0
⊢ (↑↑↑k).val = 0
Tactic:
rw [hcong, Int.cast_zero]
Proof state after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑0
⊢ ZMod.val 0 = 0
Theorem: FltRegular.CaseI.aux_cong1k₁
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑0
⊢ ZMod.val 0 = 0
Tactic:
haveI : Fact p.Prime := ⟨hpri⟩
Proof state after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑0
this : Fact p.Prime
⊢ ZMod.val 0 = 0
Theorem: FltRegular.CaseI.aux_cong1k₁
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑0
this : Fact p.Prime
⊢ ZMod.val 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux_cong1k₁
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 0 [ZMOD ↑p]
this : (↑↑↑k).val = 0
⊢ (↑↑k).val = ↑⟨0, ⋯⟩
Tactic:
simpa
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux1k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
⊢ 1 ≠ ↑k₁
Tactic:
intro habs
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : 1 = ↑k₁
⊢ False
Theorem: FltRegular.CaseI.aux1k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : 1 = ↑k₁
⊢ False
Tactic:
have h := aux0k₂ hpri hp5 hζ hab hcong hdiv
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : 1 = ↑k₁
h : 0 ≠ ↑k₂
⊢ False
Theorem: FltRegular.CaseI.aux1k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : 1 = ↑k₁
h : 0 ≠ ↑k₂
⊢ False
Tactic:
rw [show (k₁ : ℤ) = 1 by simpa using habs.symm, sub_self] at hcong
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ 0 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : 1 = ↑k₁
h : 0 ≠ ↑k₂
⊢ False
Theorem: FltRegular.CaseI.aux1k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ 0 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : 1 = ↑k₁
h : 0 ≠ ↑k₂
⊢ False
Tactic:
have := aux_cong1k₁ hpri hcong
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ 0 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : 1 = ↑k₁
h : 0 ≠ ↑k₂
this : k₂ = ⟨0, ⋯⟩
⊢ False
Theorem: FltRegular.CaseI.aux1k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ 0 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : 1 = ↑k₁
h : 0 ≠ ↑k₂
this : k₂ = ⟨0, ⋯⟩
⊢ False
Tactic:
simp only [← Fin.val_eq_val, Fin.val_mk] at this
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ 0 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : 1 = ↑k₁
h : 0 ≠ ↑k₂
this : ↑k₂ = 0
⊢ False
Theorem: FltRegular.CaseI.aux1k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ 0 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : 1 = ↑k₁
h : 0 ≠ ↑k₂
this : ↑k₂ = 0
⊢ False
Tactic:
exact h.symm this
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux1k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : 1 = ↑k₁
h : 0 ≠ ↑k₂
⊢ ↑↑k₁ = 1
Tactic:
simpa using habs.symm
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux_cong1k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑k ≡ 1 + 1 [ZMOD ↑p]
⊢ k = ⟨2, ⋯⟩
Tactic:
refine' Fin.ext _
Proof state after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑k ≡ 1 + 1 [ZMOD ↑p]
⊢ ↑k = ↑⟨2, ⋯⟩
Theorem: FltRegular.CaseI.aux_cong1k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑k ≡ 1 + 1 [ZMOD ↑p]
⊢ ↑k = ↑⟨2, ⋯⟩
Tactic:
rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
Proof state after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑k ≡ 1 + 1 [ZMOD ↑p]
⊢ (↑↑k).val = ↑⟨2, ⋯⟩
Theorem: FltRegular.CaseI.aux_cong1k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑k ≡ 1 + 1 [ZMOD ↑p]
⊢ (↑↑k).val = ↑⟨2, ⋯⟩
Tactic:
suffices ((k : ℤ) : ZMod p).val = 2 by simpa
Proof state after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑k ≡ 1 + 1 [ZMOD ↑p]
⊢ (↑↑↑k).val = 2
Theorem: FltRegular.CaseI.aux_cong1k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑k ≡ 1 + 1 [ZMOD ↑p]
⊢ (↑↑↑k).val = 2
Tactic:
rw [← ZMod.intCast_eq_intCast_iff] at hcong
Proof state after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑↑↑k).val = 2
Theorem: FltRegular.CaseI.aux_cong1k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑↑↑k).val = 2
Tactic:
rw [hcong]
Proof state after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑(1 + 1)).val = 2
Theorem: FltRegular.CaseI.aux_cong1k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑(1 + 1)).val = 2
Tactic:
simp only [Int.cast_add, algebraMap.coe_one]
Proof state after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑1 + ↑1).val = 2
Theorem: FltRegular.CaseI.aux_cong1k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑1 + ↑1).val = 2
Tactic:
haveI : Fact p.Prime := ⟨hpri⟩
Proof state after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this : Fact p.Prime
⊢ (↑1 + ↑1).val = 2
Theorem: FltRegular.CaseI.aux_cong1k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this : Fact p.Prime
⊢ (↑1 + ↑1).val = 2
Tactic:
have := congr_arg Nat.succ (Nat.succ_pred_eq_of_pos hpri.pred_pos)
Proof state after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p.pred.succ
⊢ (↑1 + ↑1).val = 2
Theorem: FltRegular.CaseI.aux_cong1k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p.pred.succ
⊢ (↑1 + ↑1).val = 2
Tactic:
rw [succ_pred_prime hpri] at this
Proof state after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p
⊢ (↑1 + ↑1).val = 2
Theorem: FltRegular.CaseI.aux_cong1k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p
⊢ (↑1 + ↑1).val = 2
Tactic:
rw [ZMod.val_add, Int.cast_one, ZMod.val_one, ← Nat.mod_add_mod, ← this, one_mod, this,
  Nat.mod_eq_of_lt]
Proof state after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p
⊢ 1 + 1 < p
Theorem: FltRegular.CaseI.aux_cong1k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p
⊢ 1 + 1 < p
Tactic:
linarith
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux_cong1k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑k ≡ 1 + 1 [ZMOD ↑p]
this : (↑↑↑k).val = 2
⊢ (↑↑k).val = ↑⟨2, ⋯⟩
Tactic:
simpa
Proof state after:
no goals
Theorem: FltRegular.CaseI.auxf1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a : ℤ
⊢ ∃ i, f1k₂ a ↑i = 0
Tactic:
refine' ⟨⟨1, hpri.one_lt⟩, _⟩
Proof state after:
p : ℕ
hpri : p.Prime
a : ℤ
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0
Theorem: FltRegular.CaseI.auxf1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a : ℤ
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0
Tactic:
have h2 : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 2 :=
  by
  intro h
  simp only [Fin.ext_iff, Fin.val_mk] at h; contradiction
Proof state after:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0
Theorem: FltRegular.CaseI.auxf1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0
Tactic:
have hzero : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 0 :=
  by
  intro h
  simp only [Fin.ext_iff, Fin.val_mk] at h
Proof state after:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
hzero : ↑⟨1, ⋯⟩ ≠ 0
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0
Theorem: FltRegular.CaseI.auxf1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
hzero : ↑⟨1, ⋯⟩ ≠ 0
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0
Tactic:
simp only [f1k₂, h2, if_false, hzero, one_lt_two.ne]
Proof state after:
no goals
Theorem: FltRegular.CaseI.auxf1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a : ℤ
⊢ ↑⟨1, ⋯⟩ ≠ 2
Tactic:
intro h
Proof state after:
p : ℕ
hpri : p.Prime
a : ℤ
h : ↑⟨1, ⋯⟩ = 2
⊢ False
Theorem: FltRegular.CaseI.auxf1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a : ℤ
h : ↑⟨1, ⋯⟩ = 2
⊢ False
Tactic:
simp only [Fin.ext_iff, Fin.val_mk] at h
Proof state after:
p : ℕ
hpri : p.Prime
a : ℤ
h : 1 = 2
⊢ False
Theorem: FltRegular.CaseI.auxf1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a : ℤ
h : 1 = 2
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: FltRegular.CaseI.auxf1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
⊢ ↑⟨1, ⋯⟩ ≠ 0
Tactic:
intro h
Proof state after:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
h : ↑⟨1, ⋯⟩ = 0
⊢ False
Theorem: FltRegular.CaseI.auxf1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
h : ↑⟨1, ⋯⟩ = 0
⊢ False
Tactic:
simp only [Fin.ext_iff, Fin.val_mk] at h
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
⊢ 1 ≠ ↑k₂
Tactic:
haveI := (⟨hpri⟩ : Fact (P : ℕ).Prime)
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ 1 ≠ ↑k₂
Theorem: FltRegular.CaseI.aux1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ 1 ≠ ↑k₂
Tactic:
symm
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ ↑k₂ ≠ 1
Theorem: FltRegular.CaseI.aux1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ ↑k₂ ≠ 1
Tactic:
intro habs
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
⊢ False
Theorem: FltRegular.CaseI.aux1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
⊢ False
Tactic:
replace hcong := hcong.symm
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ - 1 ≡ ↑↑k₂ [ZMOD ↑p]
⊢ False
Theorem: FltRegular.CaseI.aux1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ - 1 ≡ ↑↑k₂ [ZMOD ↑p]
⊢ False
Tactic:
rw [show (k₂ : ℤ) = 1 by simpa using habs, ← ZMod.intCast_eq_intCast_iff, Int.cast_sub,
  sub_eq_iff_eq_add, ← Int.cast_add, ZMod.intCast_eq_intCast_iff] at hcong
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
⊢ False
Theorem: FltRegular.CaseI.aux1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
⊢ False
Tactic:
rw [habs, pow_one, aux_cong1k₂ hpri hp5 hcong] at hdiv
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑⟨2, ⋯⟩ - ↑b * ζ
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
⊢ False
Theorem: FltRegular.CaseI.aux1k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑⟨2, ⋯⟩ - ↑b * ζ
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
⊢ False
Tactic:
ring_nf at hdiv
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ False