awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
⊢ xn a1 (m + n) = xn a1 m * xn a1 n + d a1 * yn a1 m * yn a1 n
have im_eq : (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
Tactic: injection pellZd_add a1 m n with h _
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
im_eq : (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ xn a1 (m + n) = xn a1 m * xn a1 n + d a1 * yn a1 m * yn a1 n
have zify : (↑(xn a1 (m + n)) : ℤ) =
  HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(xn a1 n) : ℤ) +
    HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 m) : ℤ) * (↑(yn a1 n) : ℤ)
Tactic: zify
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
im_eq : (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ (↑(xn a1 (m + n)) : ℤ) =
    HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(xn a1 n) : ℤ) +
      HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 m) : ℤ) * (↑(yn a1 n) : ℤ)
have rw : (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im =
  HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(xn a1 n) : ℤ) +
    HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 m) : ℤ) * (↑(yn a1 n) : ℤ)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
⊢ yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n
have re_eq : (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
Tactic: injection pellZd_add a1 m n with _ h
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq :
  (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
⊢ yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n
have h : (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
Tactic: injection pellZd_add a1 m n with _ h
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq :
  (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
h : (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n
have zify : (↑(yn a1 (m + n)) : ℤ) =
  HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(yn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 m) : ℤ) (↑(xn a1 n) : ℤ)
Tactic: zify
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq :
  (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
h : (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ (↑(yn a1 (m + n)) : ℤ) =
    HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(yn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 m) : ℤ) (↑(xn a1 n) : ℤ)
have rw : (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re =
  HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(yn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 m) : ℤ) (↑(xn a1 n) : ℤ)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 (n + (m - n)) = pellZd a1 n * pellZd a1 (m - n) := ⋯
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
have t₁ : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
Tactic: rw [add_tsub_cancel_of_le h] at t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
have rw : pellZd a1 (m - n) = pellZd a1 n * pellZd a1 (m - n) * star (pellZd a1 n)
Tactic: rw [t, mul_comm (pellZd _ n) _, mul_assoc, isPell_norm.1 (isPell_pellZd _ _), mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
rw : pellZd a1 (m - n) = pellZd a1 n * pellZd a1 (m - n) * star (pellZd a1 n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
have rw₁ : pellZd a1 (m - n) = pellZd a1 (m - n) * pellZd a1 n * star (pellZd a1 n)
Tactic: rw [t, mul_comm (pellZd _ n) _, mul_assoc, isPell_norm.1 (isPell_pellZd _ _), mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
rw : pellZd a1 (m - n) = pellZd a1 n * pellZd a1 (m - n) * star (pellZd a1 n)
rw₁ : pellZd a1 (m - n) = pellZd a1 (m - n) * pellZd a1 n * star (pellZd a1 n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
have rw₂ : pellZd a1 (m - n) = pellZd a1 (m - n) * (pellZd a1 n * star (pellZd a1 n))
Tactic: rw [t, mul_comm (pellZd _ n) _, mul_assoc, isPell_norm.1 (isPell_pellZd _ _), mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
rw : pellZd a1 (m - n) = pellZd a1 n * pellZd a1 (m - n) * star (pellZd a1 n)
rw₁ : pellZd a1 (m - n) = pellZd a1 (m - n) * pellZd a1 n * star (pellZd a1 n)
rw₂ : pellZd a1 (m - n) = pellZd a1 (m - n) * (pellZd a1 n * star (pellZd a1 n))
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
have rw₃ : pellZd a1 (m - n) = pellZd a1 (m - n) * 1
Tactic: rw [t, mul_comm (pellZd _ n) _, mul_assoc, isPell_norm.1 (isPell_pellZd _ _), mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
rw : pellZd a1 (m - n) = pellZd a1 n * pellZd a1 (m - n) * star (pellZd a1 n)
rw₁ : pellZd a1 (m - n) = pellZd a1 (m - n) * pellZd a1 n * star (pellZd a1 n)
rw₂ : pellZd a1 (m - n) = pellZd a1 (m - n) * (pellZd a1 n * star (pellZd a1 n))
rw₃ : pellZd a1 (m - n) = pellZd a1 (m - n) * 1
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
have rw₄ : pellZd a1 (m - n) = pellZd a1 (m - n)
Tactic: rw [t, mul_comm (pellZd _ n) _, mul_assoc, isPell_norm.1 (isPell_pellZd _ _), mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ xz a1 (m - n) = xz a1 m * xz a1 n - (↑(d a1) : ℤ) * yz a1 m * yz a1 n
have rw : xz a1 (m - n) = xz a1 m * xz a1 n + (↑(d a1) : ℤ) * yz a1 m * -yz a1 n
Tactic: rw [sub_eq_add_neg, ← mul_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ yz a1 (m - n) = xz a1 n * yz a1 m - xz a1 m * yz a1 n
have rw : yz a1 (m - n) = xz a1 m * -yz a1 n + yz a1 m * xz a1 n
Tactic: rw [sub_eq_add_neg, ← mul_neg, mul_comm, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
h : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
p : xn a1 n * xn a1 n - d a1 * yn a1 n * yn a1 n = 1 := ⋯
⊢ k ∣ 1
have rw : k ∣ xn a1 n * xn a1 n - d a1 * yn a1 n * yn a1 n
Tactic: rw [← p]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
⊢ yn a1 m ≤ yn a1 n
have rw : yn a1 n ≤ yn a1 n
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
⊢ yn a1 m < yn a1 (n + 1)
have this : yn a1 m ≤ yn a1 n
Tactic: have : yn a1 m ≤ yn a1 n :=
      Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_y hl)
        fun e => by rw [e]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m < xn a1 n + yn a1 n * a
have refine : yn a1 m ≤ yn a1 n * a
Tactic: refine lt_of_le_of_lt ?_ (Nat.lt_add_of_pos_left <| x_pos a1 n)
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m ≤ yn a1 n * a
have rw : yn a1 m * 1 ≤ yn a1 n * a
Tactic: rw [← mul_one (yn a1 m)]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
⊢ xn a1 m ≤ xn a1 n
have rw : xn a1 n ≤ xn a1 n
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
⊢ xn a1 m < xn a1 (n + 1)
have this : xn a1 m ≤ xn a1 n
Tactic: have : xn a1 m ≤ xn a1 n :=
      Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_x hl)
        fun e => by rw [e]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
⊢ xn a1 m < xn a1 n * a + d a1 * yn a1 n
have refine : xn a1 n < xn a1 n * a
Tactic: refine lt_of_lt_of_le (lt_of_le_of_lt this ?_) (Nat.le_add_right _ _)
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
⊢ xn a1 n < xn a1 n * a
have t : xn a1 n * 1 < xn a1 n * a
Tactic: have t := Nat.mul_lt_mul_of_pos_left a1 (x_pos a1 n)
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
t : xn a1 n * 1 < xn a1 n * a
⊢ xn a1 n < xn a1 n * a
have rwa : ∀ (t : xn a1 n < xn a1 n * a), xn a1 n < xn a1 n * a
Tactic: rwa [mul_one] at t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
⊢ yn a1 n ∣ yn a1 (n * (k + 1))
have rw : yn a1 n ∣ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n
Tactic: rw [Nat.mul_succ, yn_add]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
⊢ False
have co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
Tactic: have co : Nat.Coprime (yn a1 m) (xn a1 (m * (n / m))) :=
          Nat.Coprime.symm <| (xy_coprime a1 _).coprime_dvd_right (y_mul_dvd a1 m (n / m))
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
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
⊢ False
have hp₁ : n > 0
Tactic: rw [e, Nat.mod_zero] at hp
Cleared hypotheses: hp, co, e
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
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
⊢ False
have h₁ : yn a1 0 ∣ yn a1 n
Tactic: rw [e] at h
Cleared hypotheses: h, hp, co, e
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
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)))
⊢ False
have m0 : 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
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
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
⊢ False
have h₁ : 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
Cleared hypotheses: h, hp, co, m0
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m ∣ n
k : ℕ
e : n = m * k
⊢ yn a1 m ∣ yn a1 n
have rw : yn a1 m ∣ yn a1 (m * k)
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
⊢ 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]
have hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
Tactic: let ⟨hx, hy⟩ := xy_modEq_yn n k
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
⊢ 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]
have hy : 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
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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]
have h₂ : d a1 * yn a1 (n * k) * yn a1 n ≡ 0 [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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]
⊢ d a1 * yn a1 (n * k) * yn a1 n ≡ 0 [MOD HPow.hPow (β := ℕ) (yn a1 n) 2]
have h₂ : yn a1 n * yn a1 n ∣ d a1 * yn a1 (n * k) * yn a1 n
Tactic: rw [modEq_zero_iff_dvd, sq]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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]
⊢ yn a1 n * yn a1 n ∣ d a1 * yn a1 (n * k) * yn a1 n
have h₂ : yn a1 n ∣ d a1 * yn a1 (n * k)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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]
⊢ yn a1 n ∣ d a1 * yn a1 (n * k)
have h₂ : yn a1 n ∣ yn a1 (n * k)
Tactic: apply dvd_mul_of_dvd_right
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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]
⊢ yn a1 n ∣ yn a1 (n * k)
have h₂ : yn a1 (n * k) ≡ 0 [MOD yn a1 n]
Tactic: rw [← modEq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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]
⊢ yn a1 (n * k) ≡ 0 [MOD yn a1 n]
have h₂ : k * xn a1 n ^ (k - 1) * yn a1 n ≡ 0 [MOD yn a1 n]
Tactic: refine (hy.of_dvd <| dvd_pow_self _ <| by decide).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
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 + 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]
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
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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]
have h₁ : xn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
Tactic: gcongr ?_ + ?_
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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]
⊢ 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]
have h₂ : yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ k * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
Tactic: gcongr ?_ + ?_
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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) 3]
have 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]
Tactic: rw [_root_.pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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
have 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
Tactic: rcases k with - | k
Cleared hypotheses: k, hx, hy, L
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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
⊢ k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n
have 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
Tactic: rcases k with - | k
Cleared hypotheses: k, hx, hy, L
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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 + 1 - 1) * yn a1 n * xn a1 n = (k + 1) * xn a1 n ^ (k + 1) * yn a1 n
have 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
Tactic: simp [_root_.pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
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]
⊢ yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ k * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (goal)
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 * yn a1 n [MOD HPow.hPow (β := ℕ) (yn a1 n) 3]
have 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]
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.NumberTheory.PellMatiyasevic (hypothesis)
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 + 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]
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
  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