Theorem: FltRegular.caseII (FltRegular/CaseII/Statement.lean)

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

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

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

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

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

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

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, ?_, ?_, ?_, ?_⟩
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

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

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

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

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

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, ?_, ?_, ?_, ?_⟩
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

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

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

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

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

State before:
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:
exact not_exists_Int_solution' hreg hodd ⟨a, b, c, hgcd, hc, c0, e⟩
State after:
no goals