awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
z : ℕ
ze : yn w1 w = w * z
t : ℕ
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
nt : LT.lt (α := ℤ) (↑(n ^ k) : ℤ) (↑t : ℤ)
⊢ ∃ (w : ℕ) (a : ℕ) (t : ℕ) (z : ℕ) (a1 : 1 < a),
    xn a1 k ≡ yn a1 k * (a - n) + n ^ k [MOD t] ∧
      2 * a * n = t + (n * n + 1) ∧ n ^ k < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
have tm : x ≡ y * (a - n) + n ^ k [MOD t]
Tactic: have tm : x ≡ y * (a - n) + n ^ k [MOD t] := by
      apply modEq_of_dvd
      rw [Int.natCast_add, Int.natCast_mul, Int.ofNat_sub na, te]
      exact x_sub_y_dvd_pow a1 n k
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
z : ℕ
ze : yn w1 w = w * z
t : ℕ
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
nt : LT.lt (α := ℤ) (↑(n ^ k) : ℤ) (↑t : ℤ)
tm : x ≡ y * (a - n) + n ^ k [MOD t]
⊢ 2 * a * n = t + (n * n + 1)
have zify : HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) = (↑t : ℤ) + (HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) + 1)
Tactic: zify
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
z : ℕ
ze : yn w1 w = w * z
t : ℕ
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
nt : LT.lt (α := ℤ) (↑(n ^ k) : ℤ) (↑t : ℤ)
tm : x ≡ y * (a - n) + n ^ k [MOD t]
⊢ ∃ (w : ℕ) (a : ℕ) (t : ℕ) (z : ℕ) (a1 : 1 < a),
    xn a1 k ≡ yn a1 k * (a - n) + n ^ k [MOD t] ∧
      2 * a * n = t + (n * n + 1) ∧ n ^ k < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
have ta : 2 * a * n = t + (n * n + 1)
Tactic: have ta : 2 * a * n = t + (n * n + 1) := by
      zify
      lia
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
z : ℕ
ze : yn w1 w = w * z
t : ℕ
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
nt : LT.lt (α := ℤ) (↑(n ^ k) : ℤ) (↑t : ℤ)
tm : x ≡ y * (a - n) + n ^ k [MOD t]
ta : 2 * a * n = t + (n * n + 1)
⊢ ∃ (w : ℕ) (a : ℕ) (t : ℕ) (z : ℕ) (a1 : 1 < a),
    xn a1 k ≡ yn a1 k * (a - n) + n ^ k [MOD t] ∧
      2 * a * n = t + (n * n + 1) ∧ n ^ k < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
have zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
Tactic: have zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1 := ze ▸ pell_eq w1 w
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w a t z : ℕ
a1 : 1 < a
tm : xn a1 k ≡ yn a1 k * (a - n) + m [MOD t]
ta : 2 * a * n = t + (n * n + 1)
mt : m < t
nw : n ≤ w
kw : k ≤ w
zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
⊢ n ^ k = m
have hw0 : 0 < w
Tactic: have hw0 : 0 < w := hn0.trans_le nw
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w a t z : ℕ
a1 : 1 < a
tm : xn a1 k ≡ yn a1 k * (a - n) + m [MOD t]
ta : 2 * a * n = t + (n * n + 1)
mt : m < t
nw : n ≤ w
kw : k ≤ w
zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hw0 : 0 < w
⊢ n ^ k = m
have hw1 : 1 < w + 1
Tactic: have hw1 : 1 < w + 1 := Nat.succ_lt_succ hw0
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w a t z : ℕ
a1 : 1 < a
tm : xn a1 k ≡ yn a1 k * (a - n) + m [MOD t]
ta : 2 * a * n = t + (n * n + 1)
mt : m < t
nw : n ≤ w
kw : k ≤ w
zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hw0 : 0 < w
hw1 : 1 < w + 1
⊢ n ^ k = m
have mpr : ∀ (j : ℕ) (yj : w * z = yn hw1 j) (a1 : 1 < xn hw1 j) (tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t])
  (ta : 2 * xn hw1 j * n = t + (n * n + 1))
  (zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1), n ^ k = m
Tactic: rcases eq_pell hw1 zp with ⟨j, rfl, yj⟩
Cleared hypotheses: a, a1, tm, ta, zp
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
⊢ 0 < j
have a : j ≠ 0
Tactic: apply Nat.pos_of_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
⊢ n ^ k = m
have hj0 : 0 < j
Tactic: have hj0 : 0 < j := by
      apply Nat.pos_of_ne_zero
      rintro rfl
      exact lt_irrefl 1 a1
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
⊢ n ^ k = m
have wj : w ≤ j
Tactic: have wj : w ≤ j :=
      Nat.le_of_dvd hj0
        (modEq_zero_iff_dvd.1 <|
          (yn_modEq_a_sub_one hw1 j).symm.trans <| modEq_zero_iff_dvd.2 ⟨z, yj.symm⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
⊢ n ^ k = m
have hnka : n ^ k < xn hw1 j
Tactic: have hnka : n ^ k < xn hw1 j := calc
      n ^ k ≤ n ^ j := Nat.pow_le_pow_right hn0 (le_trans kw wj)
      _ < (w + 1) ^ j := Nat.pow_lt_pow_left (Nat.lt_succ_of_le nw) hj0.ne'
      _ ≤ xn hw1 j := xn_ge_a_pow hw1 j
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
⊢ n ^ k = m
have nt : (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
Tactic: have nt : (↑(n ^ k) : ℤ) < 2 * xn hw1 j * n - n * n - 1 :=
      eq_pow_of_pell_lem hn0.ne' hk0.ne' hnka
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
⊢ n ^ k = m
have na : n ≤ xn hw1 j
Tactic: have na : n ≤ xn hw1 j := (Nat.le_self_pow hk0.ne' _).trans hnka.le
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
na : n ≤ xn hw1 j
⊢ (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
have rw : (↑t : ℤ) + (HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) + 1) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ)
Tactic: rw [sub_sub, eq_sub_iff_add_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
na : n ≤ xn hw1 j
⊢ n ^ k = m
have te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
Tactic: have te : (t : ℤ) = 2 * xn hw1 j * n - n * n - 1 := by
      rw [sub_sub, eq_sub_iff_add_eq]
      exact mod_cast ta.symm
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
na : n ≤ xn hw1 j
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
⊢ xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
have a : (↑t : ℤ) ∣ HSub.hSub (α := ℤ) (↑(yn a1 k * (xn hw1 j - n) + n ^ k) : ℤ) (↑(xn a1 k) : ℤ)
Tactic: apply modEq_of_dvd
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
na : n ≤ xn hw1 j
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
⊢ (↑t : ℤ) ∣ HSub.hSub (α := ℤ) (↑(yn a1 k * (xn hw1 j - n) + n ^ k) : ℤ) (↑(xn a1 k) : ℤ)
have a : HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1 ∣
  (↑(yn a1 k) : ℤ) * HSub.hSub (α := ℤ) (↑(xn hw1 j) : ℤ) (↑n : ℤ) + (↑(n ^ k) : ℤ) - (↑(xn a1 k) : ℤ)
Tactic: rw [te, Nat.cast_add, Nat.cast_mul, Int.ofNat_sub na]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
na : n ≤ xn hw1 j
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
⊢ n ^ k = m
have this : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
Tactic: have : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t] := by
      apply modEq_of_dvd
      rw [te, Nat.cast_add, Nat.cast_mul, Int.ofNat_sub na]
      exact x_sub_y_dvd_pow a1 n k
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
na : n ≤ xn hw1 j
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
this : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
⊢ n ^ k = m
have this₁ : n ^ k % t = m % t
Tactic: have : n ^ k % t = m % t := (this.symm.trans tm).add_left_cancel' _
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
na : n ≤ xn hw1 j
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
this_1 : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
this : n ^ k % t = m % t
⊢ n ^ k = m
have nt₁ : LT.lt (α := ℤ) (↑(n ^ k) : ℤ) (↑t : ℤ)
Tactic: rw [← te] at nt
Cleared hypotheses: nt, na, te, this_1, this
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : LT.lt (α := ℤ) (↑(n ^ k) : ℤ) (↑t : ℤ)
na : n ≤ xn hw1 j
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
this_1 : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
this : n ^ k % t = m % t
⊢ n ^ k = m
have mpr : ∀ (this : n ^ k = m % t), n ^ k = m
Tactic: rwa [Nat.mod_eq_of_lt (Nat.cast_lt.1 nt), Nat.mod_eq_of_lt mt] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : LT.lt (α := ℤ) (↑(n ^ k) : ℤ) (↑t : ℤ)
na : n ≤ xn hw1 j
te : (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
this_1 : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
this : n ^ k % t = m % t
mpr : ∀ (this : n ^ k = m % t), n ^ k = m
⊢ n ^ k = m
have mpr₁ : ∀ (this : n ^ k = m), n ^ k = m
Tactic: rwa [Nat.mod_eq_of_lt (Nat.cast_lt.1 nt), Nat.mod_eq_of_lt mt] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.PowModTotient (goal)
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ (k + φ n) % n = x ^ k % n
have rw : x ^ k % n * 1 % n = x ^ k % n
Tactic: rw [pow_add, mul_mod, pow_totient_mod_eq_one hn h]
-- Lean 4 proof step from Mathlib.NumberTheory.PowModTotient (goal)
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
l : ℕ
ih : x ^ (k + l * φ n) % n = x ^ k % n
⊢ x ^ (k + (l + 1) * φ n) % n = x ^ k % n
have succ : x ^ (k + (l * φ n + 1 * φ n)) % n = x ^ k % n
Tactic: rw [add_mul, one_mul, ← add_assoc, pow_add_totient_mod_eq hn h, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.PowModTotient (goal)
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
l : ℕ
ih : x ^ (k + l * φ n) % n = x ^ k % n
succ : x ^ (k + (l * φ n + 1 * φ n)) % n = x ^ k % n
⊢ x ^ (k + (l + 1) * φ n) % n = x ^ k % n
have succ₁ : x ^ (k + (l * φ n + φ n)) % n = x ^ k % n
Tactic: rw [add_mul, one_mul, ← add_assoc, pow_add_totient_mod_eq hn h, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.PowModTotient (goal)
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
l : ℕ
ih : x ^ (k + l * φ n) % n = x ^ k % n
succ : x ^ (k + (l * φ n + 1 * φ n)) % n = x ^ k % n
succ₁ : x ^ (k + (l * φ n + φ n)) % n = x ^ k % n
⊢ x ^ (k + (l + 1) * φ n) % n = x ^ k % n
have succ₂ : x ^ (k + l * φ n + φ n) % n = x ^ k % n
Tactic: rw [add_mul, one_mul, ← add_assoc, pow_add_totient_mod_eq hn h, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.PowModTotient (goal)
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
l : ℕ
ih : x ^ (k + l * φ n) % n = x ^ k % n
succ : x ^ (k + (l * φ n + 1 * φ n)) % n = x ^ k % n
succ₁ : x ^ (k + (l * φ n + φ n)) % n = x ^ k % n
succ₂ : x ^ (k + l * φ n + φ n) % n = x ^ k % n
succ₃ : x ^ (k + l * φ n) % n = x ^ k % n
⊢ x ^ (k + (l + 1) * φ n) % n = x ^ k % n
have succ₄ : x ^ k % n = x ^ k % n
Tactic: rw [add_mul, one_mul, ← add_assoc, pow_add_totient_mod_eq hn h, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.PowModTotient (goal)
Goal:
x k l n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ (k + l * φ n) % n = x ^ k % n
have zero : x ^ (k + 0 * φ n) % n = x ^ k % n
Tactic: induction l with
  | zero => simp
  | succ l ih =>
    rw [add_mul, one_mul, ← add_assoc, pow_add_totient_mod_eq hn h, ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.NumberTheory.PowModTotient (goal)
Goal:
x k l n : ℕ
hn : 1 < n
h : x.Coprime n
zero : x ^ (k + 0 * φ n) % n = x ^ k % n
⊢ x ^ (k + l * φ n) % n = x ^ k % n
have succ : ∀ (l : ℕ) (ih : x ^ (k + l * φ n) % n = x ^ k % n), x ^ (k + (l + 1) * φ n) % n = x ^ k % n
Tactic: induction l with
  | zero => simp
  | succ l ih =>
    rw [add_mul, one_mul, ← add_assoc, pow_add_totient_mod_eq hn h, ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.NumberTheory.PowModTotient (goal)
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ k % n = x ^ (k % φ n) % n
have rw : x ^ (k / φ n * φ n + k % φ n) % n = x ^ ((k / φ n * φ n + k % φ n) % φ n) % n
Tactic: rw [← div_add_mod' k (φ n), add_comm, pow_add_mul_totient_mod_eq hn h, add_mul_mod_self_right,
    mod_mod k (φ n)]
-- Lean 4 proof step from Mathlib.NumberTheory.PowModTotient (goal)
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
rw : x ^ (k / φ n * φ n + k % φ n) % n = x ^ ((k / φ n * φ n + k % φ n) % φ n) % n
⊢ x ^ k % n = x ^ (k % φ n) % n
have rw₁ : x ^ (k % φ n + k / φ n * φ n) % n = x ^ ((k % φ n + k / φ n * φ n) % φ n) % n
Tactic: rw [← div_add_mod' k (φ n), add_comm, pow_add_mul_totient_mod_eq hn h, add_mul_mod_self_right,
    mod_mod k (φ n)]
-- Lean 4 proof step from Mathlib.NumberTheory.PowModTotient (goal)
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
rw : x ^ (k / φ n * φ n + k % φ n) % n = x ^ ((k / φ n * φ n + k % φ n) % φ n) % n
rw₁ : x ^ (k % φ n + k / φ n * φ n) % n = x ^ ((k % φ n + k / φ n * φ n) % φ n) % n
⊢ x ^ k % n = x ^ (k % φ n) % n
have rw₂ : x ^ (k % φ n) % n = x ^ ((k % φ n + k / φ n * φ n) % φ n) % n
Tactic: rw [← div_add_mod' k (φ n), add_comm, pow_add_mul_totient_mod_eq hn h, add_mul_mod_self_right,
    mod_mod k (φ n)]
-- Lean 4 proof step from Mathlib.NumberTheory.PowModTotient (goal)
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
rw : x ^ (k / φ n * φ n + k % φ n) % n = x ^ ((k / φ n * φ n + k % φ n) % φ n) % n
rw₁ : x ^ (k % φ n + k / φ n * φ n) % n = x ^ ((k % φ n + k / φ n * φ n) % φ n) % n
rw₂ : x ^ (k % φ n) % n = x ^ ((k % φ n + k / φ n * φ n) % φ n) % n
⊢ x ^ k % n = x ^ (k % φ n) % n
have rw₃ : x ^ (k % φ n) % n = x ^ (k % φ n % φ n) % n
Tactic: rw [← div_add_mod' k (φ n), add_comm, pow_add_mul_totient_mod_eq hn h, add_mul_mod_self_right,
    mod_mod k (φ n)]
-- Lean 4 proof step from Mathlib.NumberTheory.PowModTotient (goal)
Goal:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
rw : x ^ (k / φ n * φ n + k % φ n) % n = x ^ ((k / φ n * φ n + k % φ n) % φ n) % n
rw₁ : x ^ (k % φ n + k / φ n * φ n) % n = x ^ ((k % φ n + k / φ n * φ n) % φ n) % n
rw₂ : x ^ (k % φ n) % n = x ^ ((k % φ n + k / φ n * φ n) % φ n) % n
rw₃ : x ^ (k % φ n) % n = x ^ (k % φ n % φ n) % n
⊢ x ^ k % n = x ^ (k % φ n) % n
have rw₄ : x ^ (k % φ n) % n = x ^ (k % φ n) % n
Tactic: rw [← div_add_mod' k (φ n), add_comm, pow_add_mul_totient_mod_eq hn h, add_mul_mod_self_right,
    mod_mod k (φ n)]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
⊢ π (n - 1) = π' n
have zero : π (HSub.hSub (α := ℕ) 0 1) = π' 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
zero : π (HSub.hSub (α := ℕ) 0 1) = π' 0
⊢ π (n - 1) = π' n
have succ : ∀ (n : ℕ), π (n + 1 - 1) = π' (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
⊢ Function.Surjective π
have suffices : Function.Surjective (α := ℕ) (π ∘ fun (n : ℕ) ↦ n - 1)
Tactic: suffices Function.Surjective (π ∘ fun n => n - 1) from this.of_comp
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
⊢ Function.Surjective (α := ℕ) (π ∘ fun (n : ℕ) ↦ n - 1)
have h : (π ∘ fun (n : ℕ) ↦ n - 1) = π'
Tactic: convert! surjective_primeCounting'
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
⊢ (π ∘ fun (n : ℕ) ↦ n - 1) = π'
have h : ∀ (x : ℕ), (π ∘ fun (n : ℕ) ↦ n - 1) x = π' x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
⊢ Tendsto π' atTop atTop
have apply : ¬BddAbove (Set.range π')
Tactic: apply tendsto_atTop_atTop_of_monotone' monotone_primeCounting'
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
⊢ π' n = 0 ↔ n ≤ 2
have rw : count Prime n = 0 ↔ n ≤ 2
Tactic: rw [primeCounting', Nat.count_eq_zero ⟨_, Nat.prime_two⟩, Nat.nth_prime_zero_eq_two]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
rw : count Prime n = 0 ↔ n ≤ 2
⊢ π' n = 0 ↔ n ≤ 2
have rw₁ : n ≤ nth Prime 0 ↔ n ≤ 2
Tactic: rw [primeCounting', Nat.count_eq_zero ⟨_, Nat.prime_two⟩, Nat.nth_prime_zero_eq_two]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
rw : count Prime n = 0 ↔ n ≤ 2
rw₁ : n ≤ nth Prime 0 ↔ n ≤ 2
⊢ π' n = 0 ↔ n ≤ 2
have rw₂ : n ≤ 2 ↔ n ≤ 2
Tactic: rw [primeCounting', Nat.count_eq_zero ⟨_, Nat.prime_two⟩, Nat.nth_prime_zero_eq_two]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
⊢ n.primesBelow = (n - 1).primesLE
have zero : primesBelow 0 = (HSub.hSub (α := ℕ) 0 1).primesLE
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
zero : primesBelow 0 = (HSub.hSub (α := ℕ) 0 1).primesLE
⊢ n.primesBelow = (n - 1).primesLE
have succ : ∀ (n : ℕ), (n + 1).primesBelow = (n + 1 - 1).primesLE
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
⊢ n.primesBelow = filter Prime (Ico 0 n)
have h : ∀ (p : ℕ), p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 0 n)
Tactic: ext p
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
⊢ n.primesLE = filter Prime (Icc 0 n)
have h : ∀ (p : ℕ), p ∈ n.primesLE ↔ p ∈ filter Prime (Icc 0 n)
Tactic: ext p