-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem eq_of_xn_modEq' {i j n} (ipos : 0 < i) (hin : i ≤ n) (j4n : j ≤ 4 * n)
    (h : xn a1 j ≡ xn a1 i [MOD xn a1 n]) : j = i ∨ j + i = 4 * n :=
  have i2n : i ≤ 2 * n

Proof state:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : 2 ≤ 1
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
x✝¹ : a = 2
n1 : n = 1
x✝ : j = 0
i2 : i = 2
⊢ False

Tactic:
exact absurd hin (by decide)

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : 2 ≤ 1
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
x✝¹ : a = 2
n1 : n = 1
x✝ : j = 0
i2 : i = 2
⊢ ¬2 ≤ 1

Tactic:
decide

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
x✝¹ : a = 2
n1 : n = 1
x✝ : j = 0
i2 : i = 2
⊢ False

Tactic:
rw [n1, i2] at hin

Result:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : 2 ≤ 1
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
x✝¹ : a = 2
n1 : n = 1
x✝ : j = 0
i2 : i = 2
⊢ False

Proof state:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
⊢ 4 * n - j ≤ 2 * n

Tactic:
omega

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ n ≤ n + n

Tactic:
apply Nat.le_add_left

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ i ≤ 2 * n

Tactic:
apply le_trans hin

Result:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ n ≤ 2 * n

Proof state:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
j42n : 4 * n - j ≤ 2 * n
⊢ xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]

Tactic:
let t := xn_modEq_x4n_sub a1 j42n

Result:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
j42n : 4 * n - j ≤ 2 * n
t : xn a1 (4 * n - (4 * n - j)) ≡ xn a1 (4 * n - j) [MOD xn a1 n] := xn_modEq_x4n_sub a1 j42n
⊢ xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
j42n : 4 * n - j ≤ 2 * n
⊢ a = 2 → n = 1 → (i = 0 → 4 * n - j ≠ 2) ∧ (i = 2 → 4 * n - j ≠ 0)

Tactic:
omega

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
this : i = 4 * n - j
⊢ j + i = 4 * n

Tactic:
rw [this, add_tsub_cancel_of_le j4n]

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
j42n : 4 * n - j ≤ 2 * n
t : xn a1 (4 * n - (4 * n - j)) ≡ xn a1 (4 * n - j) [MOD xn a1 n] := xn_modEq_x4n_sub a1 j42n
⊢ xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]

Tactic:
rwa [tsub_tsub_cancel_of_le j4n] at t

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ n ≤ 2 * n

Tactic:
rw [two_mul]

Result:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ n ≤ n + n