awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]
⊢ xn a1 (4 * n + (j + 4 * n * q)) ≡ xn a1 j [MOD xn a1 n]

Tactic:
(xn_modEq_x4n_add _ _ _).trans IH

Premises used: Pell.xn_modEq_x4n_add, Nat.ModEq.trans
-- 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]
⊢ xn a1 (4 * n + (j + 4 * n * q)) ≡ xn a1 j [MOD xn a1 n]

Tactic:
exact (xn_modEq_x4n_add _ _ _).trans IH

Premises used: Pell.xn_modEq_x4n_add, Nat.ModEq.trans
-- 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 : ℕ
zero : xn a1 (j + 4 * n * 0) ≡ xn a1 j [MOD xn a1 n]
succ :
  ∀ (q : ℕ) (IH : xn a1 (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]
⊢ xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]

Tactic:
induction q with
    | zero => simp [ModEq.refl]
    | succ q IH =>
      rw [Nat.mul_succ, ← add_assoc, add_comm]
      exact (xn_modEq_x4n_add _ _ _).trans IH

Premises used: Nat.mul_succ, Nat.ModEq.refl, add_assoc, add_comm, Nat.zero, Nat.succ
-- 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
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
ji : j' = i
rwa rwa₁ rwa₂ rwa₃ : j ≡ j' [MOD 4 * n]
⊢ j ≡ i [MOD 4 * n]

Tactic:
rwa [← ji]
-- 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
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
ji : j' + i = 4 * n
rw : 4 * n ≡ 0 [MOD 4 * n]
⊢ j' + i ≡ 0 [MOD 4 * n]

Tactic:
rw [ji]
-- 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
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
ji : j' + i = 4 * n
⊢ 4 * n ≡ 0 [MOD 4 * n]

Tactic:
dvd_rfl.modEq_zero_nat

Premises used: Dvd.dvd.modEq_zero_nat, dvd_rfl
-- 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
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
ji : j' + i = 4 * n
⊢ 4 * n ≡ 0 [MOD 4 * n]

Tactic:
exact dvd_rfl.modEq_zero_nat

Premises used: Dvd.dvd.modEq_zero_nat, dvd_rfl
-- 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
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
rw : xn a1 (j % (4 * n) + 4 * n * (j / (4 * n))) ≡ xn a1 j' [MOD xn a1 n]
⊢ xn a1 j ≡ xn a1 j' [MOD xn a1 n]

Tactic:
rw [← Nat.mod_add_div j (4 * n)]

Premises used: HMul.hMul, Nat.mod_add_div, OfNat.ofNat
-- 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
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (j % (4 * n) + 4 * n * (j / (4 * n))) ≡ xn a1 j' [MOD xn a1 n]

Tactic:
this j' _
-- 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
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (j % (4 * n) + 4 * n * (j / (4 * n))) ≡ xn a1 j' [MOD xn a1 n]

Tactic:
exact this j' _
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
⊢ xn a1 0 ≡ xn b1 0 [MOD c] ∧ yn a1 0 ≡ yn b1 0 [MOD c]

Tactic:
simp [Nat.ModEq.refl]

Premises used: Nat.ModEq.refl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
⊢ xn a1 1 ≡ xn b1 1 [MOD c] ∧ yn a1 1 ≡ yn b1 1 [MOD c]

Tactic:
simpa [Nat.ModEq.refl]

Premises used: Nat.ModEq.refl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
rw : 2 * a * xn a1 (n + 1) ≡ 2 * b * xn b1 (n + 1) [MOD c]
⊢ xn a1 (n + 2) + xn a1 n ≡ xn b1 (n + 2) + xn b1 n [MOD c]

Tactic:
rw [xn_succ_succ a1, xn_succ_succ b1]

Premises used: Pell.xn_succ_succ
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * xn a1 (n + 1) ≡ 2 * b * xn b1 (n + 1) [MOD c]

Tactic:
(h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).left

Premises used: Nat.ModEq.mul_left, Nat.ModEq.mul, And.left, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * xn a1 (n + 1) ≡ 2 * b * xn b1 (n + 1) [MOD c]

Tactic:
exact (h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).left

Premises used: Nat.ModEq.mul_left, Nat.ModEq.mul, And.left, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
rw : 2 * a * yn a1 (n + 1) ≡ 2 * b * yn b1 (n + 1) [MOD c]
⊢ yn a1 (n + 2) + yn a1 n ≡ yn b1 (n + 2) + yn b1 n [MOD c]

Tactic:
rw [yn_succ_succ a1, yn_succ_succ b1]

Premises used: Pell.yn_succ_succ
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ 2 * b * yn b1 (n + 1) [MOD c]

Tactic:
(h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).right

Premises used: Nat.ModEq.mul_left, Nat.ModEq.mul, And.right, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ 2 * b * yn b1 (n + 1) [MOD c]

Tactic:
exact (h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).right

Premises used: Nat.ModEq.mul_left, Nat.ModEq.mul, And.right, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
rw :
  1 < a ∧
    k ≤ yn a1 k ∧
      (xn a1 k = 1 ∧ yn a1 k = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          xn a1 k * xn a1 k - (a * a - 1) * yn a1 k * yn a1 k = 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 k] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 k * yn a1 k ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * yn a1 k])
⊢ 1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])

Tactic:
rw [← hx, ← hy]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
k0 : k = 0
rw :
  0 ≤ yn a1 0 ∧
    (xn a1 0 = 1 ∧ yn a1 0 = 0 ∨
      ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
        xn a1 0 * xn a1 0 - (a * a - 1) * yn a1 0 * yn a1 0 = 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 0] ∧
                  b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 0 * yn a1 0 ∣ v ∧ s ≡ xn a1 0 [MOD u] ∧ t ≡ 0 [MOD 4 * yn a1 0])
⊢ k ≤ yn a1 k ∧
    (xn a1 k = 1 ∧ yn a1 k = 0 ∨
      ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
        xn a1 k * xn a1 k - (a * a - 1) * yn a1 k * yn a1 k = 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 k] ∧
                  b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 k * yn a1 k ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * yn a1 k])

Tactic:
rw [k0]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
k0 : k = 0
⊢ 0 ≤ yn a1 0 ∧
    (xn a1 0 = 1 ∧ yn a1 0 = 0 ∨
      ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
        xn a1 0 * xn a1 0 - (a * a - 1) * yn a1 0 * yn a1 0 = 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 0] ∧
                  b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 0 * yn a1 0 ∣ v ∧ s ≡ xn a1 0 [MOD u] ∧ t ≡ 0 [MOD 4 * yn a1 0])

Tactic:
⟨le_rfl, Or.inl ⟨rfl, rfl⟩⟩

Premises used: le_rfl, And.intro, Or.inl, rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
k0 : k = 0
⊢ 0 ≤ yn a1 0 ∧
    (xn a1 0 = 1 ∧ yn a1 0 = 0 ∨
      ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
        xn a1 0 * xn a1 0 - (a * a - 1) * yn a1 0 * yn a1 0 = 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 0] ∧
                  b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 0 * yn a1 0 ∣ v ∧ s ≡ xn a1 0 [MOD u] ∧ t ≡ 0 [MOD 4 * yn a1 0])

Tactic:
exact ⟨le_rfl, Or.inl ⟨rfl, rfl⟩⟩
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
refine :
  ∀ (kpos : k > 0),
    k ≤ yn a1 k ∧
      (xn a1 k = 1 ∧ yn a1 k = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          xn a1 k * xn a1 k - (a * a - 1) * yn a1 k * yn a1 k = 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 k] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 k * yn a1 k ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * yn a1 k])
⊢ 1 < a ∧
    k ≤ yn a1 k ∧
      (xn a1 k = 1 ∧ yn a1 k = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          xn a1 k * xn a1 k - (a * a - 1) * yn a1 k * yn a1 k = 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 k] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 k * yn a1 k ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * yn a1 k])

Tactic:
refine ⟨a1,
        (Nat.eq_zero_or_pos k).elim (fun k0 => by rw [k0]; exact ⟨le_rfl, Or.inl ⟨rfl, rfl⟩⟩)
          fun kpos => ?_⟩
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x_1 y_1 : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x_1 ∧ yn a1 k = y_1
a1 : 1 < a
hx : xn a1 k = x_1
hy : yn a1 k = y_1
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b ≡ a [MOD u]
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this : xn a1 1 < u
⊢ a < u

Tactic:
simpa using this
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x_1 y_1 : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x_1 ∧ yn a1 k = y_1
a1 : 1 < a
hx : xn a1 k = x_1
hy : yn a1 k = y_1
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a % u
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this_1 : xn a1 1 < u
this : a < u
⊢ b % u = a

Tactic:
rw [Nat.mod_eq_of_lt this] at ba

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x_1 y_1 : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x_1 ∧ yn a1 k = y_1
a1 : 1 < a
hx : xn a1 k = x_1
hy : yn a1 k = y_1
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a % u
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this_1 : xn a1 1 < u
this : a < u
ba₁ : b % u = a
⊢ b ≡ 1 [MOD 4 * y]

Tactic:
rw [Nat.mod_eq_of_lt this] at ba

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x_1 y_1 : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x_1 ∧ yn a1 k = y_1
a1 : 1 < a
hx : xn a1 k = x_1
hy : yn a1 k = y_1
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a % u
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this_1 : xn a1 1 < u
this : a < u
ba₁ : b % u = a
bm1₁ : b ≡ 1 [MOD 4 * y]
⊢ 1 < m

Tactic:
rw [Nat.mod_eq_of_lt this] at ba

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x_1 y_1 : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x_1 ∧ yn a1 k = y_1
a1 : 1 < a
hx : xn a1 k = x_1
hy : yn a1 k = y_1
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a % u
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this_1 : xn a1 1 < u
this : a < u
ba₁ : b % u = a
bm1₁ : b ≡ 1 [MOD 4 * y]
m1₁ : 1 < m
⊢ 0 < v

Tactic:
rw [Nat.mod_eq_of_lt this] at ba

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x_1 y_1 : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x_1 ∧ yn a1 k = y_1
a1 : 1 < a
hx : xn a1 k = x_1
hy : yn a1 k = y_1
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a % u
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this_1 : xn a1 1 < u
this : a < u
ba₁ : b % u = a
bm1₁ : b ≡ 1 [MOD 4 * y]
m1₁ : 1 < m
vp₁ : 0 < v
⊢ xn a1 1 < u

Tactic:
rw [Nat.mod_eq_of_lt this] at ba

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x_1 y_1 : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x_1 ∧ yn a1 k = y_1
a1 : 1 < a
hx : xn a1 k = x_1
hy : yn a1 k = y_1
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a % u
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this_1 : xn a1 1 < u
this : a < u
ba₁ : b % u = a
bm1₁ : b ≡ 1 [MOD 4 * y]
m1₁ : 1 < m
vp₁ : 0 < v
this₁ : xn a1 1 < u
⊢ a < u

Tactic:
rw [Nat.mod_eq_of_lt this] at ba

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x_1 y_1 : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x_1 ∧ yn a1 k = y_1
a1 : 1 < a
hx : xn a1 k = x_1
hy : yn a1 k = y_1
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this_1 : xn a1 1 < u
this : a < u
rw : b % u ≤ b
⊢ a ≤ b

Tactic:
rw [← ba]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x_1 y_1 : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x_1 ∧ yn a1 k = y_1
a1 : 1 < a
hx : xn a1 k = x_1
hy : yn a1 k = y_1
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this_1 : xn a1 1 < u
this : a < u
⊢ b % u ≤ b

Tactic:
apply Nat.mod_le

Premises used: Nat.mod_le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x_1 y_1 : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x_1 ∧ yn a1 k = y_1
a1 : 1 < a
hx : xn a1 k = x_1
hy : yn a1 k = y_1
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b ≡ a [MOD u]
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
b1 : 1 < b
s : ℕ := xn b1 k
t : ℕ := yn b1 k
sx : s ≡ x [MOD u]
rw : (↑(4 * y) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑1 : ℤ)
⊢ Dvd.dvd (α := ℤ) (↑(4 * y) : ℤ) (↑(b - 1) : ℤ)

Tactic:
rw [Int.ofNat_sub (le_of_lt b1)]

Premises used: Int.ofNat_sub, le_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x_1 y_1 : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x_1 ∧ yn a1 k = y_1
a1 : 1 < a
hx : xn a1 k = x_1
hy : yn a1 k = y_1
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b ≡ a [MOD u]
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
b1 : 1 < b
s : ℕ := xn b1 k
t : ℕ := yn b1 k
sx : s ≡ x [MOD u]
⊢ (↑(4 * y) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑1 : ℤ)

Tactic:
bm1.symm.dvd

Premises used: Nat.ModEq.symm, Nat.ModEq.dvd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x_1 y_1 : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x_1 ∧ yn a1 k = y_1
a1 : 1 < a
hx : xn a1 k = x_1
hy : yn a1 k = y_1
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b ≡ a [MOD u]
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
b1 : 1 < b
s : ℕ := xn b1 k
t : ℕ := yn b1 k
sx : s ≡ x [MOD u]
⊢ (↑(4 * y) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑1 : ℤ)

Tactic:
exact bm1.symm.dvd

Premises used: Nat.ModEq.symm, Nat.ModEq.dvd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
h : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
kpos : k > 0
⊢ k ≤ yn a1 k ∧
    (xn a1 k = 1 ∧ yn a1 k = 0 ∨
      ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
        xn a1 k * xn a1 k - (a * a - 1) * yn a1 k * yn a1 k = 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 k] ∧
                  b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 k * yn a1 k ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * yn a1 k])

Tactic:
exact
      let x := xn a1 k
      let y := yn a1 k
      let m := 2 * (k * y)
      let u := xn a1 m
      let v := yn a1 m
      have ky : k ≤ y := yn_ge_n a1 k
      have yv : y * y ∣ v := (ysq_dvd_yy a1 k).trans <| (y_dvd_iff _ _ _).2 <| dvd_mul_left _ _
      have uco : Nat.Coprime u (4 * y) :=
        have : 2 ∣ v :=
          modEq_zero_iff_dvd.1 <| (yn_modEq_two _ _).trans (dvd_mul_right _ _).modEq_zero_nat
        have : Nat.Coprime u 2 := (xy_coprime a1 m).coprime_dvd_right this
        (this.mul_right this).mul_right <|
          (xy_coprime _ _).coprime_dvd_right (dvd_of_mul_left_dvd yv)
      let ⟨b, ba, bm1⟩ := chineseRemainder uco a 1
      have m1 : 1 < m :=
        have : 0 < k * y := mul_pos kpos (strictMono_y a1 kpos)
        Nat.mul_le_mul_left 2 this
      have vp : 0 < v := strictMono_y a1 (lt_trans zero_lt_one m1)
      have b1 : 1 < b :=
        have : xn a1 1 < u := strictMono_x a1 m1
        have : a < u := by simpa using this
        lt_of_lt_of_le a1 <| by
          delta ModEq at ba; rw [Nat.mod_eq_of_lt this] at ba; rw [← ba]
          apply Nat.mod_le
      let s := xn b1 k
      let t := yn b1 k
      have sx : s ≡ x [MOD u] := (xy_modEq_of_modEq b1 a1 ba k).left
      have tk : t ≡ k [MOD 4 * y] :=
        have : 4 * y ∣ 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 _ _).of_dvd this
      ⟨ky,
        Or.inr
          ⟨u, v, s, t, b, pell_eq _ _, pell_eq _ _, pell_eq _ _, b1, bm1, ba, vp, yv, sx, tk⟩⟩

Premises used: Iff.mpr, Pell.ysq_dvd_yy, Pell.yn_ge_n, HMul.hMul, Pell.xn, Dvd.dvd.modEq_zero_nat, dvd_of_mul_left_dvd, Pell.xy_coprime, Nat.Coprime.mul_right, dvd_mul_left, Pell.y_dvd_iff, Pell.yn, Iff.mp, dvd_mul_right, Pell.yn_modEq_two, Nat.modEq_zero_iff_dvd, OfNat.ofNat, Nat.ModEq.trans, Nat.Coprime.coprime_dvd_right, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
h :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ y
o :
  x = 1 ∧ y = 0 ∨
    ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
⊢ k ≤ 0

Tactic:
rw [y0] at ky
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
h :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ y
o :
  x = 1 ∧ y = 0 ∨
    ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
ky₁ : k ≤ 0
⊢ x = 1 ∧ y = 0 ∨
    ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]

Tactic:
rw [y0] at ky
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a k x y : ℕ
h :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ y
o :
  x = 1 ∧ y = 0 ∨
    ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
ky₁ : k ≤ 0
o₁ :
  x = 1 ∧ y = 0 ∨
    ∃ (u : ℕ) (v : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
⊢ x = 1

Tactic:
rw [y0] at ky