awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
a1 : 1 < a
ky_1 : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
h :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
⊢ j ≡ k [MOD 4 * yn a1 i]

Tactic:
have jk : j ≡ k [MOD 4 * yn a1 i] :=
              have : 4 * yn a1 i ∣ b - 1 :=
                Int.natCast_dvd_natCast.1 <| by rw [Int.ofNat_sub (le_of_lt b1)]; exact bm1.symm.dvd
              ((yn_modEq_a_sub_one b1 _).of_dvd this).symm.trans tk
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
a1 : 1 < a
ky_1 : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
h :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
rw : 2 * yn a1 i < 4 * yn a1 i
⊢ yn a1 i + yn a1 i < 4 * yn a1 i

Tactic:
rw [← two_mul]

Premises used: two_mul
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
a1 : 1 < a
ky_1 : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
h :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
⊢ LT.lt (α := ℕ) 2 4

Tactic:
decide
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
a1 : 1 < a
ky_1 : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
h :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
⊢ 2 * yn a1 i < 4 * yn a1 i

Tactic:
exact Nat.mul_lt_mul_of_pos_right (by decide) (strictMono_y a1 ipos)

Premises used: Pell.strictMono_y, Nat.mul_lt_mul_of_pos_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
a1 : 1 < a
ky_1 : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
h :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
⊢ k + i < 4 * yn a1 i

Tactic:
have ki : k + i < 4 * yn a1 i :=
              lt_of_le_of_lt (_root_.add_le_add ky (yn_ge_n a1 i)) <| by
                rw [← two_mul]
                exact Nat.mul_lt_mul_of_pos_right (by decide) (strictMono_y a1 ipos)
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
a1 : 1 < a
ky_1 : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
h :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
ki : k + i < 4 * yn a1 i
⊢ j ≡ i [MOD 4 * n]

Tactic:
have ji : j ≡ i [MOD 4 * n] :=
              have : xn a1 j ≡ xn a1 i [MOD xn a1 n] :=
                (xy_modEq_of_modEq b1 a1 ba j).left.symm.trans sx
              (modEq_of_xn_modEq a1 ipos iln this).resolve_right
                fun ji : j + i ≡ 0 [MOD 4 * n] =>
                not_le_of_gt ki <|
                  Nat.le_of_dvd (lt_of_lt_of_le ipos <| Nat.le_add_left _ _) <|
                    modEq_zero_iff_dvd.1 <| (jk.symm.add_right i).trans <| ji.of_dvd yd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
a1 : 1 < a
ky_1 : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
h :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
ki : k + i < 4 * yn a1 i
ji : j ≡ i [MOD 4 * n]
⊢ i % (4 * yn a1 i) = k % (4 * yn a1 i)

Tactic:
have : i % (4 * yn a1 i) = k % (4 * yn a1 i) := (ji.of_dvd yd).symm.trans jk
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
a1 : 1 < a
ky_1 : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
h :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
ki : k + i < 4 * yn a1 i
ji : j ≡ i [MOD 4 * n]
this : i % (4 * yn a1 i) = k % (4 * yn a1 i)
rwa : ∀ (this : i = k % (4 * yn a1 i)), i = k
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : i = k), i = k
⊢ i = k

Tactic:
rwa [Nat.mod_eq_of_lt (lt_of_le_of_lt (Nat.le_add_left _ _) ki),
              Nat.mod_eq_of_lt (lt_of_le_of_lt (Nat.le_add_right _ _) ki)] at this

Premises used: lt_of_le_of_lt, Nat.le_add_right, Nat.le_add_left, Nat.mod_eq_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ (↑a : ℤ) ≤ HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 - HPow.hPow (β := ℕ) (HSub.hSub (α := ℤ) (↑a : ℤ) 1) 2 - 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ y ≤ a

Tactic:
have := hya.le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
h : 0 ≤ HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ)
h₁ : LE.le (α := ℤ) 1 (↑y : ℤ)
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 - HPow.hPow (β := ℕ) (HSub.hSub (α := ℤ) (↑a : ℤ) 1) 2 - 1 ≤
    HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 - HPow.hPow (β := ℕ) (HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ)) 2 - 1

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
h : 0 ≤ a - y
⊢ 0 ≤ HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
h : 1 ≤ y
⊢ LE.le (α := ℤ) 1 (↑y : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ 0 ≤ a - y

Tactic:
lia
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ 1 ≤ y

Tactic:
lia
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 - HPow.hPow (β := ℕ) (HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ)) 2 - 1 =
    HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
m n k : ℕ
mp :
  n ^ k = m →
    k = 0 ∧ m = 1 ∨
      0 < k ∧
        (n = 0 ∧ m = 0 ∨
          0 < n ∧
            ∃ (w : ℕ) (a : ℕ) (t : ℕ) (z : ℕ) (a1 : 1 < a),
              xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
                2 * a * n = t + (n * n + 1) ∧
                  m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)
mpr :
  k = 0 ∧ m = 1 ∨
      0 < k ∧
        (n = 0 ∧ m = 0 ∨
          0 < n ∧
            ∃ (w : ℕ) (a : ℕ) (t : ℕ) (z : ℕ) (a1 : 1 < a),
              xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
                2 * a * n = t + (n * n + 1) ∧
                  m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1) →
    n ^ k = m
⊢ n ^ k = m ↔
    k = 0 ∧ m = 1 ∨
      0 < k ∧
        (n = 0 ∧ m = 0 ∨
          0 < n ∧
            ∃ (w : ℕ) (a : ℕ) (t : ℕ) (z : ℕ) (a1 : 1 < a),
              xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
                2 * a * n = t + (n * n + 1) ∧
                  m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
n k : ℕ
⊢ k = 0 ∧ n ^ k = 1 ∨
    0 < k ∧
      (n = 0 ∧ n ^ k = 0 ∨
        0 < n ∧
          ∃ (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:
k.eq_zero_or_pos.imp (fun k0 : k = 0 => k0.symm ▸ ⟨rfl, rfl⟩) fun hk => ⟨hk, ?_⟩

Premises used: Eq.rec, And.intro, Or.imp, Eq.symm, Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
n k : ℕ
mp :
  ∀ (hk : 0 < k),
    n = 0 ∧ n ^ k = 0 ∨
      0 < n ∧
        ∃ (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
⊢ k = 0 ∧ n ^ k = 1 ∨
    0 < k ∧
      (n = 0 ∧ n ^ k = 0 ∨
        0 < n ∧
          ∃ (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:
refine k.eq_zero_or_pos.imp (fun k0 : k = 0 => k0.symm ▸ ⟨rfl, rfl⟩) fun hk => ⟨hk, ?_⟩

Premises used: Or.imp, Nat.eq_zero_or_pos
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
n k : ℕ
hk : 0 < k
⊢ n = 0 ∧ n ^ k = 0 ∨
    0 < n ∧
      ∃ (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:
n.eq_zero_or_pos.imp (fun n0 : n = 0 ↦ n0.symm ▸ ⟨rfl, zero_pow hk.ne'⟩)
      fun hn ↦ ⟨hn, ?_⟩

Premises used: Eq.rec, LT.lt.ne', And.intro, Or.imp, Eq.symm, Nat.eq_zero_or_pos, zero_pow, rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
n k : ℕ
hk : 0 < k
mp :
  ∀ (hn : 0 < n),
    ∃ (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
⊢ n = 0 ∧ n ^ k = 0 ∨
    0 < n ∧
      ∃ (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:
refine n.eq_zero_or_pos.imp (fun n0 : n = 0 ↦ n0.symm ▸ ⟨rfl, zero_pow hk.ne'⟩)
      fun hn ↦ ⟨hn, ?_⟩

Premises used: Or.imp, Nat.eq_zero_or_pos
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
⊢ n ≤ w

Tactic:
have nw : n ≤ w := le_max_left _ _
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
⊢ k ≤ w

Tactic:
have kw : k ≤ w := le_max_right _ _
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
⊢ 0 < w

Tactic:
have wpos : 0 < w := hn.trans_le nw
-- 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
⊢ 1 < w + 1

Tactic:
have w1 : 1 < w + 1 := Nat.succ_lt_succ wpos
-- 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
⊢ 1 < a

Tactic:
have a1 : 1 < a := strictMono_x w1 wpos
-- 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
⊢ n ≤ a

Tactic:
have na : n ≤ a := nw.trans (n_lt_xn w1 w).le
-- 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
⊢ w ∣ yn w1 w

Tactic:
modEq_zero_iff_dvd.1 ((yn_modEq_a_sub_one w1 w).trans dvd_rfl.modEq_zero_nat)

Premises used: Dvd.dvd.modEq_zero_nat, Iff.mp, dvd_rfl, Nat.modEq_zero_iff_dvd, Pell.yn_modEq_a_sub_one, Nat.ModEq.trans
-- 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
mp :
  ∀ (z : ℕ) (ze : yn w1 w = w * z),
    ∃ (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
⊢ ∃ (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:
obtain ⟨z, ze⟩ : w ∣ yn w1 w :=
      modEq_zero_iff_dvd.1 ((yn_modEq_a_sub_one w1 w).trans dvd_rfl.modEq_zero_nat)

Premises used: Dvd.dvd.modEq_zero_nat, Pell.yn, Iff.mp, dvd_rfl, Nat.modEq_zero_iff_dvd, Pell.yn_modEq_a_sub_one, Nat.ModEq.trans
-- 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
⊢ (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1

Tactic:
eq_pow_of_pell_lem hn.ne' hk.ne' ?_

Premises used: LT.lt.ne', Pell.eq_pow_of_pell_lem
-- 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
refine : n ^ k < a
⊢ (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1

Tactic:
refine eq_pow_of_pell_lem hn.ne' hk.ne' ?_

Premises used: LT.lt.ne', Pell.eq_pow_of_pell_lem
-- 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
⊢ n ^ k ≤ n ^ w

Tactic:
Nat.pow_le_pow_right hn kw

Premises used: Nat.pow_le_pow_right
-- 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
⊢ n ^ w < (w + 1) ^ w

Tactic:
Nat.pow_lt_pow_left (Nat.lt_succ_of_le nw) wpos.ne'

Premises used: Nat.lt_succ_of_le, LT.lt.ne', Nat.pow_lt_pow_left
-- 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
⊢ (w + 1) ^ w ≤ a

Tactic:
xn_ge_a_pow w1 w

Premises used: Pell.xn_ge_a_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
⊢ n ^ k < a

Tactic:
calc
        n ^ k ≤ n ^ w := Nat.pow_le_pow_right hn kw
        _ < (w + 1) ^ w := Nat.pow_lt_pow_left (Nat.lt_succ_of_le nw) wpos.ne'
        _ ≤ a := xn_ge_a_pow w1 w

Premises used: Nat.lt_succ_of_le, Nat.pow_le_pow_right, LT.lt.ne', HAdd.hAdd, Nat.pow_lt_pow_left, OfNat.ofNat, Pell.xn_ge_a_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
⊢ (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1

Tactic:
have nt : (↑(n ^ k) : ℤ) < 2 * a * n - n * n - 1 := by
      refine eq_pow_of_pell_lem hn.ne' hk.ne' ?_
      calc
        n ^ k ≤ n ^ w := Nat.pow_le_pow_right hn kw
        _ < (w + 1) ^ w := Nat.pow_lt_pow_left (Nat.lt_succ_of_le nw) wpos.ne'
        _ ≤ a := xn_ge_a_pow 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
nt : (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
⊢ 0 ≤ HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1

Tactic:
(Nat.cast_nonneg _).trans nt.le

Premises used: Nat.cast_nonneg, LT.lt.le, LE.le.trans
-- 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
nt : (↑(n ^ k) : ℤ) < HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1
mp :
  ∀ (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
⊢ ∃ (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:
lift (2 * a * n - n * n - 1 : ℤ) to ℕ using (Nat.cast_nonneg _).trans nt.le with t te

Premises used: HMul.hMul, Nat.cast_nonneg, HSub.hSub, LT.lt.le, Nat.cast, LE.le.trans, OfNat.ofNat
-- 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 : ℤ)
a₁ : (↑t : ℤ) ∣ HSub.hSub (α := ℤ) (↑(y * (a - n) + n ^ k) : ℤ) (↑x : ℤ)
⊢ x ≡ y * (a - n) + n ^ k [MOD t]

Tactic:
apply modEq_of_dvd

Premises used: Nat.modEq_of_dvd
-- 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 : ℤ)
a₁ :
  HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑n : ℤ) - HMul.hMul (α := ℤ) (↑n : ℤ) (↑n : ℤ) - 1 ∣
    (↑y : ℤ) * HSub.hSub (α := ℤ) (↑a : ℤ) (↑n : ℤ) + (↑(n ^ k) : ℤ) - (↑x : ℤ)
⊢ (↑t : ℤ) ∣ HSub.hSub (α := ℤ) (↑(y * (a - n) + n ^ k) : ℤ) (↑x : ℤ)

Tactic:
rw [Int.natCast_add, Int.natCast_mul, Int.ofNat_sub na, te]

Premises used: Int.ofNat_sub, Int.natCast_add, Int.natCast_mul
-- 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:
x_sub_y_dvd_pow a1 n k

Premises used: Pell.yz, Pell.xz, Pell.x_sub_y_dvd_pow