a : ℕ
a1 : 1 < a
n j : ℕ
h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (Pell.d a1 * yn a1 n * yn a1 n + 1) * xn a1 j
⊢ xn a1 n ∣ Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 n ∣ Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
have h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j =
    (d a1 * yn a1 n * yn a1 n + 1) * xn a1 j := by
  simp [add_mul, mul_assoc]
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (Pell.d a1 * yn a1 n * yn a1 n + 1) * xn a1 j
h2 : Pell.d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
⊢ xn a1 n ∣ Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (Pell.d a1 * yn a1 n * yn a1 n + 1) * xn a1 j
⊢ xn a1 n ∣ Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
have h2 : d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n := by
  zify at *
  apply add_eq_of_eq_sub' (Eq.symm (pell_eqz a1 n))
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j
h2 : Pell.d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
⊢ xn a1 n ∣ Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (Pell.d a1 * yn a1 n * yn a1 n + 1) * xn a1 j
h2 : Pell.d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
⊢ xn a1 n ∣ Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
rw [h2] at h1
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j
h2 : Pell.d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
⊢ xn a1 n ∣ xn a1 n * (xn a1 n * xn a1 j)
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j
h2 : Pell.d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
⊢ xn a1 n ∣ Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
rw [h1, mul_assoc]
no goals
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j
h2 : Pell.d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
⊢ xn a1 n ∣ xn a1 n * (xn a1 n * xn a1 j)
exact dvd_mul_right _ _
no goals
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (Pell.d a1 * yn a1 n * yn a1 n + 1) * xn a1 j
simp [add_mul, mul_assoc]
a : ℕ
a1 : 1 < a
n j : ℕ
h1 :
  ↑(Pell.d a1) * ↑(yn a1 n) * (↑(yn a1 n) * ↑(xn a1 j)) + ↑(xn a1 j) =
    (↑(Pell.d a1) * ↑(yn a1 n) * ↑(yn a1 n) + 1) * ↑(xn a1 j)
⊢ ↑(Pell.d a1) * ↑(yn a1 n) * ↑(yn a1 n) + 1 = ↑(xn a1 n) * ↑(xn a1 n)
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (Pell.d a1 * yn a1 n * yn a1 n + 1) * xn a1 j
⊢ Pell.d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
zify at *
no goals
a : ℕ
a1 : 1 < a
n j : ℕ
h1 :
  ↑(Pell.d a1) * ↑(yn a1 n) * (↑(yn a1 n) * ↑(xn a1 j)) + ↑(xn a1 j) =
    (↑(Pell.d a1) * ↑(yn a1 n) * ↑(yn a1 n) + 1) * ↑(xn a1 j)
⊢ ↑(Pell.d a1) * ↑(yn a1 n) * ↑(yn a1 n) + 1 = ↑(xn a1 n) * ↑(xn a1 n)
apply add_eq_of_eq_sub' (Eq.symm (pell_eqz a1 n))