awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o : j = n ∨ n < j
jn_1 : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i < j
h_1 : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
left_1 : a = 2
n1 : n = 1
left_2 : i = 0
j2 : j = 2
j2n₁ : HAdd.hAdd (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 2 1
jnn₁ : j + 1 ≠ n
ntriv₁ : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2₁ : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o₁ : j = n ∨ n < j
jn₁ : j > n
jn₂ : j ≠ n
s₁ : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h₁ : i < j
x : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
left : a = 2
n1₁ : n = 1
left₁ : i = 0
⊢ j = 2

Tactic:
rw [n1, j2] at j2n
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : HAdd.hAdd (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 2 1
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o : j = n ∨ n < j
jn_1 : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i < j
h_1 : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
left : a = 2
n1 : n = 1
left_1 : i = 0
j2 : j = 2
⊢ ¬HAdd.hAdd (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 2 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : HAdd.hAdd (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 2 1
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o : j = n ∨ n < j
jn_1 : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i < j
h_1 : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
left : a = 2
n1 : n = 1
left_1 : i = 0
j2 : j = 2
⊢ False

Tactic:
exact absurd j2n (by decide)

Premises used: absurd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o : j = n ∨ n < j
jn_1 : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
rw : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
⊢ xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
rw [h]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o : j = n ∨ n < j
jn_1 : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
s
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o : j = n ∨ n < j
jn_1 : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
exact s
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o : j = n ∨ n < j
jn : j > n
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
rw :
  HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - j)) : ℤ) <
    HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - (j + 1))) : ℤ)
⊢ LT.lt (α := ℤ) (↑(xn a1 j % xn a1 n) : ℤ) (↑(xn a1 (j + 1) % xn a1 n) : ℤ)

Tactic:
rw [lem2 j jn (le_of_lt j2n), lem2 (j + 1) (Nat.le_succ_of_le jn) j2n]

Premises used: le_of_lt, HAdd.hAdd, Nat.le_succ_of_le, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o : j = n ∨ n < j
jn : j > n
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
⊢ HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - j)) : ℤ) <
    HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - (j + 1))) : ℤ)

Tactic:
sub_lt_sub_left (Int.ofNat_lt_ofNat_of_lt <| strictMono_x _ ?_) _

Premises used: Int.ofNat_lt_ofNat_of_lt, Pell.strictMono_x, sub_lt_sub_left
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o : j = n ∨ n < j
jn : j > n
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
refine : 2 * n - (j + 1) < 2 * n - j
⊢ HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - j)) : ℤ) <
    HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - (j + 1))) : ℤ)

Tactic:
refine sub_lt_sub_left (Int.ofNat_lt_ofNat_of_lt <| strictMono_x _ ?_) _

Premises used: Int.ofNat_lt_ofNat_of_lt, Pell.strictMono_x, sub_lt_sub_left
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o : j = n ∨ n < j
jn : j > n
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
rw : (2 * n - j).pred < 2 * n - j
⊢ 2 * n - (j + 1) < 2 * n - j

Tactic:
rw [Nat.sub_succ]

Premises used: Nat.sub_succ
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o : j = n ∨ n < j
jn : j > n
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
⊢ (2 * n - j).pred < 2 * n - j

Tactic:
Nat.pred_lt (_root_.ne_of_gt <| tsub_pos_of_lt j2n)

Premises used: ne_of_gt, Nat.pred_lt, tsub_pos_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
o : j = n ∨ n < j
jn : j > n
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
⊢ (2 * n - j).pred < 2 * n - j

Tactic:
exact Nat.pred_lt (_root_.ne_of_gt <| tsub_pos_of_lt j2n)

Premises used: ne_of_gt, Nat.pred_lt, tsub_pos_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : n = 0
⊢ i = j

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
⊢ False

Tactic:
_root_.ne_of_gt ?_ h

Premises used: ne_of_gt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
refine : xn a1 j % xn a1 n < xn a1 i % xn a1 n
⊢ False

Tactic:
refine _root_.ne_of_gt ?_ h

Premises used: ne_of_gt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
rw : 0 < xn a1 i % xn a1 n
⊢ xn a1 j % xn a1 n < xn a1 i % xn a1 n

Tactic:
rw [jn, Nat.mod_self]

Premises used: Nat.mod_self
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
rw : 0 < xn a1 0
⊢ 0 < xn a1 0 % xn a1 n

Tactic:
rw [Nat.mod_eq_of_lt (strictMono_x a1 (Nat.pos_of_ne_zero npos))]

Premises used: Nat.mod_eq_of_lt, Nat.pos_of_ne_zero, Pell.strictMono_x
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
⊢ 0 < xn a1 0

Tactic:
Nat.succ_pos _

Premises used: Pell.xn, Nat.succ_pos
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
⊢ 0 < xn a1 0

Tactic:
exact Nat.succ_pos _

Premises used: Nat.succ_pos
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
⊢ 0 < xn a1 0 % xn a1 n

Tactic:
have x0 : 0 < xn a1 0 % xn a1 n := by
          rw [Nat.mod_eq_of_lt (strictMono_x a1 (Nat.pos_of_ne_zero npos))]
          exact Nat.succ_pos _
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
zero :
  ∀ (ij : 0 ≤ j) (h : xn a1 0 ≡ xn a1 j [MOD xn a1 n]) (ntriv : ¬(a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ j = 2))
    (ij' : 0 < j), 0 < xn a1 0 % xn a1 n
succ :
  ∀ (i : ℕ) (ij : i + 1 ≤ j) (h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]) (ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2))
    (ij' : i + 1 < j), 0 < xn a1 (i + 1) % xn a1 n
⊢ 0 < xn a1 i % xn a1 n

Tactic:
rcases i with - | i
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
ij : 0 ≤ j
h : xn a1 0 ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ j = 2)
ij' : 0 < j
⊢ 0 < xn a1 0 % xn a1 n

Tactic:
x0
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
ij : 0 ≤ j
h : xn a1 0 ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ j = 2)
ij' : 0 < j
⊢ 0 < xn a1 0 % xn a1 n

Tactic:
exact x0
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : i + 1 < j
⊢ i + 1 < n

Tactic:
rw [jn] at ij'
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : i + 1 < n
h_1 : a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2
left : a = 2
n1 : n = 1
left_1 : Eq (α := ℕ) 0 0
i2 : i + 1 = 2
⊢ LT.lt (α := ℕ) 2 1

Tactic:
rw [n1, i2] at ij'
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : i + 1 < n
h_1 : a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2
left : a = 2
n1 : n = 1
left_1 : Eq (α := ℕ) 0 0
i2 : i + 1 = 2
ij'₁ : LT.lt (α := ℕ) 2 1
⊢ a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2

Tactic:
rw [n1, i2] at ij'
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : i + 1 < n
h_1 : a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2
left : a = 2
n1 : n = 1
left_1 : Eq (α := ℕ) 0 0
i2 : i + 1 = 2
ij'₁ : LT.lt (α := ℕ) 2 1
x : a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2
⊢ a = 2

Tactic:
rw [n1, i2] at ij'
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : i + 1 < n
h_1 : a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2
left_1 : a = 2
n1 : n = 1
left_2 : Eq (α := ℕ) 0 0
i2 : i + 1 = 2
ij'₁ : LT.lt (α := ℕ) 2 1
x : a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2
left : a = 2
⊢ n = 1

Tactic:
rw [n1, i2] at ij'
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : i + 1 < n
h_1 : a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2
left_1 : a = 2
n1 : n = 1
left_2 : Eq (α := ℕ) 0 0
i2 : i + 1 = 2
ij'₁ : LT.lt (α := ℕ) 2 1
x : a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2
left : a = 2
n1₁ : n = 1
⊢ Eq (α := ℕ) 0 0

Tactic:
rw [n1, i2] at ij'
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : i + 1 < n
h_1 : a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2
left_1 : a = 2
n1 : n = 1
left_2 : Eq (α := ℕ) 0 0
i2 : i + 1 = 2
ij'₁ : LT.lt (α := ℕ) 2 1
x : a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2
left : a = 2
n1₁ : n = 1
left₁ : Eq (α := ℕ) 0 0
⊢ i + 1 = 2

Tactic:
rw [n1, i2] at ij'
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : LT.lt (α := ℕ) 2 1
h_1 : a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2
left : a = 2
n1 : n = 1
left_1 : Eq (α := ℕ) 0 0
i2 : i + 1 = 2
⊢ ¬LT.lt (α := ℕ) 2 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : LT.lt (α := ℕ) 2 1
h_1 : a = 2 ∧ n = 1 ∧ Eq (α := ℕ) 0 0 ∧ i + 1 = 2
left : a = 2
n1 : n = 1
left_1 : Eq (α := ℕ) 0 0
i2 : i + 1 = 2
⊢ False

Tactic:
exact absurd ij' (by decide)

Premises used: absurd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : i + 1 < n
⊢ 0 < xn a1 (i + 1) % xn a1 n

Tactic:
exact
          x0.trans
            (eq_of_xn_modEq_lem3 _ (Nat.pos_of_ne_zero npos) (Nat.succ_pos _) (le_trans ij j2n)
              (_root_.ne_of_lt ij') fun ⟨_, n1, _, i2⟩ => by
              rw [n1, i2] at ij'; exact absurd ij' (by decide))

Premises used: Pell.eq_of_xn_modEq_lem3, False, _private.0.match_1, Nat.pos_of_ne_zero, Nat.succ_pos, LT.lt.trans, ne_of_lt, le_trans
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : a = 2 → n = 1 → (i = 0 → j ≠ 2) ∧ (i = 2 → j ≠ 0)
⊢ i = j

Tactic:
(le_total i j).elim
    (fun ij => eq_of_xn_modEq_le a1 ij j2n h fun ⟨a2, n1, i0, j2⟩ => (ntriv a2 n1).left i0 j2)
    fun ij =>
    (eq_of_xn_modEq_le a1 ij i2n h.symm fun ⟨a2, n1, j0, i2⟩ => (ntriv a2 n1).right i2 j0).symm

Premises used: False, Pell.eq_of_xn_modEq_le, le_total, And.right, And.left, Nat.ModEq.symm, _private.0.Pell.eq_of_xn_modEq.match_2, _private.0.Pell.eq_of_xn_modEq.match_1, Or.elim, Eq.symm
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
apply : n ≤ 2 * n
⊢ i ≤ 2 * n

Tactic:
apply le_trans hin

Premises used: le_trans
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
rw : n ≤ n + n
⊢ n ≤ 2 * n

Tactic:
rw [two_mul]

Premises used: two_mul
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ n ≤ n + n

Tactic:
apply Nat.le_add_left

Premises used: Nat.le_add_left
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
h_1 : a = 2
n1 : n = 1
h_2 : j = 0
i2 : i = 2
⊢ LE.le (α := ℕ) 2 1

Tactic:
rw [n1, i2] at hin
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
h_1 : a = 2
n1 : n = 1
h_2 : j = 0
i2 : i = 2
hin₁ : LE.le (α := ℕ) 2 1
⊢ j ≤ 4 * n

Tactic:
rw [n1, i2] at hin
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
h_1 : a = 2
n1 : n = 1
h_2 : j = 0
i2 : i = 2
hin₁ : LE.le (α := ℕ) 2 1
j4n₁ : j ≤ 4 * n
⊢ xn a1 j ≡ xn a1 i [MOD xn a1 n]

Tactic:
rw [n1, i2] at hin
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
h_1 : a = 2
n1 : n = 1
h_2 : j = 0
i2 : i = 2
hin₁ : LE.le (α := ℕ) 2 1
j4n₁ : j ≤ 4 * n
h₁ : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ i ≤ 2 * n

Tactic:
rw [n1, i2] at hin
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
h_1 : a = 2
n1 : n = 1
h_2 : j = 0
i2 : i = 2
hin₁ : LE.le (α := ℕ) 2 1
j4n₁ : j ≤ 4 * n
h₁ : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n₁ : i ≤ 2 * n
⊢ j ≤ 2 * n

Tactic:
rw [n1, i2] at hin
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
h_1 : a = 2
n1 : n = 1
h_2 : j = 0
i2 : i = 2
hin₁ : LE.le (α := ℕ) 2 1
j4n₁ : j ≤ 4 * n
h₁ : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n₁ : i ≤ 2 * n
j2n₁ : j ≤ 2 * n
⊢ a = 2

Tactic:
rw [n1, i2] at hin
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
h_1 : a = 2
n1 : n = 1
h_2 : j = 0
i2 : i = 2
hin₁ : LE.le (α := ℕ) 2 1
j4n₁ : j ≤ 4 * n
h₁ : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n₁ : i ≤ 2 * n
j2n₁ : j ≤ 2 * n
x : a = 2
⊢ n = 1

Tactic:
rw [n1, i2] at hin
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
h_1 : a = 2
n1 : n = 1
h_2 : j = 0
i2 : i = 2
hin₁ : LE.le (α := ℕ) 2 1
j4n₁ : j ≤ 4 * n
h₁ : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n₁ : i ≤ 2 * n
j2n₁ : j ≤ 2 * n
x : a = 2
n1₁ : n = 1
⊢ j = 0

Tactic:
rw [n1, i2] at hin
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
h_1 : a = 2
n1 : n = 1
h_2 : j = 0
i2 : i = 2
hin₁ : LE.le (α := ℕ) 2 1
j4n₁ : j ≤ 4 * n
h₁ : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n₁ : i ≤ 2 * n
j2n₁ : j ≤ 2 * n
x : a = 2
n1₁ : n = 1
x₁ : j = 0
⊢ i = 2

Tactic:
rw [n1, i2] at hin
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : LE.le (α := ℕ) 2 1
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
h_1 : a = 2
n1 : n = 1
h_2 : j = 0
i2 : i = 2
⊢ ¬LE.le (α := ℕ) 2 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : LE.le (α := ℕ) 2 1
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
h_1 : a = 2
n1 : n = 1
h_2 : j = 0
i2 : i = 2
⊢ False

Tactic:
exact absurd hin (by decide)

Premises used: absurd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
⊢ 4 * n - j ≤ 2 * n

Tactic:
lia
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
j42n : 4 * n - j ≤ 2 * n
t : xn a1 (4 * n - (4 * n - j)) ≡ xn a1 (4 * n - j) [MOD xn a1 n] := ⋯
rwa rwa₁ rwa₂ rwa₃ : ∀ (t : xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]), xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]
⊢ xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]

Tactic:
rwa [tsub_tsub_cancel_of_le j4n] at t

Premises used: tsub_tsub_cancel_of_le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
j42n : 4 * n - j ≤ 2 * n
⊢ a = 2 → n = 1 → (i = 0 → 4 * n - j ≠ 2) ∧ (i = 2 → 4 * n - j ≠ 0)

Tactic:
lia
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
this : i = 4 * n - j
rw : j + (4 * n - j) = 4 * n
rw₁ rw₂ : 4 * n = 4 * n
⊢ j + i = 4 * n

Tactic:
rw [this, add_tsub_cancel_of_le j4n]

Premises used: add_tsub_cancel_of_le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
⊢ LT.lt (α := ℕ) 0 4

Tactic:
decide
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
rw rw₁ : j % (4 * n) = j'
⊢ j % (4 * n) = j' % (4 * n)

Tactic:
rw [Nat.mod_eq_of_lt jl]

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j_1 n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j_1 ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j_1 % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j_1 ≡ j' [MOD 4 * n]
j : ℕ
⊢ xn a1 (j + 4 * n * 0) ≡ xn a1 j [MOD xn a1 n]

Tactic:
simp [ModEq.refl]

Premises used: Nat.ModEq.refl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i j_1 n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j_1 ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j_1 % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j_1 ≡ j' [MOD 4 * n]
j q : ℕ
IH : xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
succ : xn a1 (4 * n + (j + 4 * n * q)) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (j + 4 * n * (q + 1)) ≡ xn a1 j [MOD xn a1 n]

Tactic:
rw [Nat.mul_succ, ← add_assoc, add_comm]

Premises used: Nat.mul_succ, add_assoc, add_comm