by_cases h : η₁ ≠ 1
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η₂)
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η₂)