internlm/Lean-Github huggingface dataset:
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₃ = ↑η₂ - ↑η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
have := stuff hp hreg hζ e hy hz η₁ hη₁ η₂ 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₃ = ↑η₂ - ↑η₁
this :
  (↑η₂ - ↑η₀) * ↑(ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + (↑η₀ - ↑η₁) * ↑(ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    (↑η₂ - ↑η₁) * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
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 :
  (↑η₂ - ↑η₀) * ↑(ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + (↑η₀ - ↑η₁) * ↑(ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    (↑η₂ - ↑η₁) * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
Tactic:
rw [← hu₁, ← hu₂, ← hu₃, mul_assoc _ (u₁ : 𝓞 K), mul_assoc _ (u₂ : 𝓞 K), mul_assoc _ (u₃ : 𝓞 K),
  mul_assoc (π), mul_assoc (π), ← mul_add,
  mul_right_inj' (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt), ← Units.val_mul,
  ← Units.val_mul] at this
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₃ = ↑η₂ - ↑η₁
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
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', ⋯⟩
⊢ η₁ ≠ η₀
Tactic:
rw [← Subtype.coe_injective.ne_iff]
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', ⋯⟩
⊢ ↑η₁ ≠ ↑η₀
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', ⋯⟩
⊢ ↑η₁ ≠ ↑η₀
Tactic:
show (η₀ * hζ.unit' : 𝓞 K) ≠ η₀
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ζ.unit' ≠ ↑η₀
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ζ.unit' ≠ ↑η₀
Tactic:
rw [Ne, mul_right_eq_self₀, not_or]
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ζ.unit' = 1 ∧ ¬↑η₀ = 0
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ζ.unit' = 1 ∧ ¬↑η₀ = 0
Tactic:
exact ⟨hζ.unit'_coe.ne_one hpri.out.one_lt,
  ne_zero_of_mem_nthRootsFinset (η₀ : _).prop⟩
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
⊢ η₂ ≠ η₀
Tactic:
rw [← Subtype.coe_injective.ne_iff]
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η₁ : η₁ ≠ η₀
⊢ ↑η₂ ≠ ↑η₀
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η₁ : η₁ ≠ η₀
⊢ ↑η₂ ≠ ↑η₀
Tactic:
show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀
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ζ.unit' * ↑hζ.unit' ≠ ↑η₀
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ζ.unit' * ↑hζ.unit' ≠ ↑η₀
Tactic:
rw [Ne, mul_assoc, ← pow_two, mul_right_eq_self₀, not_or]
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ζ.unit' ^ 2 = 1 ∧ ¬↑η₀ = 0
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ζ.unit' ^ 2 = 1 ∧ ¬↑η₀ = 0
Tactic:
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:
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) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
⊢ η₂ ≠ η₁
Tactic:
rw [← Subtype.coe_injective.ne_iff]
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η₂ : η₂ ≠ η₀
⊢ ↑η₂ ≠ ↑η₁
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η₂ : η₂ ≠ η₀
⊢ ↑η₂ ≠ ↑η₁
Tactic:
show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀ * hζ.unit'
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ζ.unit' * ↑hζ.unit' ≠ ↑η₀ * ↑hζ.unit'
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ζ.unit' * ↑hζ.unit' ≠ ↑η₀ * ↑hζ.unit'
Tactic:
rw [Ne, mul_right_eq_self₀, not_or]
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ζ.unit' = 1 ∧ ¬↑η₀ * ↑hζ.unit' = 0
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ζ.unit' = 1 ∧ ¬↑η₀ * ↑hζ.unit' = 0
Tactic:
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:
no goals
Theorem: exists_solution
Proof state before:
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η₂
Tactic:
exact hζ.zeta_sub_one_prime'.not_dvd_mul
  (a_div_a_zero_num_spec hp hreg hζ e hy hz η₁ hη₁)
  (a_div_a_zero_denom_spec hp hreg hζ e hy hz η₂ hη₂)
Proof state after:
no goals
Theorem: exists_solution
Proof state before:
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η₁
Tactic:
exact hζ.zeta_sub_one_prime'.not_dvd_mul
  (a_div_a_zero_num_spec hp hreg hζ e hy hz η₂ hη₂)
  (a_div_a_zero_denom_spec hp hreg hζ e hy hz η₁ hη₁)
Proof state after:
no goals
Theorem: exists_solution
Proof state before:
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η₂
Tactic:
exact hζ.zeta_sub_one_prime'.not_dvd_mul
  (a_div_a_zero_denom_spec hp hreg hζ e hy hz η₁ hη₁)
  (a_div_a_zero_denom_spec hp hreg hζ e hy hz η₂ hη₂)
Proof state after:
no goals
Theorem: exists_solution'_aux
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) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
⊢ ∃ a, ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑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) }
ε₁ ε₂ : (𝓞 K)ˣ
hx : ¬π ∣ x
h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p
this : Fact (↑p).Prime := hpri
⊢ ∃ a, ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p