internlm/Lean-Github huggingface dataset:
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 ∣ x ^ p
⊢ False
Tactic:
replace this := (Nat.prime_iff_prime_int.mp hpri.out).dvd_of_dvd_pow 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
⊢ 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 ∣ x
⊢ False
Tactic:
apply (Nat.prime_iff_prime_int.mp hpri.out).not_unit
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
⊢ IsUnit ↑p
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 ∣ x
⊢ IsUnit ↑p
Tactic:
rw [isUnit_iff_dvd_one, ← hgcd]
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 ∣ {x, y, z}.gcd id
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 ∣ x
⊢ ↑p ∣ {x, y, z}.gcd id
Tactic:
simp [dvd_gcd_iff, hz, hy, this]
Proof state after:
no goals
Theorem: FltRegular.Int.gcd_left_comm
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
a b c : ℤ
⊢ a.gcd ↑(b.gcd c) = b.gcd ↑(a.gcd c)
Tactic:
rw [← Int.gcd_assoc, ← Int.gcd_assoc, Int.gcd_comm a b]
Proof state after:
no goals
Theorem: FltRegular.caseII
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
⊢ a ^ p + b ^ p ≠ c ^ p
Tactic:
intro e
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
⊢ False
Theorem: FltRegular.caseII
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
⊢ False
Tactic:
simp only [ne_eq, mul_eq_zero, not_or] at hprod
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
hprod : (¬a = 0 ∧ ¬b = 0) ∧ ¬c = 0
⊢ False
Theorem: FltRegular.caseII
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
hprod : (¬a = 0 ∧ ¬b = 0) ∧ ¬c = 0
⊢ False
Tactic:
obtain ⟨⟨a0, b0⟩, c0⟩ := hprod
Proof state after:
case 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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
⊢ False
Theorem: FltRegular.caseII
Proof state before:
case 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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
⊢ False
Tactic:
have hodd' := Nat.Prime.odd_of_ne_two hpri.out hodd
Proof state after:
case 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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
⊢ False
Theorem: FltRegular.caseII
Proof state before:
case 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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
⊢ False
Tactic:
obtain (hab|hc) := (Nat.prime_iff_prime_int.mp hpri.out).dvd_or_dvd caseII
Proof state after:
case intro.intro.inl
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
⊢ False

case intro.intro.inr
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hc : ↑p ∣ c
⊢ False
Theorem: FltRegular.caseII
Proof state before:
case intro.intro.inl
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
⊢ False

case intro.intro.inr
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hc : ↑p ∣ c
⊢ False
Tactic:
obtain (ha|hb) := (Nat.prime_iff_prime_int.mp hpri.out).dvd_or_dvd hab
Proof state after:
case intro.intro.inl.inl
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
ha : ↑p ∣ a
⊢ False

case intro.intro.inl.inr
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
hb : ↑p ∣ b
⊢ False

case intro.intro.inr
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hc : ↑p ∣ c
⊢ False
Theorem: FltRegular.caseII
Proof state before:
case intro.intro.inl.inl
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
ha : ↑p ∣ a
⊢ False
Tactic:
refine not_exists_Int_solution' hreg hodd ⟨b, -c, -a, ?_, ?_, ?_, ?_⟩
Proof state after:
case intro.intro.inl.inl.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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
ha : ↑p ∣ a
⊢ {b, -c, -a}.gcd id = 1

case intro.intro.inl.inl.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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
ha : ↑p ∣ a
⊢ ↑p ∣ -a

case intro.intro.inl.inl.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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
ha : ↑p ∣ a
⊢ -a ≠ 0

case intro.intro.inl.inl.refine_4
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
ha : ↑p ∣ a
⊢ b ^ p + (-c) ^ p = (-a) ^ p
Theorem: FltRegular.caseII
Proof state before:
case intro.intro.inl.inl.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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
ha : ↑p ∣ a
⊢ {b, -c, -a}.gcd id = 1
Tactic:
simp only [← hgcd, Finset.mem_singleton, Finset.mem_insert, neg_inj, Finset.gcd_insert, id_eq,
  ← Int.coe_gcd, Int.neg_gcd, Nat.cast_inj, ← insert_emptyc_eq, Finset.gcd_empty,
  Int.gcd_left_comm _ a]
Proof state after:
no goals
Theorem: FltRegular.caseII
Proof state before:
case intro.intro.inl.inl.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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
ha : ↑p ∣ a
⊢ ↑p ∣ -a
Tactic:
rwa [dvd_neg]
Proof state after:
no goals
Theorem: FltRegular.caseII
Proof state before:
case intro.intro.inl.inl.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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
ha : ↑p ∣ a
⊢ -a ≠ 0
Tactic:
rwa [ne_eq, neg_eq_zero]
Proof state after:
no goals
Theorem: FltRegular.caseII
Proof state before:
case intro.intro.inl.inl.refine_4
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
ha : ↑p ∣ a
⊢ b ^ p + (-c) ^ p = (-a) ^ p
Tactic:
simp [hodd'.neg_pow, ← e]
Proof state after:
no goals
Theorem: FltRegular.caseII
Proof state before:
case intro.intro.inl.inr
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
hb : ↑p ∣ b
⊢ False
Tactic:
refine not_exists_Int_solution' hreg hodd ⟨-c, a, -b, ?_, ?_, ?_, ?_⟩
Proof state after:
case intro.intro.inl.inr.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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
hb : ↑p ∣ b
⊢ {-c, a, -b}.gcd id = 1

case intro.intro.inl.inr.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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
hb : ↑p ∣ b
⊢ ↑p ∣ -b

case intro.intro.inl.inr.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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
hb : ↑p ∣ b
⊢ -b ≠ 0

case intro.intro.inl.inr.refine_4
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
hb : ↑p ∣ b
⊢ (-c) ^ p + a ^ p = (-b) ^ p
Theorem: FltRegular.caseII
Proof state before:
case intro.intro.inl.inr.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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
hb : ↑p ∣ b
⊢ {-c, a, -b}.gcd id = 1
Tactic:
simp only [← hgcd, Finset.mem_singleton, Finset.mem_insert, neg_inj, Finset.gcd_insert, id_eq,
  ← Int.coe_gcd, Int.neg_gcd, Nat.cast_inj, ← insert_emptyc_eq, Finset.gcd_empty,
  Int.gcd_left_comm _ c]
Proof state after:
no goals
Theorem: FltRegular.caseII
Proof state before:
case intro.intro.inl.inr.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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
hb : ↑p ∣ b
⊢ ↑p ∣ -b
Tactic:
rwa [dvd_neg]
Proof state after:
no goals
Theorem: FltRegular.caseII
Proof state before:
case intro.intro.inl.inr.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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
hb : ↑p ∣ b
⊢ -b ≠ 0
Tactic:
rwa [ne_eq, neg_eq_zero]
Proof state after:
no goals
Theorem: FltRegular.caseII
Proof state before:
case intro.intro.inl.inr.refine_4
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✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hab : ↑p ∣ a * b
hb : ↑p ∣ b
⊢ (-c) ^ p + a ^ p = (-b) ^ p
Tactic:
simp [hodd'.neg_pow, ← e]
Proof state after:
no goals