internlm/Lean-Github huggingface dataset:
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro
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
⊢ False
Tactic:
have hel2 : ∃ v : Rˣ, (v : R) * x * (1 - η₁) ∈ I := by
  obtain ⟨v, hv⟩ := diff_of_roots2 ph hη₁ hη₂ hdiff hwlog
  refine ⟨v, ?_⟩
  have := Ideal.add_mem _ (mul_mem_left _ η₂ (mem_sup_left (mem_fltIdeals x y hη₁)))
      (mul_mem_left _ (-η₁) (mem_sup_right (mem_fltIdeals x y hη₂)))
  have h1 : η₂ * (↑x + η₁ * ↑y) + -η₁ * (↑x + η₂ * ↑y) = (η₂ - η₁) * x := by ring
  rwa [h1, hv, mul_right_comm] at this
Proof state after:
case a.intro.intro
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
⊢ False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro
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
⊢ False
Tactic:
have hel11 : (y : R) * (1 - η₁) ∈ P := by
  obtain ⟨v, hv⟩ := hel1
  rw [mul_assoc] at hv
  have hvunit : IsUnit (v : R) := Units.isUnit v
  apply (unit_mul_mem_iff_mem P hvunit).1 _
  apply hP2
  apply hv
Proof state after:
case a.intro.intro
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
⊢ False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro
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
⊢ False
Tactic:
have hel22 : (x : R) * (1 - η₁) ∈ P := by
  obtain ⟨v, hv⟩ := hel2
  rw [mul_assoc] at hv
  have hvunit : IsUnit (v : R) := Units.isUnit v
  apply (unit_mul_mem_iff_mem P hvunit).1 _
  apply hP2
  apply hv
Proof state after:
case a.intro.intro
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
⊢ False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro
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
⊢ False
Tactic:
have hPrime := hP1.isPrime
Proof state after:
case a.intro.intro
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
⊢ False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro
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
⊢ False
Tactic:
have hprime2 := IsPrime.mem_or_mem hPrime hel11
Proof state after:
case a.intro.intro
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
⊢ False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro
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
⊢ False
Tactic:
have hprime3 := IsPrime.mem_or_mem hPrime hel22
Proof state after:
case a.intro.intro
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
⊢ False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro
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
HC : 1 - η₁ ∈ P → False
⊢ False
Tactic:
cases' hprime2 with hprime2 hprime2
Proof state after:
case a.intro.intro.inl
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
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
HC : 1 - η₁ ∈ P → False
hprime2 : ↑y ∈ P
⊢ False

case a.intro.intro.inr
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
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
HC : 1 - η₁ ∈ P → False
hprime2 : 1 - η₁ ∈ P
⊢ False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro.inl.inr
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
HC : 1 - η₁ ∈ P → False
hprime2 : ↑y ∈ P
hprime3 : 1 - η₁ ∈ P
⊢ False

case a.intro.intro.inr
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
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
HC : 1 - η₁ ∈ P → False
hprime2 : 1 - η₁ ∈ P
⊢ False
Tactic:
apply HC hprime3
Proof state after:
case a.intro.intro.inr
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
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
HC : 1 - η₁ ∈ P → False
hprime2 : 1 - η₁ ∈ P
⊢ False
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro.inr
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
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
HC : 1 - η₁ ∈ P → False
hprime2 : 1 - η₁ ∈ P
⊢ False
Tactic:
apply HC hprime2
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
⊢ ∃ v, ↑v * ↑y * (1 - η₁) ∈ I
Tactic:
obtain ⟨v, hv⟩ := diff_of_roots ph hη₁ hη₂ hdiff hwlog
Proof state after:
case intro
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
v : (𝓞 (CyclotomicField p ℚ))ˣ
hv : η₁ - η₂ = ↑v * (1 - η₁)
⊢ ∃ v, ↑v * ↑y * (1 - η₁) ∈ I
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case intro
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
v : (𝓞 (CyclotomicField p ℚ))ˣ
hv : η₁ - η₂ = ↑v * (1 - η₁)
⊢ ∃ v, ↑v * ↑y * (1 - η₁) ∈ I
Tactic:
refine ⟨v, ?_⟩
Proof state after:
case intro
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
v : (𝓞 (CyclotomicField p ℚ))ˣ
hv : η₁ - η₂ = ↑v * (1 - η₁)
⊢ ↑v * ↑y * (1 - η₁) ∈ I
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case intro
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
v : (𝓞 (CyclotomicField p ℚ))ˣ
hv : η₁ - η₂ = ↑v * (1 - η₁)
⊢ ↑v * ↑y * (1 - η₁) ∈ I
Tactic:
have := Ideal.sub_mem _
  (mem_sup_left (mem_fltIdeals x y hη₁)) (mem_sup_right (mem_fltIdeals x y hη₂))
Proof state after:
case intro
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
v : (𝓞 (CyclotomicField p ℚ))ˣ
hv : η₁ - η₂ = ↑v * (1 - η₁)
this : ↑x + η₁ * ↑y - (↑x + η₂ * ↑y) ∈ fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
⊢ ↑v * ↑y * (1 - η₁) ∈ I
Theorem: fltIdeals_coprime2_lemma
Proof state before:
case intro
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
v : (𝓞 (CyclotomicField p ℚ))ˣ
hv : η₁ - η₂ = ↑v * (1 - η₁)
this : ↑x + η₁ * ↑y - (↑x + η₂ * ↑y) ∈ fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
⊢ ↑v * ↑y * (1 - η₁) ∈ I
Tactic:
rwa [add_sub_add_left_eq_sub, ← sub_mul, hv, mul_right_comm] at this
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
⊢ ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
Tactic:
obtain ⟨v, hv⟩ := diff_of_roots2 ph hη₁ hη₂ hdiff hwlog
Proof state after:
case intro
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
v : (𝓞 (CyclotomicField p ℚ))ˣ
hv : η₂ - η₁ = ↑v * (1 - η₁)
⊢ ∃ v, ↑v * ↑x * (1 - η₁) ∈ I