internlm/Lean-Github huggingface dataset:
Theorem: fltIdeals_coprime2_lemma
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h✝ : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
hiP : fltIdeals p x y hη₁ ≤ P
hel1 : ∃ v, ↑v * ↑y * (1 - η₁) ∈ I
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
hcapZ : comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
H1 : ↑x + ↑y + -↑y * (1 - η₁) ∈ P
H2 : η₁ * ↑y = ↑y - ↑y * (1 - η₁)
H3 : ↑x + (↑y - ↑y * (1 - η₁)) = ↑x + ↑y + -↑y * (1 - η₁)
⊢ -↑y * (1 - η₁) ∈ span {1 - η₁}
Tactic:
rw [Ideal.mem_span_singleton']
Proof state after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h✝ : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
hiP : fltIdeals p x y hη₁ ≤ P
hel1 : ∃ v, ↑v * ↑y * (1 - η₁) ∈ I
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
hcapZ : comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
H1 : ↑x + ↑y + -↑y * (1 - η₁) ∈ P
H2 : η₁ * ↑y = ↑y - ↑y * (1 - η₁)
H3 : ↑x + (↑y - ↑y * (1 - η₁)) = ↑x + ↑y + -↑y * (1 - η₁)
⊢ ∃ a, a * (1 - η₁) = -↑y * (1 - η₁)
Theorem: fltIdeals_coprime2_lemma
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h✝ : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
hiP : fltIdeals p x y hη₁ ≤ P
hel1 : ∃ v, ↑v * ↑y * (1 - η₁) ∈ I
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
hcapZ : comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
H1 : ↑x + ↑y + -↑y * (1 - η₁) ∈ P
H2 : η₁ * ↑y = ↑y - ↑y * (1 - η₁)
H3 : ↑x + (↑y - ↑y * (1 - η₁)) = ↑x + ↑y + -↑y * (1 - η₁)
⊢ ∃ a, a * (1 - η₁) = -↑y * (1 - η₁)
Tactic:
refine' ⟨-(y : R), rfl⟩
Proof state after:
no goals
Theorem: fltIdeals_coprime2_lemma
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h✝ : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
hiP : fltIdeals p x y hη₁ ≤ P
hel1 : ∃ v, ↑v * ↑y * (1 - η₁) ∈ I
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
hcapZ : comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
hxyinP : ↑x + ↑y ∈ P
⊢ x + y ∈ span {↑↑p}
Tactic:
rw [← hcapZ]
Proof state after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h✝ : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
hiP : fltIdeals p x y hη₁ ≤ P
hel1 : ∃ v, ↑v * ↑y * (1 - η₁) ∈ I
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
hcapZ : comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
hxyinP : ↑x + ↑y ∈ P
⊢ x + y ∈ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P
Theorem: fltIdeals_coprime2_lemma
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h✝ : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
hiP : fltIdeals p x y hη₁ ≤ P
hel1 : ∃ v, ↑v * ↑y * (1 - η₁) ∈ I
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
h : 1 - η₁ ∈ P
eta_sub_one_ne_zero : 1 - η₁ ≠ 0
hηprime : (span {1 - η₁}).IsPrime
H5 : (span {↑↑p}).IsPrime
hηP : span {1 - η₁} = P
hcapZ : comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P = span {↑↑p}
hxyinP : ↑x + ↑y ∈ P
⊢ x + y ∈ comap (Int.castRingHom (𝓞 (CyclotomicField p ℚ))) P
Tactic:
simp [hxyinP]
Proof state after:
no goals
Theorem: fltIdeals_coprime2
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
⊢ IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Tactic:
apply not_not.mp
Proof state after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
⊢ ¬¬IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Theorem: fltIdeals_coprime2
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
⊢ ¬¬IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Tactic:
rw [not_coprime_not_top, not_not]
Proof state after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
⊢ fltIdeals p x y hη₁ + fltIdeals p x y hη₂ = ⊤
Theorem: fltIdeals_coprime2
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
⊢ fltIdeals p x y hη₁ + fltIdeals p x y hη₂ = ⊤
Tactic:
exact fltIdeals_coprime2_lemma ph hη₁ hη₂ hdiff hp hp2 hwlog
Proof state after:
no goals
Theorem: aux_lem_flt
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
⊢ ¬↑↑p ∣ x + y
Tactic:
intro habs
Proof state after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
habs : ↑↑p ∣ x + y
⊢ False
Theorem: aux_lem_flt
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
habs : ↑↑p ∣ x + y
⊢ False
Tactic:
rw [← ZMod.intCast_zmod_eq_zero_iff_dvd, Int.cast_add] at habs
Proof state after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
⊢ False
Theorem: aux_lem_flt
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
⊢ False
Tactic:
replace H := congr_arg (fun x : ℤ => (x : ZMod p)) H.symm
Proof state after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
H : (fun x => ↑x) (z ^ ↑p) = (fun x => ↑x) (x ^ ↑p + y ^ ↑p)
⊢ False
Theorem: aux_lem_flt
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
H : (fun x => ↑x) (z ^ ↑p) = (fun x => ↑x) (x ^ ↑p + y ^ ↑p)
⊢ False
Tactic:
simp only [Int.cast_add, Int.cast_pow, ZMod.pow_card, habs,
  ZMod.intCast_zmod_eq_zero_iff_dvd] at H
Proof state after:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
H : ↑↑p ∣ z
⊢ False
Theorem: aux_lem_flt
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
H : ↑↑p ∣ z
⊢ False
Tactic:
exact caseI (Dvd.dvd.mul_left H _)
Proof state after:
no goals
Theorem: aux_lem_flt
Proof state before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
habs : ↑↑p ∣ x + y
⊢ ↑↑p ∣ x + y
Tactic:
simpa using habs
Proof state after:
no goals
Theorem: fltIdeals_coprime
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Tactic:
have : Fact (p : ℕ).Prime := ⟨hpri⟩
Proof state after:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Theorem: fltIdeals_coprime
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Tactic:
by_cases h : η₁ ≠ 1
Proof state after:
case pos
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : η₁ ≠ 1
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)

case neg
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : ¬η₁ ≠ 1
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Theorem: fltIdeals_coprime
Proof state before:
case pos
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : η₁ ≠ 1
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)

case neg
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : ¬η₁ ≠ 1
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Tactic:
apply fltIdeals_coprime2 p5 hη₁ hη₂ hdiff hxy (aux_lem_flt H caseI) h
Proof state after:
case neg
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : ¬η₁ ≠ 1
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Theorem: fltIdeals_coprime
Proof state before:
case neg
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : ¬η₁ ≠ 1
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Tactic:
have h2 : η₂ ≠ 1 := by
  simp at h
  rw [h] at hdiff
  exact hdiff.symm
Proof state after:
case neg
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : ¬η₁ ≠ 1
h2 : η₂ ≠ 1
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Theorem: fltIdeals_coprime
Proof state before:
case neg
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : ¬η₁ ≠ 1
h2 : η₂ ≠ 1
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Tactic:
have := fltIdeals_coprime2 p5 hη₂ hη₁ hdiff.symm hxy (aux_lem_flt H caseI) h2
Proof state after:
case neg
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this✝ : Fact (↑p).Prime
h : ¬η₁ ≠ 1
h2 : η₂ ≠ 1
this : IsCoprime (fltIdeals p x y hη₂) (fltIdeals p x y hη₁)
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Theorem: fltIdeals_coprime
Proof state before:
case neg
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this✝ : Fact (↑p).Prime
h : ¬η₁ ≠ 1
h2 : η₂ ≠ 1
this : IsCoprime (fltIdeals p x y hη₂) (fltIdeals p x y hη₁)
⊢ let_fun this := ⋯;
  IsCoprime (fltIdeals p x y hη₁) (fltIdeals p x y hη₂)
Tactic:
apply IsCoprime.symm
Proof state after:
case neg.H
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this✝ : Fact (↑p).Prime
h : ¬η₁ ≠ 1
h2 : η₂ ≠ 1
this : IsCoprime (fltIdeals p x y hη₂) (fltIdeals p x y hη₁)
⊢ IsCoprime (fltIdeals p x y hη₂) (fltIdeals p x y hη₁)
Theorem: fltIdeals_coprime
Proof state before:
case neg.H
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this✝ : Fact (↑p).Prime
h : ¬η₁ ≠ 1
h2 : η₂ ≠ 1
this : IsCoprime (fltIdeals p x y hη₂) (fltIdeals p x y hη₁)
⊢ IsCoprime (fltIdeals p x y hη₂) (fltIdeals p x y hη₁)
Tactic:
exact this
Proof state after:
no goals
Theorem: fltIdeals_coprime
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : ¬η₁ ≠ 1
⊢ η₂ ≠ 1
Tactic:
simp at h
Proof state after:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : η₁ = 1
⊢ η₂ ≠ 1
Theorem: fltIdeals_coprime
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : η₁ = 1
⊢ η₂ ≠ 1
Tactic:
rw [h] at hdiff
Proof state after:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : 1 ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : η₁ = 1
⊢ η₂ ≠ 1
Theorem: fltIdeals_coprime
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hpri : (↑p).Prime
p5 : 5 ≤ p
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hxy : IsCoprime x y
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : 1 ≠ η₂
caseI : ¬↑↑p ∣ x * y * z
this : Fact (↑p).Prime
h : η₁ = 1
⊢ η₂ ≠ 1
Tactic:
exact hdiff.symm
Proof state after:
no goals
Theorem: dvd_last_coeff_cycl_integer
Proof state before:
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
⊢ m ∣ f ⟨(↑p).pred, ⋯⟩
Tactic:
obtain ⟨i, Hi⟩ := hf
Proof state after:
case intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
i : Fin ↑p
Hi : f i = 0
⊢ m ∣ f ⟨(↑p).pred, ⋯⟩
Theorem: dvd_last_coeff_cycl_integer
Proof state before:
case intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
i : Fin ↑p
Hi : f i = 0
⊢ m ∣ f ⟨(↑p).pred, ⋯⟩
Tactic:
have hlast :
  (Fin.castOrderIso (succ_pred_prime hp.out)) (Fin.last (p : ℕ).pred) =
  ⟨(p : ℕ).pred, pred_lt hp.out.ne_zero⟩ := Fin.ext rfl
Proof state after:
case intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
i : Fin ↑p
Hi : f i = 0
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
⊢ m ∣ f ⟨(↑p).pred, ⋯⟩