Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro.inl.inl.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 : η₁ ≠ η₂
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 : ↑x ∈ P
a b : ℤ
hab : a * x + b * y = 1
hone : P = ⊤
hcontra : ⊤ ≠ ⊤
⊢ False

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:
simp only [Ne, eq_self_iff_true, not_true] at hcontra
Proof state after:
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