Theorem: exists_solution'_aux (FltRegular/CaseII/InductionStep.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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
⊢ ∃ a, ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
Tactic:
letI : Fact (Nat.Prime p) := hpri
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this : Fact (↑p).Prime := hpri
⊢ ∃ a, ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p

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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this : Fact (↑p).Prime := hpri
⊢ ∃ a, ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
Tactic:
obtain ⟨a, b, e⟩ : IsCoprime ↑p x := isCoprime_of_not_zeta_sub_one_dvd hζ hx
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
⊢ ∃ a, ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p

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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
⊢ ∃ a, ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
Tactic:
have : (p : 𝓞 K) ∣ b * x - 1 := by use -a ; rw [← e]; ring
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this✝ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this : ↑↑p ∣ b * x - 1
⊢ ∃ a, ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p

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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this✝ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this : ↑↑p ∣ b * x - 1
⊢ ∃ a, ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
Tactic:
have := (this.trans (sub_one_dvd_pow_sub_one _ p)).trans (dvd_mul_left _ ↑(ε₁ / ε₂))
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
⊢ ∃ a, ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p

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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
⊢ ∃ a, ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
Tactic:
use - y * b
State after:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
⊢ ↑↑p ∣ ↑(ε₁ / ε₂) - (-y * b) ^ ↑p

State before:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
⊢ ↑↑p ∣ ↑(ε₁ / ε₂) - (-y * b) ^ ↑p
Tactic:
replace h := (h.trans (dvd_mul_right _ (b ^ (p : ℕ)))).trans (dvd_mul_left _ ↑(ε₂⁻¹))
State after:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
h : ↑↑p ∣ ↑ε₂⁻¹ * ((↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p) * b ^ ↑p)
⊢ ↑↑p ∣ ↑(ε₁ / ε₂) - (-y * b) ^ ↑p

State before:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
h : ↑↑p ∣ ↑ε₂⁻¹ * ((↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p) * b ^ ↑p)
⊢ ↑↑p ∣ ↑(ε₁ / ε₂) - (-y * b) ^ ↑p
Tactic:
rw [add_mul, mul_assoc, mul_assoc, ← mul_pow, ← mul_pow, mul_add] at h
State after:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
h : ↑↑p ∣ ↑ε₂⁻¹ * (↑ε₁ * (x * b) ^ ↑p) + ↑ε₂⁻¹ * (↑ε₂ * (y * b) ^ ↑p)
⊢ ↑↑p ∣ ↑(ε₁ / ε₂) - (-y * b) ^ ↑p

State before:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
h : ↑↑p ∣ ↑ε₂⁻¹ * (↑ε₁ * (x * b) ^ ↑p) + ↑ε₂⁻¹ * (↑ε₂ * (y * b) ^ ↑p)
⊢ ↑↑p ∣ ↑(ε₁ / ε₂) - (-y * b) ^ ↑p
Tactic:
simp_rw [← mul_assoc, ← Units.val_mul] at h
State after:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
h : ↑↑p ∣ ↑(ε₂⁻¹ * ε₁) * (x * b) ^ ↑p + ↑(ε₂⁻¹ * ε₂) * (y * b) ^ ↑p
⊢ ↑↑p ∣ ↑(ε₁ / ε₂) - (-y * b) ^ ↑p

State before:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
h : ↑↑p ∣ ↑(ε₂⁻¹ * ε₁) * (x * b) ^ ↑p + ↑(ε₂⁻¹ * ε₂) * (y * b) ^ ↑p
⊢ ↑↑p ∣ ↑(ε₁ / ε₂) - (-y * b) ^ ↑p
Tactic:
rw [← mul_comm ε₁, ← div_eq_mul_inv, inv_mul_self, Units.val_one, one_mul] at h
State after:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
h : ↑↑p ∣ ↑(ε₁ / ε₂) * (x * b) ^ ↑p + (y * b) ^ ↑p
⊢ ↑↑p ∣ ↑(ε₁ / ε₂) - (-y * b) ^ ↑p

State before:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
h : ↑↑p ∣ ↑(ε₁ / ε₂) * (x * b) ^ ↑p + (y * b) ^ ↑p
⊢ ↑↑p ∣ ↑(ε₁ / ε₂) - (-y * b) ^ ↑p
Tactic:
convert dvd_sub h this using 1
State after:
case h.e'_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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
h : ↑↑p ∣ ↑(ε₁ / ε₂) * (x * b) ^ ↑p + (y * b) ^ ↑p
⊢ ↑(ε₁ / ε₂) - (-y * b) ^ ↑p = ↑(ε₁ / ε₂) * (x * b) ^ ↑p + (y * b) ^ ↑p - ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)

State before:
case h.e'_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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
this✝¹ : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
this✝ : ↑↑p ∣ b * x - 1
this : ↑↑p ∣ ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
h : ↑↑p ∣ ↑(ε₁ / ε₂) * (x * b) ^ ↑p + (y * b) ^ ↑p
⊢ ↑(ε₁ / ε₂) - (-y * b) ^ ↑p = ↑(ε₁ / ε₂) * (x * b) ^ ↑p + (y * b) ^ ↑p - ↑(ε₁ / ε₂) * ((b * x) ^ ↑p - 1)
Tactic:
rw [neg_mul, (Nat.Prime.odd_of_ne_two hpri.out (PNat.coe_injective.ne hp)).neg_pow,
  sub_neg_eq_add, mul_sub, mul_one, mul_comm x b, add_sub_sub_cancel, add_comm]
State after:
no goals

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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
⊢ ↑↑p ∣ b * x - 1
Tactic:
use -a
State after:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
⊢ b * x - 1 = ↑↑p * -a

State before:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
⊢ b * x - 1 = ↑↑p * -a
Tactic:
rw [← e]
State after:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
⊢ b * x - (a * ↑↑p + b * x) = ↑↑p * -a

State before:
case h
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e✝ : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this : Fact (↑p).Prime := hpri
a b : 𝓞 K
e : a * ↑↑p + b * x = 1
⊢ b * x - (a * ↑↑p + b * x) = ↑↑p * -a
Tactic:
ring
State after:
no goals