Theorem: FltRegular.not_exists_Int_solution' (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✝
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⟩
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

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

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

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

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

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

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

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

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