internlm/Lean-Github huggingface dataset:
Theorem: x_plus_y_mul_ne_zero
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : x + y * ↑η = 0
⊢ x + y * ↑η ∣ x ^ ↑p + y ^ ↑p
Tactic:
rw [pow_add_pow_eq_prod_add_zeta_runity_mul
  (hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)) hζ.unit'_coe]
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : x + y * ↑η = 0
⊢ x + y * ↑η ∣ ∏ ζ ∈ nthRootsFinset (↑p) (𝓞 K), (x + ζ * y)
Theorem: x_plus_y_mul_ne_zero
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : x + y * ↑η = 0
⊢ x + y * ↑η ∣ ∏ ζ ∈ nthRootsFinset (↑p) (𝓞 K), (x + ζ * y)
Tactic:
simp_rw [mul_comm _ y]
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : x + y * ↑η = 0
⊢ x + y * ↑η ∣ ∏ x_1 ∈ nthRootsFinset (↑p) (𝓞 K), (x + y * x_1)
Theorem: x_plus_y_mul_ne_zero
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : x + y * ↑η = 0
⊢ x + y * ↑η ∣ ∏ x_1 ∈ nthRootsFinset (↑p) (𝓞 K), (x + y * x_1)
Tactic:
exact Finset.dvd_prod_of_mem _ η.prop
Proof state after:
no goals
Theorem: stuff
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (↑η₂ - ↑η₀) * ↑(ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + (↑η₀ - ↑η₁) * ↑(ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    (↑η₂ - ↑η₁) * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
Tactic:
rw [← mul_right_inj' (x_plus_y_mul_ne_zero hp hζ e hz η₀), mul_add]
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (x + y * ↑η₀) * ((↑η₂ - ↑η₀) * ↑(ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p) +
      (x + y * ↑η₀) * ((↑η₀ - ↑η₁) * ↑(ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p) =
    (x + y * ↑η₀) * ((↑η₂ - ↑η₁) * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p)
Theorem: stuff
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (x + y * ↑η₀) * ((↑η₂ - ↑η₀) * ↑(ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p) +
      (x + y * ↑η₀) * ((↑η₀ - ↑η₁) * ↑(ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p) =
    (x + y * ↑η₀) * ((↑η₂ - ↑η₁) * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p)
Tactic:
simp_rw [mul_left_comm (x + y * η₀), mul_pow, mul_assoc, mul_left_comm (η₂ - η₀ : 𝓞 K),
  mul_left_comm (η₀ - η₁ : 𝓞 K), ← mul_assoc,
  associated_eta_zero_unit_spec, mul_assoc, ← mul_left_comm (η₂ - η₀ : 𝓞 K),
  ← mul_left_comm (η₀ - η₁ : 𝓞 K), pow_mul, ← mul_pow, mul_comm (β η₂ hη₂), ← mul_assoc]
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (↑η₂ - ↑η₀) * (x + y * ↑η₁) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p +
      (↑η₀ - ↑η₁) * (x + y * ↑η₂) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p =
    (↑η₂ - ↑η₁) * (x + y * ↑η₀) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p
Theorem: stuff
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (↑η₂ - ↑η₀) * (x + y * ↑η₁) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p +
      (↑η₀ - ↑η₁) * (x + y * ↑η₂) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p =
    (↑η₂ - ↑η₁) * (x + y * ↑η₀) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p
Tactic:
rw [← add_mul]
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ ((↑η₂ - ↑η₀) * (x + y * ↑η₁) + (↑η₀ - ↑η₁) * (x + y * ↑η₂)) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p =
    (↑η₂ - ↑η₁) * (x + y * ↑η₀) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p
Theorem: stuff
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ ((↑η₂ - ↑η₀) * (x + y * ↑η₁) + (↑η₀ - ↑η₁) * (x + y * ↑η₂)) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p =
    (↑η₂ - ↑η₁) * (x + y * ↑η₀) * (π ^ m * β η₁ hη₁ * β η₂ hη₂) ^ ↑p
Tactic:
congr 1
Proof state after:
case e_a
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) }
hη₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (↑η₂ - ↑η₀) * (x + y * ↑η₁) + (↑η₀ - ↑η₁) * (x + y * ↑η₂) = (↑η₂ - ↑η₁) * (x + y * ↑η₀)
Theorem: stuff
Proof state before:
case e_a
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) }
hη₁ : η₁ ≠ η₀
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη₂ : η₂ ≠ η₀
⊢ (↑η₂ - ↑η₀) * (x + y * ↑η₁) + (↑η₀ - ↑η₁) * (x + y * ↑η₂) = (↑η₂ - ↑η₁) * (x + y * ↑η₀)
Tactic:
ring
Proof state after:
no goals
Theorem: exists_solution
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
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
letI : Fact (Nat.Prime p) := hpri
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
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' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Theorem: exists_solution
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
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' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
let η₁ : nthRootsFinset p (𝓞 K) := ⟨η₀ * hζ.unit', mul_mem_nthRootsFinset
  (η₀ : _).prop (hζ.unit'_coe.mem_nthRootsFinset hpri.out.pos)⟩
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
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' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Theorem: exists_solution
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
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' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
let η₂ : nthRootsFinset p (𝓞 K) := ⟨η₀ * hζ.unit' * hζ.unit', mul_mem_nthRootsFinset
  η₁.prop (hζ.unit'_coe.mem_nthRootsFinset hpri.out.pos)⟩
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
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', ⋯⟩
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Theorem: exists_solution
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
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', ⋯⟩
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
have hη₁ : η₁ ≠ η₀ := by
  rw [← Subtype.coe_injective.ne_iff]
  show (η₀ * hζ.unit' : 𝓞 K) ≠ η₀
  rw [Ne, mul_right_eq_self₀, not_or]
  exact ⟨hζ.unit'_coe.ne_one hpri.out.one_lt,
    ne_zero_of_mem_nthRootsFinset (η₀ : _).prop⟩
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
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η₁ : η₁ ≠ η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Theorem: exists_solution
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
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η₁ : η₁ ≠ η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
have hη₂ : η₂ ≠ η₀ := by
  rw [← Subtype.coe_injective.ne_iff]
  show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀
  rw [Ne, mul_assoc, ← pow_two, mul_right_eq_self₀, not_or]
  exact ⟨hζ.unit'_coe.pow_ne_one_of_pos_of_lt zero_lt_two
    (hpri.out.two_le.lt_or_eq.resolve_right (PNat.coe_injective.ne hp.symm)),
    ne_zero_of_mem_nthRootsFinset (η₀ : _).prop⟩
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
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η₂ : η₂ ≠ η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Theorem: exists_solution
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
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η₂ : η₂ ≠ η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
have hη : η₂ ≠ η₁ := by
  rw [← Subtype.coe_injective.ne_iff]
  show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀ * hζ.unit'
  rw [Ne, mul_right_eq_self₀, not_or]
  exact ⟨hζ.unit'_coe.ne_one hpri.out.one_lt,
    mul_ne_zero (ne_zero_of_mem_nthRootsFinset (η₀ : _).prop)
    (hζ.unit'_coe.ne_zero hpri.out.ne_zero)⟩
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
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η : η₂ ≠ η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Theorem: exists_solution
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
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η : η₂ ≠ η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
obtain ⟨u₁, hu₁⟩ := hζ.unit'_coe.associated_sub_one hpri.out η₂.prop (η₀ : _).prop
  (Subtype.coe_injective.ne_iff.mpr hη₂)
Proof state after:
case 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₁ = ↑η₂ - ↑η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Theorem: exists_solution
Proof state before:
case 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₁ = ↑η₂ - ↑η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
obtain ⟨u₂, hu₂⟩ := hζ.unit'_coe.associated_sub_one hpri.out (η₀ : _).prop η₁.prop
  (Subtype.coe_injective.ne_iff.mpr hη₁.symm)
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
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₂ = ↑η₀ - ↑η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Theorem: exists_solution
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
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₂ = ↑η₀ - ↑η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
obtain ⟨u₃, hu₃⟩ := hζ.unit'_coe.associated_sub_one hpri.out η₂.prop (η₁ : _).prop
  (Subtype.coe_injective.ne_iff.mpr hη)
Proof state after:
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₃ = ↑η₂ - ↑η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p