-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem eq_of_xn_modEq_lem3 {i n} (npos : 0 < n) :
    ∀ {j}, i < j → j ≤ 2 * n → j ≠ n → ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2) →
        xn a1 i % xn a1 n < xn a1 j % xn a1 n
  | 0, ij, _, _, _ => absurd ij (Nat.not_lt_zero _)
  | j + 1, ij, j2n, jnn, ntriv =>
    have lem2 : ∀ k > n, k ≤ 2 * n → (↑(xn a1 k % xn a1 n) : ℤ) =
        xn a1 n - xn a1 (2 * n - k) := fun k kn k2n => by
      let k2nl :=
        lt_of_add_lt_add_right <|
          show 2 * n - k + k < n + k by
            rw [tsub_add_cancel_of_le]
            · rw [two_mul]
              exact add_lt_add_left kn n
            exact k2n
      have xle : xn a1 (2 * n - k) ≤ xn a1 n := le_of_lt <| strictMono_x a1 k2nl
      suffices xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k) by rw [this, Int.ofNat_sub xle]
      rw [← Nat.mod_eq_of_lt (Nat.sub_lt (x_pos a1 n) (x_pos a1 (2 * n - k)))]
      apply ModEq.add_right_cancel' (xn a1 (2 * n - k))
      rw [tsub_add_cancel_of_le xle]
      have t := xn_modEq_x2n_sub_lem a1 k2nl.le
      rw [tsub_tsub_cancel_of_le k2n] at t
      exact t.trans dvd_rfl.zero_modEq_nat
    (lt_trichotomy j n).elim (fun jn : j < n => eq_of_xn_modEq_lem1 _ ij (lt_of_le_of_ne jn jnn))
      fun o =>
      o.elim
        (fun jn : j = n => by
          cases jn
          apply Int.lt_of_ofNat_lt_ofNat
          rw [lem2 (n + 1) (Nat.lt_succ_self _) j2n,
            show 2 * n - (n + 1) = n - 1 by
              rw [two_mul, tsub_add_eq_tsub_tsub, add_tsub_cancel_right]]
          refine lt_sub_left_of_add_lt (Int.ofNat_lt_ofNat_of_lt ?_)
          rcases lt_or_eq_of_le <| Nat.le_of_succ_le_succ ij with lin | ein
          · rw [Nat.mod_eq_of_lt (strictMono_x _ lin)]
            have ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n

Proof state:
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n

Tactic:
rcases lt_or_eq_of_le il with ill | ile

Result:
case refl.a.inl.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ill : i < n - 1
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n

case refl.a.inl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n

Proof state:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ n + n < n + k

Tactic:
exact add_lt_add_left kn n

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n)))
        (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]

Tactic:
have t := xn_modEq_x2n_sub_lem a1 k2nl.le

Result:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n)))
        (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 (2 * n - (2 * n - k)) + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n)))
        (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n - xn a1 (2 * n - k) + xn a1 (2 * n - k) [MOD xn a1 n]

Tactic:
rw [tsub_add_cancel_of_le xle]

Result:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n)))
        (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n)))
        (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 (2 * n - (2 * n - k)) + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]

Tactic:
rw [tsub_tsub_cancel_of_le k2n] at t

Result:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n :=
  lt_of_add_lt_add_right
    (let_fun this :=
      Eq.mpr (id (congrArg (fun _a => _a < n + k) (tsub_add_cancel_of_le k2n)))
        (Eq.mpr (id (congrArg (fun _a => _a < n + k) (two_mul n))) (add_lt_add_left kn n));
    this)
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 k + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]

Proof state:
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n

Tactic:
have il : i ≤ n - 1 := by
  apply Nat.le_of_succ_le_succ
  rw [npm]
  exact lin

Result:
case refl.a.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n