awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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 : ℤ)
⊢ HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1 ∣
    (↑y : ℤ) * HSub.hSub (α := ℤ) (↑a : ℤ) (↑n : ℤ) + (↑(n ^ k) : ℤ) - (↑x : ℤ)

Tactic:
exact x_sub_y_dvd_pow a1 n k

Premises used: Pell.x_sub_y_dvd_pow
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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 : ℤ)
⊢ 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
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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]
zify : HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) = (↑t : ℤ) + (HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) + 1)
⊢ 2 * a * n = t + (n * n + 1)

Tactic:
zify
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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]
⊢ HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) = (↑t : ℤ) + (HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) + 1)

Tactic:
lia
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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)

Tactic:
have ta : 2 * a * n = t + (n * n + 1) := by
      zify
      lia
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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)
⊢ 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
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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)
zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 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

Tactic:
⟨w, a, t, z, a1, tm, ta, Nat.cast_lt.1 nt, nw, kw, zp⟩

Premises used: And.intro, Exists.intro, Iff.mp, Nat.cast_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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)
zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 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

Tactic:
exact ⟨w, a, t, z, a1, tm, ta, Nat.cast_lt.1 nt, nw, kw, zp⟩
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) n 0 = 1

Tactic:
_root_.pow_zero n

Premises used: pow_zero
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) n 0 = 1

Tactic:
exact _root_.pow_zero n

Premises used: pow_zero
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
k : ℕ
hk0 : 0 < k
⊢ HPow.hPow (α := ℕ) 0 k = 0

Tactic:
zero_pow hk0.ne'

Premises used: LT.lt.ne', zero_pow
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
k : ℕ
hk0 : 0 < k
⊢ HPow.hPow (α := ℕ) 0 k = 0

Tactic:
exact zero_pow hk0.ne'

Premises used: LT.lt.ne', zero_pow
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
⊢ 0 < w

Tactic:
have hw0 : 0 < w := hn0.trans_le nw
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
⊢ 1 < w + 1

Tactic:
have hw1 : 1 < w + 1 := Nat.succ_lt_succ hw0
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
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
⊢ n ^ k = m

Tactic:
rcases eq_pell hw1 zp with ⟨j, rfl, yj⟩

Premises used: Pell.eq_pell, rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
a : j ≠ 0
⊢ 0 < j

Tactic:
apply Nat.pos_of_ne_zero

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
yj : w * z = yn hw1 0
a1 : 1 < xn hw1 0
tm : xn a1 k ≡ yn a1 k * (xn hw1 0 - n) + m [MOD t]
ta : 2 * xn hw1 0 * n = t + (n * n + 1)
zp : xn hw1 0 * xn hw1 0 - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
⊢ False

Tactic:
lt_irrefl 1 a1

Premises used: lt_irrefl, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
yj : w * z = yn hw1 0
a1 : 1 < xn hw1 0
tm : xn a1 k ≡ yn a1 k * (xn hw1 0 - n) + m [MOD t]
ta : 2 * xn hw1 0 * n = t + (n * n + 1)
zp : xn hw1 0 * xn hw1 0 - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
⊢ False

Tactic:
exact lt_irrefl 1 a1

Premises used: lt_irrefl, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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

Tactic:
have hj0 : 0 < j := by
      apply Nat.pos_of_ne_zero
      rintro rfl
      exact lt_irrefl 1 a1
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
⊢ 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⟩)
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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 < 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
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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) : ℤ) < 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
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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 ≤ xn hw1 j

Tactic:
have na : n ≤ xn hw1 j := (Nat.le_self_pow hk0.ne' _).trans hnka.le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
rw : (↑t : ℤ) + (HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) + 1) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ)
⊢ (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1

Tactic:
rw [sub_sub, eq_sub_iff_add_eq]

Premises used: eq_sub_iff_add_eq, sub_sub
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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 (α := ℤ) (↑n : ℤ) (↑n : ℤ) + 1) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ)

Tactic:
mod_cast ta.symm

Premises used: Nat.cast_mul._simp_1, HMul.hMul, Pell.xn, congrArg, Nat.cast_add._simp_1, cast, Nat.cast, HAdd.hAdd, congr, Nat.cast_inj._simp_1, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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 (α := ℤ) (↑n : ℤ) (↑n : ℤ) + 1) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ)

Tactic:
exact mod_cast ta.symm

Premises used: Eq.symm
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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

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
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
a : (↑t : ℤ) ∣ HSub.hSub (α := ℤ) (↑(yn a1 k * (xn hw1 j - n) + n ^ k) : ℤ) (↑(xn a1 k) : ℤ)
⊢ xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]

Tactic:
apply modEq_of_dvd

Premises used: Nat.modEq_of_dvd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
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) : ℤ)
⊢ (↑t : ℤ) ∣ HSub.hSub (α := ℤ) (↑(yn a1 k * (xn hw1 j - n) + n ^ k) : ℤ) (↑(xn a1 k) : ℤ)

Tactic:
rw [te, Nat.cast_add, Nat.cast_mul, Int.ofNat_sub na]

Premises used: Int.ofNat_sub, Nat.cast_add, Nat.cast_mul
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
⊢ 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:
x_sub_y_dvd_pow a1 n k

Premises used: Pell.yz, Pell.xz, Pell.x_sub_y_dvd_pow
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
⊢ 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:
exact x_sub_y_dvd_pow a1 n k

Premises used: Pell.x_sub_y_dvd_pow
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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]

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
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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 % t = m % t

Tactic:
have : n ^ k % t = m % t := (this.symm.trans tm).add_left_cancel' _
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
⊢ LT.lt (α := ℤ) (↑(n ^ k) : ℤ) (↑t : ℤ)

Tactic:
rw [← te] at nt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
nt₁ : LT.lt (α := ℤ) (↑(n ^ k) : ℤ) (↑t : ℤ)
⊢ n ≤ xn hw1 j

Tactic:
rw [← te] at nt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
nt₁ : LT.lt (α := ℤ) (↑(n ^ k) : ℤ) (↑t : ℤ)
na₁ : n ≤ xn hw1 j
⊢ (↑t : ℤ) = HMul.hMul (α := ℤ) 2 (↑(xn hw1 j) : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1

Tactic:
rw [← te] at nt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
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
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
⊢ xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]

Tactic:
rw [← te] at nt