-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xn_modEq_x2n_sub_lem {n j} (h : j ≤ n) : xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j

Tactic:
rw [yz_sub _ h, mul_sub_left_distrib, sub_add_eq_add_sub]

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * (xz a1 j * yz a1 n) + xz a1 j - ↑(Pell.d a1) * yz a1 n * (xz a1 n * yz a1 j)

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1) * yz a1 n * (↑(xn a1 j) * yz a1 n) + ↑(xn a1 j)

Tactic:
delta yz

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1) * ↑(yn a1 n) * (↑(xn a1 j) * ↑(yn a1 n)) + ↑(xn a1 j)

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1) * ↑(yn a1 n) * (↑(yn a1 n) * ↑(xn a1 j)) + ↑(xn a1 j)

Tactic:
exact mod_cast (xn_modEq_x2n_add_lem _ n j)

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1 * yn a1 n * yn a1 (n - j) + xn a1 j)

Tactic:
simpa [xz, yz] using h1

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

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 _)

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ 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]

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 n * xn a1 (n - j) + (Pell.d a1 * yn a1 n * yn a1 (n - j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * (xz a1 j * yz a1 n) + xz a1 j

Tactic:
delta xz

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1) * yz a1 n * (↑(xn a1 j) * yz a1 n) + ↑(xn a1 j)

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * (xz a1 j * yz a1 n) + xz a1 j - ↑(Pell.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 _)

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1) * ↑(yn a1 n) * (↑(xn a1 j) * ↑(yn a1 n)) + ↑(xn a1 j)

Tactic:
rw [mul_comm (xn _ _ : ℤ)]

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(Pell.d a1) * ↑(yn a1 n) * (↑(yn a1 n) * ↑(xn a1 j)) + ↑(xn a1 j)

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(Pell.d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 n * xn a1 (n - j) + (Pell.d a1 * yn a1 n * yn a1 (n - j) + xn a1 j) ≡ 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

Result:
no goals