internlm/Lean-Github huggingface dataset:
Theorem: exists_solution'
Proof state before:
case hcong
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' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
have : p - 1 ≤ m * p := (Nat.sub_le _ _).trans
  ((le_of_eq (one_mul _).symm).trans (Nat.mul_le_mul_right p (one_le_m hp hζ e hy hz)))
Proof state after:
case hcong
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' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
this : ↑p - 1 ≤ m * ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Theorem: exists_solution'
Proof state before:
case hcong
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' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
this : ↑p - 1 ≤ m * ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
obtain ⟨u, hu⟩ := (associated_zeta_sub_one_pow_prime hζ).symm
Proof state after:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Theorem: exists_solution'
Proof state before:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
rw [mul_pow, ← pow_mul, mul_comm (ε₃ : 𝓞 K), mul_assoc, ← Nat.sub_add_cancel this,
  add_comm _ (p - 1 : ℕ), pow_add, mul_assoc] at e'
Proof state after:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = π ^ (↑p - 1) * (π ^ (m * ↑p - (↑p - 1)) * (z' ^ ↑p * ↑ε₃))
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Theorem: exists_solution'
Proof state before:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = π ^ (↑p - 1) * (π ^ (m * ↑p - (↑p - 1)) * (z' ^ ↑p * ↑ε₃))
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
apply_fun Ideal.Quotient.mk (Ideal.span <| singleton (p : 𝓞 K)) at e'
Proof state after:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' :
  (Ideal.Quotient.mk (Ideal.span {↑↑p})) (↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p) =
    (Ideal.Quotient.mk (Ideal.span {↑↑p})) (π ^ (↑p - 1) * (π ^ (m * ↑p - (↑p - 1)) * (z' ^ ↑p * ↑ε₃)))
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Theorem: exists_solution'
Proof state before:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' :
  (Ideal.Quotient.mk (Ideal.span {↑↑p})) (↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p) =
    (Ideal.Quotient.mk (Ideal.span {↑↑p})) (π ^ (↑p - 1) * (π ^ (m * ↑p - (↑p - 1)) * (z' ^ ↑p * ↑ε₃)))
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
rw [map_mul, (Ideal.Quotient.eq_zero_iff_dvd _ _).mpr
  (associated_zeta_sub_one_pow_prime hζ).symm.dvd, zero_mul, Ideal.Quotient.eq_zero_iff_dvd] at e'
Proof state after:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Theorem: exists_solution'
Proof state before:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
obtain ⟨a, ha⟩ := exists_solution'_aux hp hζ hx' e'
Proof state after:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Theorem: exists_solution'
Proof state before:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
obtain ⟨b, hb⟩ := exists_dvd_pow_sub_Int_pow hp a
Proof state after:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
b : ℤ
hb : ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Theorem: exists_solution'
Proof state before:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
b : ℤ
hb : ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
have := dvd_add ha hb
Proof state after:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this✝ : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
b : ℤ
hb : ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
this : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p + (a ^ ↑p - ↑b ^ ↑p)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Theorem: exists_solution'
Proof state before:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this✝ : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
b : ℤ
hb : ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
this : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p + (a ^ ↑p - ↑b ^ ↑p)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
rw [sub_add_sub_cancel, ← Int.cast_pow] at this
Proof state after:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this✝ : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
b : ℤ
hb : ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
this : ↑↑p ∣ ↑(ε₁ / ε₂) - ↑(b ^ ↑p)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Theorem: exists_solution'
Proof state before:
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
this✝ : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
e' : ↑↑p ∣ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p
a : 𝓞 K
ha : ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p
b : ℤ
hb : ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
this : ↑↑p ∣ ↑(ε₁ / ε₂) - ↑(b ^ ↑p)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
Tactic:
exact ⟨b ^ (p : ℕ), this⟩
Proof state after:
no goals
Theorem: coprime_add_self_pow
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y z : R
n : ℕ
hn : 0 < n
hsoln : x ^ n + y ^ n = z ^ n
hxx : IsCoprime x y
⊢ IsCoprime x z
Tactic:
have := IsCoprime.mul_add_left_right (hxx.pow (n := n) (m := n)) 1
Proof state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
n : ℕ
hn : 0 < n
hsoln : x ^ n + y ^ n = z ^ n
hxx : IsCoprime x y
this : IsCoprime (x ^ n) (x ^ n * 1 + y ^ n)
⊢ IsCoprime x z
Theorem: coprime_add_self_pow
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y z : R
n : ℕ
hn : 0 < n
hsoln : x ^ n + y ^ n = z ^ n
hxx : IsCoprime x y
this : IsCoprime (x ^ n) (x ^ n * 1 + y ^ n)
⊢ IsCoprime x z
Tactic:
rwa [mul_one, hsoln, IsCoprime.pow_iff hn hn] at this
Proof state after:
no goals
Theorem: Int.factor_div
Proof state before:
a x : ℤ
hodd : Odd x
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
Tactic:
have h0' : x ≠ 0 := by
  rintro rfl
  contradiction
Proof state after:
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
Theorem: Int.factor_div
Proof state before:
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
Tactic:
set c := a % x with hc
Proof state after:
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
Theorem: Int.factor_div
Proof state before:
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
Tactic:
by_cases H : 2 * c.natAbs < x.natAbs
Proof state after:
case pos
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : 2 * c.natAbs < x.natAbs
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs

case neg
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ¬2 * c.natAbs < x.natAbs
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
Theorem: Int.factor_div
Proof state before:
a x : ℤ
hodd : Odd x
⊢ x ≠ 0
Tactic:
rintro rfl
Proof state after:
a : ℤ
hodd : Odd 0
⊢ False
Theorem: Int.factor_div
Proof state before:
a : ℤ
hodd : Odd 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Int.factor_div
Proof state before:
case pos
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : 2 * c.natAbs < x.natAbs
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
Tactic:
exact ⟨a / x, c, Int.emod_add_ediv' a x, H⟩
Proof state after:
no goals
Theorem: Int.factor_div
Proof state before:
case neg
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ¬2 * c.natAbs < x.natAbs
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
Tactic:
push_neg at H
Proof state after:
case neg
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
Theorem: Int.factor_div
Proof state before:
case neg
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
Tactic:
refine' ⟨(a + abs x) / x, c - abs x, _, _⟩
Proof state after:
case neg.refine'_1
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
⊢ c - |x| + (a + |x|) / x * x = a

case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
⊢ 2 * (c - |x|).natAbs < x.natAbs
Theorem: Int.factor_div
Proof state before:
case neg.refine'_1
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
⊢ c - |x| + (a + |x|) / x * x = a
Tactic:
have := self_dvd_abs x
Proof state after:
case neg.refine'_1
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
this : x ∣ |x|
⊢ c - |x| + (a + |x|) / x * x = a
Theorem: Int.factor_div
Proof state before:
case neg.refine'_1
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
this : x ∣ |x|
⊢ c - |x| + (a + |x|) / x * x = a
Tactic:
rw [Int.add_ediv_of_dvd_right this, add_mul, Int.ediv_mul_cancel this, sub_add_add_cancel, hc,
  Int.emod_add_ediv']
Proof state after:
no goals
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
⊢ 2 * (c - |x|).natAbs < x.natAbs
Tactic:
rw [← Int.ofNat_lt]
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs
Tactic:
replace H := Int.ofNat_le_ofNat_of_le H
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ ↑(2 * c.natAbs)
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ ↑(2 * c.natAbs)
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs
Tactic:
have ofNat_two : ((2 : Nat) : Int) = 2 := rfl
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ ↑(2 * c.natAbs)
ofNat_two : ↑2 = 2
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ ↑(2 * c.natAbs)
ofNat_two : ↑2 = 2
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs
Tactic:
rw [Int.ofNat_mul, ofNat_two] at H ⊢
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * ↑c.natAbs
ofNat_two : ↑2 = 2
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * ↑c.natAbs
ofNat_two : ↑2 = 2
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs
Tactic:
have hcnonneg := Int.emod_nonneg a h0'
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * ↑c.natAbs
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * ↑c.natAbs
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs
Tactic:
have := Int.emod_lt a h0'
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * ↑c.natAbs
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * ↑c.natAbs
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs
Tactic:
rw [Int.natAbs_of_nonneg hcnonneg] at H
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs
Tactic:
rw [← Int.natAbs_neg, neg_sub, Int.natAbs_of_nonneg (sub_nonneg_of_le this.le), mul_sub,
  sub_lt_iff_lt_add, two_mul, Int.abs_eq_natAbs, add_lt_add_iff_left]
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ ↑x.natAbs < 2 * (a % x)
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ ↑x.natAbs < 2 * (a % x)
Tactic:
apply lt_of_le_of_ne H
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ ↑x.natAbs ≠ 2 * (a % x)
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ ↑x.natAbs ≠ 2 * (a % x)
Tactic:
contrapose! hodd with heqtwomul
Proof state after:
case neg.refine'_2
a x : ℤ
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
heqtwomul : ↑x.natAbs = 2 * (a % x)
⊢ ¬Odd x
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
heqtwomul : ↑x.natAbs = 2 * (a % x)
⊢ ¬Odd x
Tactic:
rw [← Int.even_iff_not_odd, ← Int.natAbs_even, ← Int.even_coe_nat, even_iff_two_dvd]
Proof state after:
case neg.refine'_2
a x : ℤ
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
heqtwomul : ↑x.natAbs = 2 * (a % x)
⊢ 2 ∣ ↑x.natAbs
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
heqtwomul : ↑x.natAbs = 2 * (a % x)
⊢ 2 ∣ ↑x.natAbs
Tactic:
exact ⟨_, heqtwomul⟩
Proof state after:
no goals
Theorem: two_not_cube
Proof state before:
r : ℕ
⊢ r ^ 3 ≠ 2
Tactic:
apply Monotone.ne_of_lt_of_lt_nat (Nat.pow_left_strictMono three_ne_zero).monotone 1 <;> norm_num
Proof state after:
no goals
Theorem: Int.two_not_cube
Proof state before:
r : ℤ
⊢ r ^ 3 ≠ 2
Tactic:
intro H
Proof state after:
r : ℤ
H : r ^ 3 = 2
⊢ False