awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ (↑(xn a1 n) : ℤ) ∣
    HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 n) : ℤ) * HMul.hMul (α := ℤ) (↑(yn a1 n) : ℤ) (↑(xn a1 j) : ℤ) +
      (↑(xn a1 j) : ℤ)

Tactic:
mod_cast (xn_modEq_x2n_add_lem _ n j)

Premises used: Nat.cast_mul._simp_1, Dvd.dvd, HMul.hMul, Pell.xn, congrArg, Nat.cast_add._simp_1, cast, Nat.cast, HAdd.hAdd, Pell.yn, congr, Pell.xn_modEq_x2n_add_lem, congrFun', _private.0.Pell.d, Eq.symm, Eq.trans, Int.ofNat_dvd._simp_1
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ (↑(xn a1 n) : ℤ) ∣
    HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 n) : ℤ) * HMul.hMul (α := ℤ) (↑(yn a1 n) : ℤ) (↑(xn a1 j) : ℤ) +
      (↑(xn a1 j) : ℤ)

Tactic:
exact mod_cast (xn_modEq_x2n_add_lem _ n j)

Premises used: Pell.xn_modEq_x2n_add_lem
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ (↑(d a1) : ℤ) * yz a1 n * (xz a1 j * yz a1 n) + xz a1 j - (↑(d a1) : ℤ) * yz a1 n * (xz a1 n * yz a1 j)

Tactic:
exact
      dvd_sub
        (by
          delta xz; delta yz
          rw [mul_comm (xn _ _ : ℤ)]
          exact mod_cast (xn_modEq_x2n_add_lem _ n j))
        ((dvd_mul_right _ _).mul_left _)
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ (↑(d a1) : ℤ) * yz a1 n * yz a1 (n - j) + xz a1 j

Tactic:
have h1 : xz a1 n ∣ d a1 * yz a1 n * yz a1 (n - j) + xz a1 j := by
    rw [yz_sub _ h, mul_sub_left_distrib, sub_add_eq_add_sub]
    exact
      dvd_sub
        (by
          delta xz; delta yz
          rw [mul_comm (xn _ _ : ℤ)]
          exact mod_cast (xn_modEq_x2n_add_lem _ n j))
        ((dvd_mul_right _ _).mul_left _)
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ (↑(d a1) : ℤ) * yz a1 n * yz a1 (n - j) + xz a1 j
rw : xn a1 n * xn a1 (n - j) + (d a1 * yn a1 n * yn a1 (n - j) + xn a1 j) ≡ HAdd.hAdd (α := ℕ) 0 0 [MOD xn a1 n]
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
rw [two_mul, add_tsub_assoc_of_le h, xn_add, add_assoc, ← zero_add 0]

Premises used: add_tsub_assoc_of_le, add_assoc, two_mul, zero_add, Pell.xn_add, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ (↑(d a1) : ℤ) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ Dvd.dvd (α := ℤ) (↑(xn a1 n) : ℤ) (↑(d a1 * yn a1 n * yn a1 (n - j) + xn a1 j) : ℤ)

Tactic:
simpa [xz, yz] using h1

Premises used: Pell.yz, Pell.xz
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ (↑(d a1) : ℤ) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 n * xn a1 (n - j) + (d a1 * yn a1 n * yn a1 (n - j) + xn a1 j) ≡ HAdd.hAdd (α := ℕ) 0 0 [MOD xn a1 n]

Tactic:
exact
    (dvd_mul_right _ _).modEq_zero_nat.add
      (Int.natCast_dvd_natCast.1 <| by simpa [xz, yz] using h1).modEq_zero_nat

Premises used: Nat.ModEq.add, Dvd.dvd.modEq_zero_nat, Iff.mp, dvd_mul_right, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
rw : n + n ≤ n + j
⊢ 2 * n - j + j ≤ n + j

Tactic:
rw [tsub_add_cancel_of_le h, two_mul]

Premises used: two_mul, tsub_add_cancel_of_le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ n + n ≤ n + j

Tactic:
Nat.add_le_add_left jn _

Premises used: Nat.add_le_add_left
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ n + n ≤ n + j

Tactic:
exact Nat.add_le_add_left jn _

Premises used: Nat.add_le_add_left
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ 2 * n - j + j ≤ n + j

Tactic:
have : 2 * n - j + j ≤ n + j := by
      rw [tsub_add_cancel_of_le h, two_mul]; exact Nat.add_le_add_left jn _
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
this : 2 * n - j + j ≤ n + j
t : xn a1 (2 * n - (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n] := ⋯
rwa : ∀ (t : xn a1 j + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]), xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (t : xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]), xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
rwa [tsub_tsub_cancel_of_le h, add_comm] at t

Premises used: add_comm, tsub_tsub_cancel_of_le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
rw : 0 ≡ xn a1 (2 * n + j) + xn a1 j [MOD xn a1 n]
⊢ 0 ≡ xn a1 j + xn a1 (2 * n + j) [MOD xn a1 n]

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ 0 ≡ xn a1 (2 * n + j) + xn a1 j [MOD xn a1 n]

Tactic:
(xn_modEq_x2n_add _ _ _).symm

Premises used: Pell.xn_modEq_x2n_add, Nat.ModEq.symm
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ 0 ≡ xn a1 (2 * n + j) + xn a1 j [MOD xn a1 n]

Tactic:
exact (xn_modEq_x2n_add _ _ _).symm

Premises used: Pell.xn_modEq_x2n_add, Nat.ModEq.symm
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
refine : xn a1 (4 * n + j) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]
⊢ xn a1 (4 * n + j) + xn a1 (2 * n + j) ≡ xn a1 j + xn a1 (2 * n + j) [MOD xn a1 n]

Tactic:
refine @ModEq.trans _ _ 0 _ ?_ (by rw [add_comm]; exact (xn_modEq_x2n_add _ _ _).symm)

Premises used: Nat.ModEq.trans
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
rw : xn a1 (2 * n + (2 * n + j)) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]
⊢ xn a1 (4 * n + j) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]

Tactic:
rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_assoc]

Premises used: add_assoc, right_distrib, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (2 * n + (2 * n + j)) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]

Tactic:
apply xn_modEq_x2n_add

Premises used: Pell.xn_modEq_x2n_add
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
rw rw₁ : 1 * n + n ≤ 1 * n + n
⊢ 2 * n ≤ 2 * n

Tactic:
rw [Nat.succ_mul]

Premises used: Nat.succ_mul
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
rw : 0 ≡ xn a1 (2 * n - j) + xn a1 j [MOD xn a1 n]
⊢ 0 ≡ xn a1 j + xn a1 (2 * n - j) [MOD xn a1 n]

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 (2 * n - j) + xn a1 j [MOD xn a1 n]

Tactic:
(xn_modEq_x2n_sub _ h).symm

Premises used: Pell.xn_modEq_x2n_sub, Nat.ModEq.symm
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 (2 * n - j) + xn a1 j [MOD xn a1 n]

Tactic:
exact (xn_modEq_x2n_sub _ h).symm

Premises used: Pell.xn_modEq_x2n_sub, Nat.ModEq.symm
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
refine : xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]
⊢ xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ xn a1 j + xn a1 (2 * n - j) [MOD xn a1 n]

Tactic:
refine @ModEq.trans _ _ 0 _ ?_ (by rw [add_comm]; exact (xn_modEq_x2n_sub _ h).symm)

Premises used: Nat.ModEq.trans
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
rw : xn a1 (2 * n + (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]
⊢ xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]

Tactic:
rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_tsub_assoc_of_le h']

Premises used: add_tsub_assoc_of_le, right_distrib, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (2 * n + (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]

Tactic:
apply xn_modEq_x2n_add

Premises used: Pell.xn_modEq_x2n_add
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
this : 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 j : ℕ
ij : i < j + 1
jn : j + 1 < n
this : 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:
this
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
this : 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 this
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
suffices : 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:
suffices xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n from
      (lt_or_eq_of_le (Nat.le_of_succ_le_succ ij)).elim
        (fun h => lt_trans (eq_of_xn_modEq_lem1 h (le_of_lt jn)) this) fun h => by
        rw [h]; exact this
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
rw : xn a1 j < xn a1 (j + 1)
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
rw [Nat.mod_eq_of_lt (strictMono_x _ (Nat.lt_of_succ_lt jn)),
        Nat.mod_eq_of_lt (strictMono_x _ jn)]

Premises used: Nat.mod_eq_of_lt, Pell.strictMono_x, Nat.lt_of_succ_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j < xn a1 (j + 1)

Tactic:
strictMono_x _ (Nat.lt_succ_self _)

Premises used: Nat.lt_succ_self, Pell.strictMono_x
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j < xn a1 (j + 1)

Tactic:
exact strictMono_x _ (Nat.lt_succ_self _)

Premises used: Nat.lt_succ_self, Pell.strictMono_x
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
h : 2 * xn a1 n = xn a1 (n + 1)
⊢ xn a1 n * 2 = xn a1 n * a + d a1 * yn a1 n

Tactic:
rw [xn_succ, mul_comm] at h

Premises used: Pell.xn_succ, mul_comm
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
h : xn a1 n * 2 = xn a1 n * a + d a1 * yn a1 n
⊢ n = 0

Tactic:
have : n = 0 :=
    n.eq_zero_or_pos.resolve_right fun np =>
      _root_.ne_of_lt
        (lt_of_le_of_lt (Nat.mul_le_mul_left _ a1)
          (Nat.lt_add_of_pos_right <| mul_pos (d_pos a1) (strictMono_y a1 np)))
        h
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
h : xn a1 n * 2 = xn a1 n * a + d a1 * yn a1 n
this : n = 0
refl : ∀ (h : xn a1 0 * 2 = xn a1 0 * a + d a1 * yn a1 0), a = 2 ∧ Eq (α := ℕ) 0 0
⊢ a = 2 ∧ n = 0

Tactic:
cases this
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
h : xn a1 0 * 2 = xn a1 0 * a + d a1 * yn a1 0
⊢ 2 = a

Tactic:
simp at h
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
h : 2 = a
⊢ a = 2 ∧ Eq (α := ℕ) 0 0

Tactic:
⟨h.symm, rfl⟩

Premises used: And.intro, Eq.symm, rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
h : 2 = a
⊢ a = 2 ∧ Eq (α := ℕ) 0 0

Tactic:
exact ⟨h.symm, rfl⟩
-- 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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ 2 * n - k < n

Tactic:
lia
-- 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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := ⋯
⊢ xn a1 (2 * n - k) ≤ xn a1 n

Tactic:
have xle : xn a1 (2 * n - k) ≤ xn a1 n := le_of_lt <| strictMono_x a1 k2nl
-- 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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := ⋯
xle : xn a1 (2 * n - k) ≤ xn a1 n
this : xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k)
rw : (↑(xn a1 n - xn a1 (2 * n - k)) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
rw₁ rw₂ :
  HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ) =
    HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)
⊢ (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)

Tactic:
rw [this, Int.ofNat_sub xle]

Premises used: Int.ofNat_sub
-- 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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := ⋯
xle : xn a1 (2 * n - k) ≤ xn a1 n
suffices : xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k)
⊢ (↑(xn a1 k % xn a1 n) : ℤ) = HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (2 * n - k)) : ℤ)

Tactic:
suffices xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k) by rw [this, Int.ofNat_sub xle]
-- 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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := ⋯
xle : xn a1 (2 * n - k) ≤ xn a1 n
rw : xn a1 k % xn a1 n = (xn a1 n - xn a1 (2 * n - k)) % xn a1 n
⊢ xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k)

Tactic:
rw [← Nat.mod_eq_of_lt (Nat.sub_lt (x_pos a1 n) (x_pos a1 (2 * n - k)))]

Premises used: HMul.hMul, HSub.hSub, Pell.x_pos, Nat.sub_lt, Nat.mod_eq_of_lt, 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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := ⋯
xle : xn a1 (2 * n - k) ≤ xn a1 n
apply : xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n - xn a1 (2 * n - k) + xn a1 (2 * n - k) [MOD xn a1 n]
⊢ xn a1 k % xn a1 n = (xn a1 n - xn a1 (2 * n - k)) % xn a1 n

Tactic:
apply ModEq.add_right_cancel' (xn a1 (2 * n - k))

Premises used: HMul.hMul, Pell.xn, HSub.hSub, Nat.ModEq.add_right_cancel', 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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := ⋯
xle : xn a1 (2 * n - k) ≤ xn a1 n
rw : xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n - xn a1 (2 * n - k) + xn a1 (2 * n - k) [MOD xn a1 n]

Tactic:
rw [tsub_add_cancel_of_le xle]

Premises used: tsub_add_cancel_of_le
-- 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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := ⋯
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 (2 * n - (2 * n - k)) + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]

Tactic:
have t := xn_modEq_x2n_sub_lem a1 k2nl.le
-- 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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := ⋯
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 (2 * n - (2 * n - k)) + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]

Tactic:
rw [tsub_tsub_cancel_of_le k2n] at t

Premises used: tsub_tsub_cancel_of_le
-- 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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := ⋯
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 k + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]

Tactic:
t.trans dvd_rfl.zero_modEq_nat

Premises used: dvd_rfl, Dvd.dvd.zero_modEq_nat, Nat.ModEq.trans
-- 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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := ⋯
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 k + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]

Tactic:
exact t.trans dvd_rfl.zero_modEq_nat

Premises used: dvd_rfl, Dvd.dvd.zero_modEq_nat, Nat.ModEq.trans
-- 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
refl :
  ∀ (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), xn a1 i % xn a1 n < xn a1 (n + 1) % xn a1 n
⊢ xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
cases jn
-- 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
refl : LT.lt (α := ℤ) (↑(xn a1 i % xn a1 n) : ℤ) (↑(xn a1 (n + 1) % xn a1 n) : ℤ)
⊢ xn a1 i % xn a1 n < xn a1 (n + 1) % xn a1 n

Tactic:
apply Int.lt_of_ofNat_lt_ofNat

Premises used: Int.lt_of_ofNat_lt_ofNat
-- 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
rw : n + n - (n + 1) = n - 1
rw₁ : n + n - n - 1 = n - 1
rw₂ rw₃ : n - 1 = n - 1
⊢ 2 * n - (n + 1) = n - 1

Tactic:
rw [two_mul, tsub_add_eq_tsub_tsub, add_tsub_cancel_right]

Premises used: two_mul, tsub_add_eq_tsub_tsub, add_tsub_cancel_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
refl : (↑(xn a1 i % xn a1 n) : ℤ) < HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (n - 1)) : ℤ)
⊢ LT.lt (α := ℤ) (↑(xn a1 i % xn a1 n) : ℤ) (↑(xn a1 (n + 1) % xn a1 n) : ℤ)

Tactic:
rw [lem2 (n + 1) (Nat.lt_succ_self _) j2n,
            show 2 * n - (n + 1) = n - 1 by
              rw [two_mul, tsub_add_eq_tsub_tsub, add_tsub_cancel_right]]

Premises used: Nat.lt_succ_self, HAdd.hAdd, OfNat.ofNat
-- 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
⊢ (↑(xn a1 i % xn a1 n) : ℤ) < HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (n - 1)) : ℤ)

Tactic:
lt_sub_left_of_add_lt (Int.ofNat_lt_ofNat_of_lt ?_)

Premises used: Int.ofNat_lt_ofNat_of_lt, lt_sub_left_of_add_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
refl : xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n
⊢ (↑(xn a1 i % xn a1 n) : ℤ) < HSub.hSub (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 (n - 1)) : ℤ)

Tactic:
refine lt_sub_left_of_add_lt (Int.ofNat_lt_ofNat_of_lt ?_)

Premises used: lt_sub_left_of_add_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
refl : ∀ (lin : i < n), xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n
refl₁ : ∀ (ein : i = n), xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n

Tactic:
rcases lt_or_eq_of_le <| Nat.le_of_succ_le_succ ij with lin | ein

Premises used: lt_or_eq_of_le, 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
refl : xn a1 (n - 1) + xn a1 i < xn a1 n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n

Tactic:
rw [Nat.mod_eq_of_lt (strictMono_x _ lin)]

Premises used: Nat.mod_eq_of_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
lin : i < n
rw rw₁ : xn a1 n = xn a1 n
⊢ xn a1 n = xn a1 (n - 1 + 1)

Tactic:
rw [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
rw : xn a1 (n - 1) * 2 ≤ xn a1 (n - 1) * a + d a1 * yn a1 (n - 1)
⊢ xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n

Tactic:
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]

Premises used: Pell.xn_succ, two_mul, mul_comm
-- 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) * 2 ≤ xn a1 (n - 1) * a + d a1 * yn a1 (n - 1)

Tactic:
le_trans (Nat.mul_le_mul_left _ a1) (Nat.le_add_right _ _)

Premises used: Nat.le_add_right, Nat.mul_le_mul_left, le_trans
-- 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) * 2 ≤ xn a1 (n - 1) * a + d a1 * yn a1 (n - 1)

Tactic:
exact le_trans (Nat.mul_le_mul_left _ a1) (Nat.le_add_right _ _)

Premises used: Nat.le_add_right, Nat.mul_le_mul_left, le_trans