internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Tactic:
haveI : Fact (PNat.Prime ⟨p, hpri.out.pos⟩) := hpri
Proof state after:
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this : Fact (PNat.Prime ⟨p, ⋯⟩)
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this : Fact (PNat.Prime ⟨p, ⋯⟩)
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Tactic:
haveI := CyclotomicField.isCyclotomicExtension ⟨p, hpri.out.pos⟩ ℚ
Proof state after:
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝ : Fact (PNat.Prime ⟨p, ⋯⟩)
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝ : Fact (PNat.Prime ⟨p, ⋯⟩)
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Tactic:
obtain ⟨ζ, hζ⟩ := IsCyclotomicExtension.exists_prim_root
  ℚ (B := (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)) (Set.mem_singleton (⟨p, hpri.out.pos⟩ : ℕ+))
Proof state after:
case intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝ : Fact (PNat.Prime ⟨p, ⋯⟩)
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
case intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝ : Fact (PNat.Prime ⟨p, ⋯⟩)
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Tactic:
have hodd' : (⟨p, hpri.out.pos⟩ : ℕ+) ≠ (2 : ℕ+) := by
  rwa [← PNat.coe_injective.ne_iff]
Proof state after:
case intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝ : Fact (PNat.Prime ⟨p, ⋯⟩)
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
case intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝ : Fact (PNat.Prime ⟨p, ⋯⟩)
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Tactic:
have := fun n ↦ zeta_sub_one_dvd_Int_iff (K := CyclotomicField ⟨p, hpri.out.pos⟩ ℚ) hζ (n := n)
Proof state after:
case intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑↑⟨p, ⋯⟩ ∣ n
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
case intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑↑⟨p, ⋯⟩ ∣ n
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Tactic:
simp only [PNat.mk_coe] at this
Proof state after:
case intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
case intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
⊢ ¬∃ x y z, ¬↑p ∣ y ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Tactic:
simp_rw [← this]
Proof state after:
case intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
⊢ ¬∃ x y z, ¬↑hζ.unit' - 1 ∣ ↑y ∧ ↑hζ.unit' - 1 ∣ ↑z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
case intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
⊢ ¬∃ x y z, ¬↑hζ.unit' - 1 ∣ ↑y ∧ ↑hζ.unit' - 1 ∣ ↑z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Tactic:
rintro ⟨x, y, z, hy, hz, hz', e⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
x y z : ℤ
hy : ¬↑hζ.unit' - 1 ∣ ↑y
hz : ↑hζ.unit' - 1 ∣ ↑z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ False
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
x y z : ℤ
hy : ¬↑hζ.unit' - 1 ∣ ↑y
hz : ↑hζ.unit' - 1 ∣ ↑z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ False
Tactic:
refine not_exists_solution' (K := CyclotomicField ⟨p, hpri.out.pos⟩ ℚ) hodd' ?_
  hζ ⟨x, y, z, hy, hz, ?_, ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.refine_1
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
x y z : ℤ
hy : ¬↑hζ.unit' - 1 ∣ ↑y
hz : ↑hζ.unit' - 1 ∣ ↑z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ (↑⟨p, ⋯⟩).Coprime (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))))

case intro.intro.intro.intro.intro.intro.intro.refine_2
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
x y z : ℤ
hy : ¬↑hζ.unit' - 1 ∣ ↑y
hz : ↑hζ.unit' - 1 ∣ ↑z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ ↑z ≠ 0

case intro.intro.intro.intro.intro.intro.intro.refine_3
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
x y z : ℤ
hy : ¬↑hζ.unit' - 1 ∣ ↑y
hz : ↑hζ.unit' - 1 ∣ ↑z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ ↑x ^ ↑⟨p, ⋯⟩ + ↑y ^ ↑⟨p, ⋯⟩ = ↑z ^ ↑⟨p, ⋯⟩
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝ : Fact (PNat.Prime ⟨p, ⋯⟩)
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
⊢ ⟨p, ⋯⟩ ≠ 2
Tactic:
rwa [← PNat.coe_injective.ne_iff]
Proof state after:
no goals
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.refine_1
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
x y z : ℤ
hy : ¬↑hζ.unit' - 1 ∣ ↑y
hz : ↑hζ.unit' - 1 ∣ ↑z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ (↑⟨p, ⋯⟩).Coprime (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))))
Tactic:
convert hreg
Proof state after:
no goals
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.refine_2
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
x y z : ℤ
hy : ¬↑hζ.unit' - 1 ∣ ↑y
hz : ↑hζ.unit' - 1 ∣ ↑z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ ↑z ≠ 0
Tactic:
rwa [ne_eq, Int.cast_eq_zero]
Proof state after:
no goals
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.refine_3
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
x y z : ℤ
hy : ¬↑hζ.unit' - 1 ∣ ↑y
hz : ↑hζ.unit' - 1 ∣ ↑z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ ↑x ^ ↑⟨p, ⋯⟩ + ↑y ^ ↑⟨p, ⋯⟩ = ↑z ^ ↑⟨p, ⋯⟩
Tactic:
dsimp
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.refine_3
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
x y z : ℤ
hy : ¬↑hζ.unit' - 1 ∣ ↑y
hz : ↑hζ.unit' - 1 ∣ ↑z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ ↑x ^ p + ↑y ^ p = ↑z ^ p
Theorem: FltRegular.not_exists_Int_solution
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.refine_3
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
this✝¹ : Fact (PNat.Prime ⟨p, ⋯⟩)
this✝ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
ζ : CyclotomicField ⟨p, ⋯⟩ ℚ
hζ : IsPrimitiveRoot ζ ↑⟨p, ⋯⟩
hodd' : ⟨p, ⋯⟩ ≠ 2
this : ∀ (n : ℤ), ↑hζ.unit' - 1 ∣ ↑n ↔ ↑p ∣ n
x y z : ℤ
hy : ¬↑hζ.unit' - 1 ∣ ↑y
hz : ↑hζ.unit' - 1 ∣ ↑z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ ↑x ^ p + ↑y ^ p = ↑z ^ p
Tactic:
simp_rw [← Int.cast_pow, ← Int.cast_add, e]
Proof state after:
no goals
Theorem: FltRegular.not_exists_Int_solution'
Proof state before:
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
⊢ ¬∃ x y z, {x, y, z}.gcd id = 1 ∧ ↑p ∣ z ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p
Tactic:
rintro ⟨x, y, z, hgcd, hz, hz', e⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
x y z : ℤ
hgcd : {x, y, z}.gcd id = 1
hz : ↑p ∣ z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ False
Theorem: FltRegular.not_exists_Int_solution'
Proof state before:
case intro.intro.intro.intro.intro.intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
x y z : ℤ
hgcd : {x, y, z}.gcd id = 1
hz : ↑p ∣ z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ False
Tactic:
refine not_exists_Int_solution hreg hodd ⟨x, y, z, ?_, hz, hz', e⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
x y z : ℤ
hgcd : {x, y, z}.gcd id = 1
hz : ↑p ∣ z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ ¬↑p ∣ y
Theorem: FltRegular.not_exists_Int_solution'
Proof state before:
case intro.intro.intro.intro.intro.intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
x y z : ℤ
hgcd : {x, y, z}.gcd id = 1
hz : ↑p ∣ z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
⊢ ¬↑p ∣ y
Tactic:
intro hy
Proof state after:
case intro.intro.intro.intro.intro.intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
x y z : ℤ
hgcd : {x, y, z}.gcd id = 1
hz : ↑p ∣ z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
hy : ↑p ∣ y
⊢ False
Theorem: FltRegular.not_exists_Int_solution'
Proof state before:
case intro.intro.intro.intro.intro.intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
x y z : ℤ
hgcd : {x, y, z}.gcd id = 1
hz : ↑p ∣ z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
hy : ↑p ∣ y
⊢ False
Tactic:
have := dvd_sub (dvd_pow hz hpri.out.ne_zero) (dvd_pow hy hpri.out.ne_zero)
Proof state after:
case intro.intro.intro.intro.intro.intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
x y z : ℤ
hgcd : {x, y, z}.gcd id = 1
hz : ↑p ∣ z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
hy : ↑p ∣ y
this : ↑p ∣ z ^ p - y ^ p
⊢ False
Theorem: FltRegular.not_exists_Int_solution'
Proof state before:
case intro.intro.intro.intro.intro.intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
x y z : ℤ
hgcd : {x, y, z}.gcd id = 1
hz : ↑p ∣ z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
hy : ↑p ∣ y
this : ↑p ∣ z ^ p - y ^ p
⊢ False
Tactic:
rw [← e, add_sub_cancel_right] at this
Proof state after:
case intro.intro.intro.intro.intro.intro
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
x y z : ℤ
hgcd : {x, y, z}.gcd id = 1
hz : ↑p ∣ z
hz' : z ≠ 0
e : x ^ p + y ^ p = z ^ p
hy : ↑p ∣ y
this : ↑p ∣ x ^ p
⊢ False