Theorem: fltIdeals_coprime (FltRegular/NumberTheory/Cyclotomic/CyclRat.lean)

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⟩
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η₂)

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
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η₂)

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
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η₂)

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
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η₂)

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
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η₂)

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
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η₁)

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
State after:
no goals

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
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

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
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

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
State after:
no goals