Theorem: exists_solution
Proof state before:
case 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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  ↑(u₁ * ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + ↑(u₂ * ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    ↑u₃ * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
refine ⟨_, _, _, _, _, _, ?_, ?_, ?_, this⟩
Proof state after:
case 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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  ↑(u₁ * ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + ↑(u₂ * ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    ↑u₃ * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ¬π ∣ α η₁ hη₁ * β η₂ hη₂

case 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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  ↑(u₁ * ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + ↑(u₂ * ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    ↑u₃ * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ¬π ∣ α η₂ hη₂ * β η₁ hη₁

case 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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  ↑(u₁ * ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + ↑(u₂ * ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    ↑u₃ * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ¬π ∣ β η₁ hη₁ * β η₂ hη₂