awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
⊢ n > 0

Tactic:
rw [e, Nat.mod_zero] at hp

Premises used: Nat.mod_zero
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
hp₁ : n > 0
⊢ (yn a1 m).Coprime (xn a1 (m * (n / m)))

Tactic:
rw [e, Nat.mod_zero] at hp

Premises used: Nat.mod_zero
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
hp₁ : n > 0
co₁ : (yn a1 m).Coprime (xn a1 (m * (n / m)))
⊢ m = 0

Tactic:
rw [e, Nat.mod_zero] at hp

Premises used: Nat.mod_zero
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
⊢ yn a1 0 ∣ yn a1 n

Tactic:
rw [e] at h
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
h₁ : yn a1 0 ∣ yn a1 n
⊢ n > 0

Tactic:
rw [e] at h
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
h₁ : yn a1 0 ∣ yn a1 n
hp₁ : n > 0
⊢ (yn a1 m).Coprime (xn a1 (m * (n / m)))

Tactic:
rw [e] at h
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
h₁ : yn a1 0 ∣ yn a1 n
hp₁ : n > 0
co₁ : (yn a1 m).Coprime (xn a1 (m * (n / m)))
⊢ m = 0

Tactic:
rw [e] at h
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 0 ∣ yn a1 n
hp : n > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
⊢ False

Tactic:
_root_.ne_of_lt (strictMono_y a1 hp) (eq_zero_of_zero_dvd h).symm

Premises used: Pell.strictMono_y, eq_zero_of_zero_dvd, Eq.symm, ne_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 0 ∣ yn a1 n
hp : n > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
⊢ False

Tactic:
exact _root_.ne_of_lt (strictMono_y a1 hp) (eq_zero_of_zero_dvd h).symm

Premises used: Pell.strictMono_y, eq_zero_of_zero_dvd, Eq.symm, ne_of_lt
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
⊢ 0 < m

Tactic:
have m0 : 0 < m :=
          m.eq_zero_or_pos.resolve_left fun e => by
            rw [e, Nat.mod_zero] at hp;rw [e] at h
            exact _root_.ne_of_lt (strictMono_y a1 hp) (eq_zero_of_zero_dvd h).symm
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
m0 : 0 < m
⊢ yn a1 m ∣ xn a1 (n % m) * yn a1 (m * (n / m)) + yn a1 (n % m) * xn a1 (m * (n / m))

Tactic:
rw [← Nat.mod_add_div n m, yn_add] at h

Premises used: Pell.yn_add, Nat.mod_add_div
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
m0 : 0 < m
h₁ : yn a1 m ∣ xn a1 (n % m) * yn a1 (m * (n / m)) + yn a1 (n % m) * xn a1 (m * (n / m))
⊢ n % m > 0

Tactic:
rw [← Nat.mod_add_div n m, yn_add] at h

Premises used: Pell.yn_add, Nat.mod_add_div
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
m0 : 0 < m
h₁ : yn a1 m ∣ xn a1 (n % m) * yn a1 (m * (n / m)) + yn a1 (n % m) * xn a1 (m * (n / m))
hp₁ : n % m > 0
⊢ (yn a1 m).Coprime (xn a1 (m * (n / m)))

Tactic:
rw [← Nat.mod_add_div n m, yn_add] at h

Premises used: Pell.yn_add, Nat.mod_add_div
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
m0 : 0 < m
h₁ : yn a1 m ∣ xn a1 (n % m) * yn a1 (m * (n / m)) + yn a1 (n % m) * xn a1 (m * (n / m))
hp₁ : n % m > 0
co₁ : (yn a1 m).Coprime (xn a1 (m * (n / m)))
⊢ 0 < m

Tactic:
rw [← Nat.mod_add_div n m, yn_add] at h

Premises used: Pell.yn_add, Nat.mod_add_div
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ xn a1 (n % m) * yn a1 (m * (n / m)) + yn a1 (n % m) * xn a1 (m * (n / m))
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
m0 : 0 < m
⊢ False

Tactic:
not_le_of_gt (strictMono_y _ <| Nat.mod_lt n m0)
            (Nat.le_of_dvd (strictMono_y _ hp) <|
              co.dvd_of_dvd_mul_right <|
                (Nat.dvd_add_iff_right <| (y_mul_dvd _ _ _).mul_left _).2 h)

Premises used: Iff.mpr, Pell.strictMono_y, Dvd.dvd.mul_left, Nat.mod_lt, Pell.y_mul_dvd, not_le_of_gt, Nat.dvd_add_iff_right, Nat.le_of_dvd, Nat.Coprime.dvd_of_dvd_mul_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ xn a1 (n % m) * yn a1 (m * (n / m)) + yn a1 (n % m) * xn a1 (m * (n / m))
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
m0 : 0 < m
⊢ False

Tactic:
exact
          not_le_of_gt (strictMono_y _ <| Nat.mod_lt n m0)
            (Nat.le_of_dvd (strictMono_y _ hp) <|
              co.dvd_of_dvd_mul_right <|
                (Nat.dvd_add_iff_right <| (y_mul_dvd _ _ _).mul_left _).2 h)

Premises used: Iff.mpr, Pell.strictMono_y, Dvd.dvd.mul_left, Nat.mod_lt, Pell.y_mul_dvd, not_le_of_gt, Nat.dvd_add_iff_right, Nat.le_of_dvd, Nat.Coprime.dvd_of_dvd_mul_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m ∣ n
k : ℕ
e : n = m * k
rw : yn a1 m ∣ yn a1 (m * k)
⊢ yn a1 m ∣ yn a1 n

Tactic:
rw [e]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m ∣ n
k : ℕ
e : n = m * k
⊢ yn a1 m ∣ yn a1 (m * k)

Tactic:
apply y_mul_dvd

Premises used: Pell.y_mul_dvd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ xn a1 (n * 0) ≡ HPow.hPow (β := ℕ) (xn a1 n) 0 [MOD HPow.hPow (β := ℕ) (yn a1 n) 2] ∧
    yn a1 (n * 0) ≡ 0 * xn a1 n ^ HSub.hSub (α := ℕ) 0 1 * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]

Tactic:
simp [Nat.ModEq.refl]

Premises used: Nat.ModEq.refl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
⊢ xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]

Tactic:
let ⟨hx, hy⟩ := xy_modEq_yn n k
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
⊢ yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]

Tactic:
let ⟨hx, hy⟩ := xy_modEq_yn n k
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
h₂ : d a1 * yn a1 (n * k) * yn a1 n ≡ 0 [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
⊢ xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
h₂ : yn a1 n * yn a1 n ∣ d a1 * yn a1 (n * k) * yn a1 n
⊢ d a1 * yn a1 (n * k) * yn a1 n ≡ 0 [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]

Tactic:
rw [modEq_zero_iff_dvd, sq]

Premises used: sq, Nat.modEq_zero_iff_dvd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
h₂ : yn a1 n ∣ d a1 * yn a1 (n * k)
⊢ yn a1 n * yn a1 n ∣ d a1 * yn a1 (n * k) * yn a1 n

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
h₂ : yn a1 n ∣ yn a1 (n * k)
⊢ yn a1 n ∣ d a1 * yn a1 (n * k)

Tactic:
apply dvd_mul_of_dvd_right

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
h₂ : yn a1 (n * k) ≡ 0 [MOD yn a1 n]
⊢ yn a1 n ∣ yn a1 (n * k)

Tactic:
rw [← modEq_zero_iff_dvd]

Premises used: Nat.modEq_zero_iff_dvd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
⊢ Ne (α := ℕ) 3 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
h₂ : k * xn a1 n ^ (k - 1) * yn a1 n ≡ 0 [MOD yn a1 n]
⊢ yn a1 (n * k) ≡ 0 [MOD yn a1 n]

Tactic:
refine (hy.of_dvd <| dvd_pow_self _ <| by decide).trans ?_

Premises used: dvd_pow_self, Nat.ModEq.of_dvd, Nat.ModEq.trans
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
⊢ k * xn a1 n ^ (k - 1) * yn a1 n ≡ 0 [MOD yn a1 n]

Tactic:
simp [modEq_zero_iff_dvd]

Premises used: Nat.modEq_zero_iff_dvd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
⊢ xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]

Tactic:
have L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡
        xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2] := by
      gcongr
      rw [modEq_zero_iff_dvd, sq]
      gcongr
      apply dvd_mul_of_dvd_right
      rw [← modEq_zero_iff_dvd]
      refine (hy.of_dvd <| dvd_pow_self _ <| by decide).trans ?_
      simp [modEq_zero_iff_dvd]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
h₁ : xn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
h₂ : yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ k * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
⊢ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 3]

Tactic:
gcongr ?_ + ?_
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
h₁ : xn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 2 * yn a1 n]
⊢ xn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]

Tactic:
rw [_root_.pow_succ]

Premises used: pow_succ
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
⊢ xn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 2 * yn a1 n]

Tactic:
hx.mul_right' _

Premises used: Nat.ModEq.mul_right'
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
⊢ xn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 2 * yn a1 n]

Tactic:
exact hx.mul_right' _

Premises used: Nat.ModEq.mul_right'
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
zero :
  ∀ (hx : xn a1 (n * 0) ≡ HPow.hPow (β := ℕ) (xn a1 n) 0 [MOD HPow.hPow (β := ℕ) (yn a1 n) 2])
    (hy : yn a1 (n * 0) ≡ 0 * xn a1 n ^ HSub.hSub (α := ℕ) 0 1 * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3])
    (L :
      xn a1 (n * 0) * xn a1 n + d a1 * yn a1 (n * 0) * yn a1 n ≡ HPow.hPow (β := ℕ) (xn a1 n) 0 * xn a1 n + 0 [MOD
        HPow.hPow (β := ℕ) (yn a1 n) 2]),
    0 * xn a1 n ^ HSub.hSub (α := ℕ) 0 1 * yn a1 n * xn a1 n = 0 * HPow.hPow (β := ℕ) (xn a1 n) 0 * yn a1 n
succ :
  ∀ (k : ℕ) (hx : xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD HPow.hPow (β := ℕ) (yn a1 n) 2])
    (hy : yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3])
    (L :
      xn a1 (n * (k + 1)) * xn a1 n + d a1 * yn a1 (n * (k + 1)) * yn a1 n ≡ xn a1 n ^ (k + 1) * xn a1 n + 0 [MOD
        HPow.hPow (β := ℕ) (yn a1 n) 2]),
    (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n * xn a1 n = (k + 1) * xn a1 n ^ (k + 1) * yn a1 n
⊢ k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n

Tactic:
rcases k with - | k
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
hx : xn a1 (n * 0) ≡ HPow.hPow (β := ℕ) (xn a1 n) 0 [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * 0) ≡ 0 * xn a1 n ^ HSub.hSub (α := ℕ) 0 1 * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * 0) * xn a1 n + d a1 * yn a1 (n * 0) * yn a1 n ≡ HPow.hPow (β := ℕ) (xn a1 n) 0 * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
⊢ 0 * xn a1 n ^ HSub.hSub (α := ℕ) 0 1 * yn a1 n * xn a1 n = 0 * HPow.hPow (β := ℕ) (xn a1 n) 0 * yn a1 n

Tactic:
simp [_root_.pow_succ]

Premises used: pow_succ
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * (k + 1)) * xn a1 n + d a1 * yn a1 (n * (k + 1)) * yn a1 n ≡ xn a1 n ^ (k + 1) * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
succ : (k + 1) * xn a1 n ^ k * yn a1 n * xn a1 n = (k + 1) * (xn a1 n ^ k * xn a1 n) * yn a1 n
⊢ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n * xn a1 n = (k + 1) * xn a1 n ^ (k + 1) * yn a1 n

Tactic:
simp [_root_.pow_succ]

Premises used: pow_succ
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * (k + 1)) * xn a1 n + d a1 * yn a1 (n * (k + 1)) * yn a1 n ≡ xn a1 n ^ (k + 1) * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
⊢ (k + 1) * xn a1 n ^ k * yn a1 n * xn a1 n = (k + 1) * (xn a1 n ^ k * xn a1 n) * yn a1 n

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
⊢ k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n

Tactic:
have : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n := by
          rcases k with - | k <;> simp [_root_.pow_succ]; ring_nf
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
this : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n
h₂ : yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
⊢ yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ k * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]

Tactic:
rw [← this]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
this : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n
⊢ yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
⊢ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 3]

Tactic:
have R : xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡
        xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 3] := by
      gcongr ?_ + ?_
      · rw [_root_.pow_succ]
        exact hx.mul_right' _
      · have : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n := by
          rcases k with - | k <;> simp [_root_.pow_succ]; ring_nf
        rw [← this]
        gcongr
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
R :
  xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 3]
rw :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n [MOD
      HPow.hPow (β := ℕ) (yn a1 n) 2] ∧
    xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
      HPow.hPow (β := ℕ) (yn a1 n) 3]
⊢ xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD HPow.hPow (β := ℕ) (yn a1 n) 2] ∧
    yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]

Tactic:
rw [add_tsub_cancel_right, Nat.mul_succ, xn_add, yn_add, pow_succ (xn _ n), Nat.succ_mul,
      add_comm (k * xn _ n ^ k) (xn _ n ^ k), right_distrib]

Premises used: Nat.mul_succ, HMul.hMul, Pell.yn_add, Pell.xn, pow_succ, add_comm, Nat.succ_mul, HPow.hPow, Pell.xn_add, right_distrib, add_tsub_cancel_right
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
R :
  xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 3]
⊢ xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n [MOD
      HPow.hPow (β := ℕ) (yn a1 n) 2] ∧
    xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
      HPow.hPow (β := ℕ) (yn a1 n) 3]

Tactic:
⟨L, R⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
L :
  xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 2]
R :
  xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
    HPow.hPow (β := ℕ) (yn a1 n) 3]
⊢ xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n [MOD
      HPow.hPow (β := ℕ) (yn a1 n) 2] ∧
    xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
      HPow.hPow (β := ℕ) (yn a1 n) 3]

Tactic:
exact ⟨L, R⟩
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ yn a1 n * yn a1 n ∣ HPow.hPow (β := ℕ) (yn a1 n) 3

Tactic:
simp [_root_.pow_succ]

Premises used: pow_succ
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ yn a1 n * yn a1 n ∣ yn a1 n * xn a1 n ^ (yn a1 n - 1) * yn a1 n

Tactic:
simp [mul_dvd_mul_left, mul_assoc]

Premises used: mul_assoc, mul_dvd_mul_left
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0 : n = 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (nt : 0 ∣ t) (n0 : n = 0), yn a1 0 ∣ t
⊢ yn a1 n ∣ t

Tactic:
rwa [n0] at nt ⊢
-- 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
let : ∀ (k : ℕ) (ke : t = n * k), yn a1 n ∣ t
⊢ yn a1 n ∣ t

Tactic:
let ⟨k, ke⟩ := nt
-- 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) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]

Tactic:
have xm := (xy_modEq_yn a1 n k).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
xm : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
⊢ yn a1 t ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]

Tactic:
rw [← ke] at xm
-- 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
xm : yn a1 t ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
⊢ yn a1 n * yn a1 n ∣ HPow.hPow (β := ℕ) (yn a1 n) 3

Tactic:
simp [_root_.pow_succ]

Premises used: pow_succ
-- 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
xm : yn a1 t ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
⊢ k * xn a1 n ^ (k - 1) * yn a1 n ≡ 0 [MOD yn a1 n * yn a1 n]

Tactic:
exact (xm.of_dvd <| by simp [_root_.pow_succ]).symm.trans h.modEq_zero_nat

Premises used: Dvd.dvd.modEq_zero_nat, Nat.ModEq.symm, Nat.ModEq.of_dvd, Nat.ModEq.trans