internlm/Lean-Github huggingface dataset:
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
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ False
Tactic:
have key : ↑(p : ℤ) ∣ ∑ j in range p, f1k₂ a j • ζ ^ j := by
  suffices ∑ j in range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2 by
    rwa [this]
  simp_rw [f1k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right
    (show 0 ≠ 2 by norm_num), Finset.range_filter_eq]
  simp only [hpri.pos, ite_true, zsmul_eq_mul, sum_singleton, _root_.pow_zero, mul_one, two_lt hp5, neg_smul,
sum_neg_distrib, ne_eq, mem_range, not_and, not_not, zero_smul, sum_const_zero, add_zero]
  ring
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
key : ↑↑p ∣ ∑ j ∈ range p, f1k₂ a j • ζ ^ j
⊢ 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
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ j ∈ range p, f1k₂ a j • ζ ^ j
⊢ False
Tactic:
rw [sum_range] at key
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
key : ↑↑p ∣ ∑ i : Fin p, f1k₂ a ↑i • ζ ^ ↑i
⊢ 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
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ i : Fin p, f1k₂ a ↑i • ζ ^ ↑i
⊢ False
Tactic:
refine' caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right _ _) _)
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
key : ↑↑p ∣ ∑ i : Fin p, f1k₂ a ↑i • ζ ^ ↑i
⊢ ↑p ∣ a
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
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ i : Fin p, f1k₂ a ↑i • ζ ^ ↑i
⊢ ↑p ∣ a
Tactic:
have hpri₁ : (P : ℕ).Prime := hpri
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
key : ↑↑p ∣ ∑ i : Fin p, f1k₂ a ↑i • ζ ^ ↑i
hpri₁ : (↑⟨p, ⋯⟩).Prime
⊢ ↑p ∣ a
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
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
key : ↑↑p ∣ ∑ i : Fin p, f1k₂ a ↑i • ζ ^ ↑i
hpri₁ : (↑⟨p, ⋯⟩).Prime
⊢ ↑p ∣ a
Tactic:
simpa [f1k₂] using dvd_coeff_cycl_integer hpri₁ hζ (auxf1k₂ hpri a) key ⟨0, hpri.pos⟩
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
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ - 1 ≡ ↑↑k₂ [ZMOD ↑p]
⊢ ↑↑k₂ = 1
Tactic:
simpa using habs
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
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ ↑↑p ∣ ∑ j ∈ range p, f1k₂ a j • ζ ^ j
Tactic:
suffices ∑ j in range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2 by
  rwa [this]
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
⊢ ∑ j ∈ range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2
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
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ ∑ j ∈ range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2
Tactic:
simp_rw [f1k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right
  (show 0 ≠ 2 by norm_num), Finset.range_filter_eq]
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
⊢ ∑ x ∈ if 0 < p then {0} else ∅, a • ζ ^ x +
      (∑ x ∈ if 2 < p then {2} else ∅, -a • ζ ^ x + ∑ x ∈ filter (fun a => a ≠ 0 ∧ a ≠ 2) (range p), 0 • ζ ^ x) =
    ↑a - ↑a * ζ ^ 2
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
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ ∑ x ∈ if 0 < p then {0} else ∅, a • ζ ^ x +
      (∑ x ∈ if 2 < p then {2} else ∅, -a • ζ ^ x + ∑ x ∈ filter (fun a => a ≠ 0 ∧ a ≠ 2) (range p), 0 • ζ ^ x) =
    ↑a - ↑a * ζ ^ 2
Tactic:
simp only [hpri.pos, ite_true, zsmul_eq_mul, sum_singleton, _root_.pow_zero, mul_one, two_lt hp5, neg_smul,
sum_neg_distrib, ne_eq, mem_range, not_and, not_not, zero_smul, sum_const_zero, add_zero]
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
⊢ ↑a + -(↑a * ζ ^ 2) = ↑a - ↑a * ζ ^ 2
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
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ ↑a + -(↑a * ζ ^ 2) = ↑a - ↑a * ζ ^ 2
Tactic:
ring
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
this✝ : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
this : ∑ j ∈ range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2
⊢ ↑↑p ∣ ∑ j ∈ range p, f1k₂ a j • ζ ^ j
Tactic:
rwa [this]
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
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 1
hcong : ↑↑k₁ ≡ 1 + 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a - ↑a * ζ ^ 2
⊢ 0 ≠ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: FltRegular.CaseI.auxk₁k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
⊢ ↑k₁ ≠ ↑k₂
Tactic:
haveI := (⟨hpri⟩ : Fact p.Prime)
Proof state after:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
this : Fact p.Prime
⊢ ↑k₁ ≠ ↑k₂
Theorem: FltRegular.CaseI.auxk₁k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
this : Fact p.Prime
⊢ ↑k₁ ≠ ↑k₂
Tactic:
intro habs
Proof state after:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
this : Fact p.Prime
habs : ↑k₁ = ↑k₂
⊢ False
Theorem: FltRegular.CaseI.auxk₁k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
this : Fact p.Prime
habs : ↑k₁ = ↑k₂
⊢ False
Tactic:
rw [habs, ← ZMod.intCast_eq_intCast_iff, Int.cast_sub, ← sub_eq_zero] at hcong
Proof state after:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
this : Fact p.Prime
hcong : ↑↑↑k₂ - (↑↑↑k₂ - ↑1) = 0
habs : ↑k₁ = ↑k₂
⊢ False
Theorem: FltRegular.CaseI.auxk₁k₂
Proof state before:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
this : Fact p.Prime
hcong : ↑↑↑k₂ - (↑↑↑k₂ - ↑1) = 0
habs : ↑k₁ = ↑k₂
⊢ False
Tactic:
simp at hcong
Proof state after:
no goals
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
⊢ multiplicity.Finite x y
Tactic:
by_contra h
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
h : ¬multiplicity.Finite x y
⊢ False
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
h : ¬multiplicity.Finite x y
⊢ False
Tactic:
rw [multiplicity.Finite, not_exists_not] at h
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
h : ∀ (x_1 : ℕ), x ^ (x_1 + 1) ∣ y
⊢ False
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
h : ∀ (x_1 : ℕ), x ^ (x_1 + 1) ∣ y
⊢ False
Tactic:
choose f hf using h
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
⊢ False
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
⊢ False
Tactic:
obtain ⟨_, ⟨n, rfl⟩, hn⟩ :=
  (WfDvdMonoid.wellFounded_dvdNotUnit (α := M)).has_min (Set.range f) (Set.range_nonempty f)
Proof state after:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ False
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ False
Tactic:
apply hn _ ⟨n + 1, rfl⟩
Proof state after:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ DvdNotUnit (f (n + 1)) (f n)
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ DvdNotUnit (f (n + 1)) (f n)
Tactic:
constructor
Proof state after:
case intro.intro.intro.left
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ f (n + 1) ≠ 0

case intro.intro.intro.right
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ ∃ x, ¬IsUnit x ∧ f n = f (n + 1) * x
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
case intro.intro.intro.left
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ f (n + 1) ≠ 0
Tactic:
intro e
Proof state after:
case intro.intro.intro.left
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : f (n + 1) = 0
⊢ False
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
case intro.intro.intro.left
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : f (n + 1) = 0
⊢ False
Tactic:
apply hy
Proof state after:
case intro.intro.intro.left
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : f (n + 1) = 0
⊢ y = 0
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
case intro.intro.intro.left
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : f (n + 1) = 0
⊢ y = 0
Tactic:
rw [hf (n + 1), e, mul_zero]
Proof state after:
no goals
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
case intro.intro.intro.right
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ ∃ x, ¬IsUnit x ∧ f n = f (n + 1) * x
Tactic:
refine ⟨x, hx, ?_⟩
Proof state after:
case intro.intro.intro.right
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ f n = f (n + 1) * x
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
case intro.intro.intro.right
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ f n = f (n + 1) * x
Tactic:
rw [mul_comm, ← (mul_right_injective₀ (a := x ^ (n + 1)) _).eq_iff]
Proof state after:
case intro.intro.intro.right
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ x ^ (n + 1) * f n = x ^ (n + 1) * (x * f (n + 1))

K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ x ^ (n + 1) ≠ 0
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
case intro.intro.intro.right
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ x ^ (n + 1) * f n = x ^ (n + 1) * (x * f (n + 1))
Tactic:
simp only [← mul_assoc, ← pow_succ, ← hf]
Proof state after:
no goals
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
⊢ x ^ (n + 1) ≠ 0
Tactic:
intro e
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : x ^ (n + 1) = 0
⊢ False
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : x ^ (n + 1) = 0
⊢ False
Tactic:
apply hy
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : x ^ (n + 1) = 0
⊢ y = 0
Theorem: WfDvdMonoid.multiplicity_finite
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
hx : ¬IsUnit x
hy : y ≠ 0
f : ℕ → M
hf : ∀ (x_1 : ℕ), y = x ^ (x_1 + 1) * f x_1
n : ℕ
hn : ∀ x ∈ Set.range f, ¬DvdNotUnit x (f n)
e : x ^ (n + 1) = 0
⊢ y = 0
Tactic:
rw [hf n, e, zero_mul]
Proof state after:
no goals
Theorem: WfDvdMonoid.multiplicity_finite_iff
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
⊢ multiplicity.Finite x y ↔ ¬IsUnit x ∧ y ≠ 0
Tactic:
constructor
Proof state after:
case mp
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
⊢ multiplicity.Finite x y → ¬IsUnit x ∧ y ≠ 0

case mpr
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
⊢ ¬IsUnit x ∧ y ≠ 0 → multiplicity.Finite x y
Theorem: WfDvdMonoid.multiplicity_finite_iff
Proof state before:
case mp
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
⊢ multiplicity.Finite x y → ¬IsUnit x ∧ y ≠ 0
Tactic:
rw [← not_imp_not, Ne, ← not_or, not_not]
Proof state after:
case mp
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
⊢ IsUnit x ∨ y = 0 → ¬multiplicity.Finite x y