awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n

Tactic:
have ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n := by
              rw [← two_mul, mul_comm,
                show xn a1 n = xn a1 (n - 1 + 1) by rw [tsub_add_cancel_of_le (succ_le_of_lt npos)],
                xn_succ]
              exact le_trans (Nat.mul_le_mul_left _ a1) (Nat.le_add_right _ _)
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
⊢ (n - 1).succ = n

Tactic:
have npm : (n - 1).succ = n := Nat.succ_pred_eq_of_pos npos
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
a₁ : i.succ ≤ (n - 1).succ
⊢ i ≤ n - 1

Tactic:
apply Nat.le_of_succ_le_succ

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

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

Tactic:
lin

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

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

Tactic:
have il : i ≤ n - 1 := by
              apply Nat.le_of_succ_le_succ
              rw [npm]
              exact lin
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
refl : ∀ (ill : i < n - 1), xn a1 (n - 1) + xn a1 i < xn a1 n
refl₁ : ∀ (ile : i = n - 1), xn a1 (n - 1) + xn a1 i < xn a1 n
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n

Tactic:
rcases lt_or_eq_of_le il with ill | ile

Premises used: lt_or_eq_of_le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ill : i < n - 1
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n

Tactic:
lt_of_lt_of_le (Nat.add_lt_add_left (strictMono_x a1 ill) _) ll

Premises used: Pell.strictMono_x, Nat.add_lt_add_left, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ill : i < n - 1
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n

Tactic:
exact lt_of_lt_of_le (Nat.add_lt_add_left (strictMono_x a1 ill) _) ll

Premises used: Pell.strictMono_x, Nat.add_lt_add_left, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
refl : xn a1 (n - 1) + xn a1 (n - 1) < xn a1 n
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n

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

Tactic:
apply lt_of_le_of_ne ll

Premises used: lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
refl : 2 * xn a1 (n - 1) ≠ xn a1 n
⊢ xn a1 (n - 1) + xn a1 (n - 1) ≠ xn a1 n

Tactic:
rw [← two_mul]

Premises used: two_mul
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
rwa rwa₁ rwa₂ rwa₃ : 2 * xn a1 (n - 1) = xn a1 n
⊢ 2 * xn a1 (n - 1) = xn a1 (n - 1 + 1)

Tactic:
rwa [tsub_add_cancel_of_le (succ_le_of_lt npos)]

Premises used: Nat.succ_le_of_lt, tsub_add_cancel_of_le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
⊢ a = 2

Tactic:
let ⟨a2, s1⟩ :=
                    @eq_of_xn_modEq_lem2 _ a1 (n - 1)
                      (by rwa [tsub_add_cancel_of_le (succ_le_of_lt npos)])
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
⊢ n - 1 = 0

Tactic:
let ⟨a2, s1⟩ :=
                    @eq_of_xn_modEq_lem2 _ a1 (n - 1)
                      (by rwa [tsub_add_cancel_of_le (succ_le_of_lt npos)])
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
s1 : n - 1 = 0
⊢ n = 1

Tactic:
have n1 : n = 1 := le_antisymm (tsub_eq_zero_iff_le.mp s1) npos
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
s1 : n - 1 = 0
n1 : n = 1
rw : Eq (α := ℕ) 2 2 ∧ Eq (α := ℕ) 1 1 ∧ HSub.hSub (α := ℕ) 1 1 = 0 ∧ HAdd.hAdd (α := ℕ) 1 1 = 2
⊢ a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2

Tactic:
rw [ile, a2, n1]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
s1 : n - 1 = 0
n1 : n = 1
⊢ Eq (α := ℕ) 2 2 ∧ Eq (α := ℕ) 1 1 ∧ HSub.hSub (α := ℕ) 1 1 = 0 ∧ HAdd.hAdd (α := ℕ) 1 1 = 2

Tactic:
⟨rfl, rfl, rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
s1 : n - 1 = 0
n1 : n = 1
⊢ Eq (α := ℕ) 2 2 ∧ Eq (α := ℕ) 1 1 ∧ HSub.hSub (α := ℕ) 1 1 = 0 ∧ HAdd.hAdd (α := ℕ) 1 1 = 2

Tactic:
exact ⟨rfl, rfl, rfl, rfl⟩
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
⊢ 2 * xn a1 (n - 1) ≠ xn a1 n

Tactic:
exact fun e =>
                ntriv <| by
                  let ⟨a2, s1⟩ :=
                    @eq_of_xn_modEq_lem2 _ a1 (n - 1)
                      (by rwa [tsub_add_cancel_of_le (succ_le_of_lt npos)])
                  have n1 : n = 1 := le_antisymm (tsub_eq_zero_iff_le.mp s1) npos
                  rw [ile, a2, n1]; exact ⟨rfl, rfl, rfl, rfl⟩
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
ein : i = n
refl : xn a1 (n - 1) < xn a1 n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n

Tactic:
rw [ein, Nat.mod_self, add_zero]

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

Tactic:
strictMono_x _ (Nat.pred_lt npos.ne')

Premises used: LT.lt.ne', Nat.pred_lt, Pell.strictMono_x
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
ein : i = n
⊢ xn a1 (n - 1) < xn a1 n

Tactic:
exact strictMono_x _ (Nat.pred_lt npos.ne')

Premises used: LT.lt.ne', Nat.pred_lt, Pell.strictMono_x
-- 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 : a = 2
n1 : n = 1
left_1 : i = 0
j2 : j = 2
⊢ HAdd.hAdd (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 2 1

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 : 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 : a = 2
n1 : n = 1
left_1 : i = 0
j2 : j = 2
j2n₁ : HAdd.hAdd (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 2 1
⊢ j + 1 ≠ n

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 : 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 : a = 2
n1 : n = 1
left_1 : i = 0
j2 : j = 2
j2n₁ : HAdd.hAdd (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 2 1
jnn₁ : j + 1 ≠ n
⊢ ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 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 : 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 : a = 2
n1 : n = 1
left_1 : 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)
⊢ ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)

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 : 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 : a = 2
n1 : n = 1
left_1 : 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)) : ℤ)
⊢ j = n ∨ n < j

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 : 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 : a = 2
n1 : n = 1
left_1 : 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
⊢ j > n

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 : 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 : a = 2
n1 : n = 1
left_1 : 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
⊢ j ≠ n

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 : 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 : a = 2
n1 : n = 1
left_1 : 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
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n

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 : 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 : a = 2
n1 : n = 1
left_1 : 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
⊢ i < j

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 : 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 : a = 2
n1 : n = 1
left_1 : 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
⊢ a = 2 ∧ n = 1 ∧ 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 : 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 : a = 2
n1 : n = 1
left_1 : 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
⊢ a = 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 : 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
⊢ n = 1

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 : 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
⊢ i = 0

Tactic:
rw [n1, j2] at j2n