awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0l : 0 < n
k : ℕ
ke : t = n * k
⊢ yn a1 n ∣ k * xn a1 n ^ (k - 1)

Tactic:
have : yn a1 n ∣ k * xn a1 n ^ (k - 1) :=
      Nat.dvd_of_mul_dvd_mul_right (strictMono_y a1 n0l) <|
        modEq_zero_iff_dvd.1 <| by
          have xm := (xy_modEq_yn a1 n k).right; rw [← ke] at xm
          exact (xm.of_dvd <| by simp [_root_.pow_succ]).symm.trans h.modEq_zero_nat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0l : 0 < n
k : ℕ
ke : t = n * k
this : yn a1 n ∣ k * xn a1 n ^ (k - 1)
rw : yn a1 n ∣ n * k
⊢ yn a1 n ∣ t

Tactic:
rw [ke]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0l : 0 < n
k : ℕ
ke : t = n * k
this : yn a1 n ∣ k * xn a1 n ^ (k - 1)
⊢ yn a1 n ∣ n * k

Tactic:
dvd_mul_of_dvd_right (((xy_coprime _ _).pow_left _).symm.dvd_of_dvd_mul_right this) _

Premises used: Nat.Coprime.symm, dvd_mul_of_dvd_right, Pell.xy_coprime, Nat.Coprime.pow_left, Nat.Coprime.dvd_of_dvd_mul_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0l : 0 < n
k : ℕ
ke : t = n * k
this : yn a1 n ∣ k * xn a1 n ^ (k - 1)
⊢ yn a1 n ∣ n * k

Tactic:
exact dvd_mul_of_dvd_right (((xy_coprime _ _).pow_left _).symm.dvd_of_dvd_mul_right this) _

Premises used: Nat.Coprime.symm, dvd_mul_of_dvd_right, Pell.xy_coprime, Nat.Coprime.pow_left, Nat.Coprime.dvd_of_dvd_mul_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
re : (pellZd a1 (n + 2) + pellZd a1 n).re = ((↑(2 * a) : ℤ√(↑(d a1) : ℤ)) * pellZd a1 (n + 1)).re
im : (pellZd a1 (n + 2) + pellZd a1 n).im = ((↑(2 * a) : ℤ√(↑(d a1) : ℤ)) * pellZd a1 (n + 1)).im
⊢ pellZd a1 (n + 2) + pellZd a1 n = (↑(2 * a) : ℤ√(↑(d a1) : ℤ)) * pellZd a1 (n + 1)

Tactic:
ext
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
re :
  (HMul.hMul (α := ℤ) (↑(xn a1 n) : ℤ) (↑a : ℤ) + (HMul.hMul (α := ℤ) (↑a : ℤ) (↑a : ℤ) - 1) * (↑(yn a1 n) : ℤ)) *
          (↑a : ℤ) +
        (HMul.hMul (α := ℤ) (↑a : ℤ) (↑a : ℤ) - 1) * ((↑(xn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 n) : ℤ) (↑a : ℤ)) +
      (↑(xn a1 n) : ℤ) =
    HMul.hMul (α := ℤ) 2 (↑a : ℤ) *
      (HMul.hMul (α := ℤ) (↑(xn a1 n) : ℤ) (↑a : ℤ) + (HMul.hMul (α := ℤ) (↑a : ℤ) (↑a : ℤ) - 1) * (↑(yn a1 n) : ℤ))
⊢ (pellZd a1 (n + 2) + pellZd a1 n).re = ((↑(2 * a) : ℤ√(↑(d a1) : ℤ)) * pellZd a1 (n + 1)).re

Tactic:
simp [dz_val, az]

Premises used: Pell.dz_val, Pell.az
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
im :
  HMul.hMul (α := ℤ) (↑(xn a1 n) : ℤ) (↑a : ℤ) + (HMul.hMul (α := ℤ) (↑a : ℤ) (↑a : ℤ) - 1) * (↑(yn a1 n) : ℤ) +
        ((↑(xn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 n) : ℤ) (↑a : ℤ)) * (↑a : ℤ) +
      (↑(yn a1 n) : ℤ) =
    HMul.hMul (α := ℤ) 2 (↑a : ℤ) * ((↑(xn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 n) : ℤ) (↑a : ℤ))
⊢ (pellZd a1 (n + 2) + pellZd a1 n).im = ((↑(2 * a) : ℤ√(↑(d a1) : ℤ)) * pellZd a1 (n + 1)).im

Tactic:
simp [dz_val, az]

Premises used: Pell.dz_val, Pell.az
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (HMul.hMul (α := ℤ) (↑(xn a1 n) : ℤ) (↑a : ℤ) + (HMul.hMul (α := ℤ) (↑a : ℤ) (↑a : ℤ) - 1) * (↑(yn a1 n) : ℤ)) *
          (↑a : ℤ) +
        (HMul.hMul (α := ℤ) (↑a : ℤ) (↑a : ℤ) - 1) * ((↑(xn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 n) : ℤ) (↑a : ℤ)) +
      (↑(xn a1 n) : ℤ) =
    HMul.hMul (α := ℤ) 2 (↑a : ℤ) *
      (HMul.hMul (α := ℤ) (↑(xn a1 n) : ℤ) (↑a : ℤ) + (HMul.hMul (α := ℤ) (↑a : ℤ) (↑a : ℤ) - 1) * (↑(yn a1 n) : ℤ))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ HMul.hMul (α := ℤ) (↑(xn a1 n) : ℤ) (↑a : ℤ) + (HMul.hMul (α := ℤ) (↑a : ℤ) (↑a : ℤ) - 1) * (↑(yn a1 n) : ℤ) +
        ((↑(xn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 n) : ℤ) (↑a : ℤ)) * (↑a : ℤ) +
      (↑(yn a1 n) : ℤ) =
    HMul.hMul (α := ℤ) 2 (↑a : ℤ) * ((↑(xn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 n) : ℤ) (↑a : ℤ))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ pellZd a1 (n + 2) + pellZd a1 n = (↑(2 * a) : ℤ√(↑(d a1) : ℤ)) * pellZd a1 (n + 1)

Tactic:
have := pellZd_succ_succ a1 n
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
this :
  HAdd.hAdd (α := ℤ√(↑(d a1) : ℤ)) { re := (↑(xn a1 (n + 2)) : ℤ), im := (↑(yn a1 (n + 2)) : ℤ) : ℤ√(↑(d a1) : ℤ) }
      { re := (↑(xn a1 n) : ℤ), im := (↑(yn a1 n) : ℤ) : ℤ√(↑(d a1) : ℤ) } =
    HMul.hMul (α := ℤ√(↑(d a1) : ℤ)) (↑(2 * a) : ℤ√(↑(d a1) : ℤ))
      { re := (↑(xn a1 (n + 1)) : ℤ), im := (↑(yn a1 (n + 1)) : ℤ) }
⊢ HAdd.hAdd (α := ℤ√(↑(d a1) : ℤ)) { re := (↑(xn a1 (n + 2)) : ℤ), im := (↑(yn a1 (n + 2)) : ℤ) : ℤ√(↑(d a1) : ℤ) }
      { re := (↑(xn a1 n) : ℤ), im := (↑(yn a1 n) : ℤ) : ℤ√(↑(d a1) : ℤ) } =
    { re := HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(xn a1 (n + 1)) : ℤ),
      im := HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(yn a1 (n + 1)) : ℤ) }

Tactic:
rw [Zsqrtd.nsmul_val (2 * a : ℕ)] at this

Premises used: HMul.hMul, Zsqrtd.nsmul_val, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
this :
  HAdd.hAdd (α := ℤ√(↑(d a1) : ℤ)) { re := (↑(xn a1 (n + 2)) : ℤ), im := (↑(yn a1 (n + 2)) : ℤ) : ℤ√(↑(d a1) : ℤ) }
      { re := (↑(xn a1 n) : ℤ), im := (↑(yn a1 n) : ℤ) : ℤ√(↑(d a1) : ℤ) } =
    { re := HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(xn a1 (n + 1)) : ℤ),
      im := HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(yn a1 (n + 1)) : ℤ) }
⊢ Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := (↑(xn a1 (n + 2)) : ℤ), im := (↑(yn a1 (n + 2)) : ℤ) : ℤ√(↑(d a1) : ℤ) } +
      Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := (↑(xn a1 n) : ℤ), im := (↑(yn a1 n) : ℤ) : ℤ√(↑(d a1) : ℤ) } =
    HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(xn a1 (n + 1)) : ℤ)

Tactic:
injection this with h₁ h₂
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
this :
  HAdd.hAdd (α := ℤ√(↑(d a1) : ℤ)) { re := (↑(xn a1 (n + 2)) : ℤ), im := (↑(yn a1 (n + 2)) : ℤ) : ℤ√(↑(d a1) : ℤ) }
      { re := (↑(xn a1 n) : ℤ), im := (↑(yn a1 n) : ℤ) : ℤ√(↑(d a1) : ℤ) } =
    { re := HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(xn a1 (n + 1)) : ℤ),
      im := HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(yn a1 (n + 1)) : ℤ) }
h₁ :
  Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := (↑(xn a1 (n + 2)) : ℤ), im := (↑(yn a1 (n + 2)) : ℤ) : ℤ√(↑(d a1) : ℤ) } +
      Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := (↑(xn a1 n) : ℤ), im := (↑(yn a1 n) : ℤ) : ℤ√(↑(d a1) : ℤ) } =
    HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(xn a1 (n + 1)) : ℤ)
⊢ Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := (↑(xn a1 (n + 2)) : ℤ), im := (↑(yn a1 (n + 2)) : ℤ) : ℤ√(↑(d a1) : ℤ) } +
      Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := (↑(xn a1 n) : ℤ), im := (↑(yn a1 n) : ℤ) : ℤ√(↑(d a1) : ℤ) } =
    HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(yn a1 (n + 1)) : ℤ)

Tactic:
injection this with h₁ h₂
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
h₁ :
  Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := (↑(xn a1 (n + 2)) : ℤ), im := (↑(yn a1 (n + 2)) : ℤ) : ℤ√(↑(d a1) : ℤ) } +
      Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := (↑(xn a1 n) : ℤ), im := (↑(yn a1 n) : ℤ) : ℤ√(↑(d a1) : ℤ) } =
    HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(xn a1 (n + 1)) : ℤ)
h₂ :
  Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := (↑(xn a1 (n + 2)) : ℤ), im := (↑(yn a1 (n + 2)) : ℤ) : ℤ√(↑(d a1) : ℤ) } +
      Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := (↑(xn a1 n) : ℤ), im := (↑(yn a1 n) : ℤ) : ℤ√(↑(d a1) : ℤ) } =
    HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(yn a1 (n + 1)) : ℤ)
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Tactic:
grind
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1)

Tactic:
(xy_succ_succ a1 n).1

Premises used: Pell.xy_succ_succ, And.left
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Tactic:
(xy_succ_succ a1 n).2

Premises used: Pell.xy_succ_succ, And.right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
rw : (↑(xn a1 (n + 2) + xn a1 n) : ℤ) = HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(xn a1 (n + 1)) : ℤ)
rw₁ : Eq (α := ℤ) (↑(xn a1 (n + 2) + xn a1 n) : ℤ) (↑(2 * a * xn a1 (n + 1)) : ℤ)
rw₂ rw₃ : Eq (α := ℤ) (↑(2 * a * xn a1 (n + 1)) : ℤ) (↑(2 * a * xn a1 (n + 1)) : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑(xn a1 (n + 2)) : ℤ) (↑(xn a1 n) : ℤ) = HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(xn a1 (n + 1)) : ℤ)

Tactic:
rw [← Int.natCast_add, ← Int.natCast_mul, xn_succ_succ]

Premises used: Int.natCast_add, Int.natCast_mul, Pell.xn_succ_succ
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
rw : (↑(yn a1 (n + 2) + yn a1 n) : ℤ) = HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(yn a1 (n + 1)) : ℤ)
rw₁ : Eq (α := ℤ) (↑(yn a1 (n + 2) + yn a1 n) : ℤ) (↑(2 * a * yn a1 (n + 1)) : ℤ)
rw₂ rw₃ : Eq (α := ℤ) (↑(2 * a * yn a1 (n + 1)) : ℤ) (↑(2 * a * yn a1 (n + 1)) : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑(yn a1 (n + 2)) : ℤ) (↑(yn a1 n) : ℤ) = HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(yn a1 (n + 1)) : ℤ)

Tactic:
rw [← Int.natCast_add, ← Int.natCast_mul, yn_succ_succ]

Premises used: Int.natCast_add, Int.natCast_mul, Pell.yn_succ_succ
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
⊢ yn a1 0 ≡ 0 [MOD a - 1]

Tactic:
simp [Nat.ModEq.refl]

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

Tactic:
simp [Nat.ModEq.refl]

Premises used: Nat.ModEq.refl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ n + 2 + n = 2 * (n + 1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
rw : 2 * a * yn a1 (n + 1) ≡ 2 * (n + 1) [MOD a - 1]
⊢ yn a1 (n + 2) + yn a1 n ≡ n + 2 + n [MOD a - 1]

Tactic:
rw [yn_succ_succ, (by ring : n + 2 + n = 2 * (n + 1))]

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

Tactic:
((modEq_sub a1.le).mul_left 2).mul (yn_modEq_a_sub_one (n + 1))

Premises used: Nat.ModEq.mul_left, Nat.ModEq.mul, LT.lt.le, Nat.modEq_sub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ 2 * (n + 1) [MOD a - 1]

Tactic:
exact ((modEq_sub a1.le).mul_left 2).mul (yn_modEq_a_sub_one (n + 1))

Premises used: Nat.ModEq.mul_left, Nat.ModEq.mul, LT.lt.le, Nat.modEq_sub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
⊢ yn a1 0 ≡ 0 [MOD 2]

Tactic:
rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
⊢ yn a1 1 ≡ 1 [MOD 2]

Tactic:
simp [Nat.ModEq.refl]

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

Tactic:
rw [yn_succ_succ, mul_assoc, (by ring : n + 2 + n = 2 * (n + 1))]

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

Tactic:
(dvd_mul_right 2 _).modEq_zero_nat.trans (dvd_mul_right 2 _).zero_modEq_nat

Premises used: Dvd.dvd.modEq_zero_nat, dvd_mul_right, OfNat.ofNat, Dvd.dvd.zero_modEq_nat, Nat.ModEq.trans
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 2 * (a * yn a1 (n + 1)) ≡ 2 * (n + 1) [MOD 2]

Tactic:
exact (dvd_mul_right 2 _).modEq_zero_nat.trans (dvd_mul_right 2 _).zero_modEq_nat

Premises used: Dvd.dvd.modEq_zero_nat, dvd_mul_right, OfNat.ofNat, Dvd.dvd.zero_modEq_nat, Nat.ModEq.trans
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
y2 y1 y0 yn1 yn0 xn1 xn0 ay a2 : ℤ
⊢ (a2 * yn1 - yn0) * ay + y2 - (a2 * xn1 - xn0) = y2 - a2 * y1 + y0 + a2 * (yn1 * ay + y1 - xn1) - (yn0 * ay + y0 - xn0)

Tactic:
ring
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
y : ℕ
⊢ HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1 ∣
    yz a1 0 * HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ) + (↑(HPow.hPow (β := ℕ) y 0) : ℤ) - xz a1 0

Tactic:
simp [xz, yz]

Premises used: Pell.yz, Pell.xz
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
y : ℕ
⊢ HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1 ∣
    yz a1 1 * HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ) + (↑(HPow.hPow (β := ℕ) y 1) : ℤ) - xz a1 1

Tactic:
simp [xz, yz]

Premises used: Pell.yz, Pell.xz
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
y n : ℕ
simp :
  (↑y : ℤ) * ((↑y : ℤ) * HPow.hPow (α := ℤ) (↑y : ℤ) n) - (↑a : ℤ) * ((↑y : ℤ) * HPow.hPow (α := ℤ) (↑y : ℤ) n * 2) +
      HPow.hPow (α := ℤ) (↑y : ℤ) n =
    -(HPow.hPow (α := ℤ) (↑y : ℤ) n *
        ((↑a : ℤ) * HMul.hMul (α := ℤ) (↑y : ℤ) 2 - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1))
⊢ (↑(y ^ (n + 2)) : ℤ) - HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(y ^ (n + 1)) : ℤ) + (↑(y ^ n) : ℤ) =
    (HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1) * -(↑(y ^ n) : ℤ)

Tactic:
simp [_root_.pow_succ, mul_comm, mul_left_comm]

Premises used: pow_succ, mul_left_comm, mul_comm
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
y n : ℕ
⊢ (↑y : ℤ) * ((↑y : ℤ) * HPow.hPow (α := ℤ) (↑y : ℤ) n) - (↑a : ℤ) * ((↑y : ℤ) * HPow.hPow (α := ℤ) (↑y : ℤ) n * 2) +
      HPow.hPow (α := ℤ) (↑y : ℤ) n =
    -(HPow.hPow (α := ℤ) (↑y : ℤ) n *
        ((↑a : ℤ) * HMul.hMul (α := ℤ) (↑y : ℤ) 2 - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1))

Tactic:
ring
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
y n : ℕ
⊢ HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1 ∣
    (↑(y ^ (n + 2)) : ℤ) - HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(y ^ (n + 1)) : ℤ) + (↑(y ^ n) : ℤ)

Tactic:
have : (2 * a * y - y * y - 1 : ℤ) ∣ ↑(y ^ (n + 2)) - ↑(2 * a) * ↑(y ^ (n + 1)) + ↑(y ^ n) :=
      ⟨-↑(y ^ n), by
        simp [_root_.pow_succ, mul_comm, mul_left_comm]
        ring⟩
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
y n : ℕ
this :
  HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1 ∣
    (↑(y ^ (n + 2)) : ℤ) - HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(y ^ (n + 1)) : ℤ) + (↑(y ^ n) : ℤ)
rw :
  HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1 ∣
    (↑(y ^ (n + 2)) : ℤ) - HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(y ^ (n + 1)) : ℤ) + (↑(y ^ n) : ℤ) +
        (↑(2 * a) : ℤ) * (yz a1 (n + 1) * HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ) + (↑(y ^ (n + 1)) : ℤ) - xz a1 (n + 1)) -
      (yz a1 n * HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ) + (↑(y ^ n) : ℤ) - xz a1 n)
⊢ HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1 ∣
    yz a1 (n + 2) * HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ) + (↑(y ^ (n + 2)) : ℤ) - xz a1 (n + 2)

Tactic:
rw [xz_succ_succ, yz_succ_succ, x_sub_y_dvd_pow_lem ↑(y ^ (n + 2)) ↑(y ^ (n + 1)) ↑(y ^ n)]

Premises used: Nat.cast, Pell.yz_succ_succ, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Pell.x_sub_y_dvd_pow_lem, Pell.xz_succ_succ
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
y n : ℕ
this :
  HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1 ∣
    (↑(y ^ (n + 2)) : ℤ) - HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(y ^ (n + 1)) : ℤ) + (↑(y ^ n) : ℤ)
⊢ HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1 ∣
    (↑(y ^ (n + 2)) : ℤ) - HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(y ^ (n + 1)) : ℤ) + (↑(y ^ n) : ℤ) +
        (↑(2 * a) : ℤ) * (yz a1 (n + 1) * HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ) + (↑(y ^ (n + 1)) : ℤ) - xz a1 (n + 1)) -
      (yz a1 n * HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ) + (↑(y ^ n) : ℤ) - xz a1 n)

Tactic:
_root_.dvd_sub (dvd_add this <| (x_sub_y_dvd_pow _ (n + 1)).mul_left _)
      (x_sub_y_dvd_pow _ n)

Premises used: Dvd.dvd.mul_left, dvd_sub, HAdd.hAdd, OfNat.ofNat, dvd_add
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
y n : ℕ
this :
  HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1 ∣
    (↑(y ^ (n + 2)) : ℤ) - HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(y ^ (n + 1)) : ℤ) + (↑(y ^ n) : ℤ)
⊢ HMul.hMul (α := ℤ) 2 (↑a : ℤ) * (↑y : ℤ) - HMul.hMul (α := ℤ) (↑y : ℤ) (↑y : ℤ) - 1 ∣
    (↑(y ^ (n + 2)) : ℤ) - HMul.hMul (α := ℤ) (↑(2 * a) : ℤ) (↑(y ^ (n + 1)) : ℤ) + (↑(y ^ n) : ℤ) +
        (↑(2 * a) : ℤ) * (yz a1 (n + 1) * HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ) + (↑(y ^ (n + 1)) : ℤ) - xz a1 (n + 1)) -
      (yz a1 n * HSub.hSub (α := ℤ) (↑a : ℤ) (↑y : ℤ) + (↑(y ^ n) : ℤ) - xz a1 n)

Tactic:
exact _root_.dvd_sub (dvd_add this <| (x_sub_y_dvd_pow _ (n + 1)).mul_left _)
      (x_sub_y_dvd_pow _ n)

Premises used: Dvd.dvd.mul_left, dvd_sub, HAdd.hAdd, OfNat.ofNat, dvd_add
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ 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

Tactic:
simp [add_mul, mul_assoc]

Premises used: add_mul, mul_assoc
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ 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

Tactic:
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]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
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
zify :
  ∀
    (h1 :
      HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 n) : ℤ) * HMul.hMul (α := ℤ) (↑(yn a1 n) : ℤ) (↑(xn a1 j) : ℤ) +
          (↑(xn a1 j) : ℤ) =
        (HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 n) : ℤ) * (↑(yn a1 n) : ℤ) + 1) * (↑(xn a1 j) : ℤ)),
    HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 n) : ℤ) * (↑(yn a1 n) : ℤ) + 1 =
      HMul.hMul (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 n) : ℤ)
⊢ d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n

Tactic:
zify at *
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h1 :
  HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 n) : ℤ) * HMul.hMul (α := ℤ) (↑(yn a1 n) : ℤ) (↑(xn a1 j) : ℤ) +
      (↑(xn a1 j) : ℤ) =
    (HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 n) : ℤ) * (↑(yn a1 n) : ℤ) + 1) * (↑(xn a1 j) : ℤ)
⊢ HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 n) : ℤ) * (↑(yn a1 n) : ℤ) + 1 =
    HMul.hMul (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 n) : ℤ)

Tactic:
apply add_eq_of_eq_sub' (Eq.symm (pell_eqz a1 n))

Premises used: Pell.pell_eqz, add_eq_of_eq_sub', Eq.symm
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
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
⊢ d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n

Tactic:
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))
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
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
h2 : d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
⊢ d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j

Tactic:
rw [h2] at h1
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
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
h2 : d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
h1₁ : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j
⊢ d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n

Tactic:
rw [h2] at h1
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j
h2 : d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
rw : xn a1 n ∣ xn a1 n * (xn a1 n * xn a1 j)
⊢ xn a1 n ∣ d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j

Tactic:
rw [h1, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j
h2 : 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)

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j
h2 : 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)

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n 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_assoc, xn_add, add_assoc, ← zero_add 0]

Premises used: add_assoc, two_mul, zero_add, Pell.xn_add, OfNat.ofNat
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n 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:
(dvd_mul_right (xn a1 n) (xn a1 (n + j))).modEq_zero_nat.add ?_

Premises used: Nat.ModEq.add, Pell.xn, Dvd.dvd.modEq_zero_nat, HAdd.hAdd, dvd_mul_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
refine : d a1 * yn a1 n * yn a1 (n + j) + xn a1 j ≡ 0 [MOD xn a1 n]
⊢ 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:
refine (dvd_mul_right (xn a1 n) (xn a1 (n + j))).modEq_zero_nat.add ?_

Premises used: Nat.ModEq.add, Pell.xn, Dvd.dvd.modEq_zero_nat, HAdd.hAdd, dvd_mul_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
rw :
  d a1 * yn a1 n * (xn a1 n * yn a1 j) + (d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j) ≡ HAdd.hAdd (α := ℕ) 0 0 [MOD
    xn a1 n]
⊢ d a1 * yn a1 n * yn a1 (n + j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
rw [yn_add, left_distrib, add_assoc, ← zero_add 0]

Premises used: Pell.yn_add, add_assoc, zero_add, OfNat.ofNat, left_distrib
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ d a1 * yn a1 n * (xn a1 n * yn a1 j) + (d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j) ≡ HAdd.hAdd (α := ℕ) 0 0 [MOD
    xn a1 n]

Tactic:
((dvd_mul_right _ _).mul_left _).modEq_zero_nat.add (xn_modEq_x2n_add_lem _ _ _).modEq_zero_nat

Premises used: Nat.ModEq.add, Dvd.dvd.modEq_zero_nat, Dvd.dvd.mul_left, Pell.xn_modEq_x2n_add_lem, dvd_mul_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ d a1 * yn a1 n * (xn a1 n * yn a1 j) + (d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j) ≡ HAdd.hAdd (α := ℕ) 0 0 [MOD
    xn a1 n]

Tactic:
exact
    ((dvd_mul_right _ _).mul_left _).modEq_zero_nat.add (xn_modEq_x2n_add_lem _ _ _).modEq_zero_nat

Premises used: Nat.ModEq.add, Dvd.dvd.modEq_zero_nat, Dvd.dvd.mul_left, Pell.xn_modEq_x2n_add_lem, dvd_mul_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
rw : 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)
⊢ xz a1 n ∣ (↑(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]

Premises used: Pell.yz_sub, mul_sub_left_distrib, sub_add_eq_add_sub
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
rw :
  (↑(xn a1 n) : ℤ) ∣
    HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 n) : ℤ) * HMul.hMul (α := ℤ) (↑(yn a1 n) : ℤ) (↑(xn a1 j) : ℤ) +
      (↑(xn a1 j) : ℤ)
⊢ (↑(xn a1 n) : ℤ) ∣
    HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 n) : ℤ) * HMul.hMul (α := ℤ) (↑(xn a1 j) : ℤ) (↑(yn a1 n) : ℤ) +
      (↑(xn a1 j) : ℤ)

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

Premises used: Pell.xn, Nat.cast, mul_comm