-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem eq_pell_lem : ∀ (n) (b : ℤ√(d a1)), 1 ≤ b → IsPell b →
    b ≤ pellZd a1 n → ∃ n, b = pellZd a1 n
  | 0, _ => fun h1 _ hl => ⟨0, @Zsqrtd.le_antisymm _ (dnsq a1) _ _ hl h1⟩
  | n + 1, b => fun h1 hp h =>
    have a1p : (0 : ℤ√(d a1)) ≤ ⟨a, 1⟩ := trivial
    have am1p : (0 : ℤ√(d a1)) ≤ ⟨a, -1⟩ := show (_ : Nat) ≤ _ by simp; exact Nat.pred_le _
    have a1m : (⟨a, 1⟩ * ⟨a, -1⟩ : ℤ√(d a1)) = 1 := isPell_norm.1 (isPell_one a1)
    if ha : (⟨↑a, 1⟩ : ℤ√(d a1)) ≤ b then
      let ⟨m, e⟩ :=
        eq_pell_lem n (b * ⟨a, -1⟩) (by rw [← a1m]; exact mul_le_mul_of_nonneg_right ha am1p)
          (isPell_mul hp (isPell_star.1 (isPell_one a1)))
          (by
            have t := mul_le_mul_of_nonneg_right h am1p
            rwa [pellZd_succ, mul_assoc, a1m, mul_one] at t)
      ⟨m + 1, by
        rw [show b = b * ⟨a, -1⟩ * ⟨a, 1⟩ by rw [mul_assoc, Eq.trans (mul_comm _ _) a1m]; simp,
          pellZd_succ, e]⟩
    else
      suffices ¬1 < b from ⟨0, show b = 1 from (Or.resolve_left (lt_or_eq_of_le h1) this).symm⟩
      fun h1l => by
      obtain ⟨x, y⟩ := b
      exact by
        have bm : (_ * ⟨_, _⟩ : ℤ√d a1) = 1 := Pell.isPell_norm.1 hp
        have y0l : (0 : ℤ√d a1) < ⟨x - x, y - -y⟩ :=
          sub_lt_sub h1l fun hn : (1 : ℤ√d a1) ≤ ⟨x, -y⟩ => by
            have t := mul_le_mul_of_nonneg_left hn (le_trans zero_le_one h1)
            rw [bm, mul_one] at t
            exact h1l t
        have yl2 : (⟨_, _⟩ : ℤ√_) < ⟨_, _⟩ :=
          show (⟨x, y⟩ - ⟨x, -y⟩ : ℤ√d a1) < ⟨a, 1⟩ - ⟨a, -1⟩ from
            sub_lt_sub ha fun hn : (⟨x, -y⟩ : ℤ√d a1) ≤ ⟨a, -1⟩ => by
              have t := mul_le_mul_of_nonneg_right
                      (mul_le_mul_of_nonneg_left hn (le_trans zero_le_one h1)) a1p
              rw [bm, one_mul, mul_assoc, Eq.trans (mul_comm _ _) a1m, mul_one] at t
              exact ha t
        simp only [sub_self, sub_neg_eq_add] at y0l; simp only [Zsqrtd.neg_re, add_neg_cancel,
          Zsqrtd.neg_im, neg_neg] at yl2
        exact
          match y, y0l, (yl2 : (⟨_, _⟩ : ℤ√_) < ⟨_, _⟩) with
          | 0, y0l, _ => y0l (le_refl 0)
          | (y + 1 : ℕ), _, yl2 =>
            yl2
              (Zsqrtd.le_of_le_le (by simp [sub_eq_add_neg])
                (let t := Int.ofNat_le_ofNat_of_le (Nat.succ_pos y)
                add_le_add t t))
          | Int.negSucc _, y0l, _ => y0l trivial

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(Pell.d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
⊢ b * { re := ↑a, im := -1 } ≤ pellZd a1 n

Tactic:
have t := mul_le_mul_of_nonneg_right h am1p

Result:
a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(Pell.d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
t : b * { re := ↑a, im := -1 } ≤ pellZd a1 (n + 1) * { re := ↑a, im := -1 }
⊢ b * { re := ↑a, im := -1 } ≤ pellZd a1 n

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(Pell.d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
⊢ { re := ↑a, im := 1 } * { re := ↑a, im := -1 } ≤ b * { re := ↑a, im := -1 }

Tactic:
exact mul_le_mul_of_nonneg_right ha am1p

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(Pell.d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
m : ℕ
e : b * { re := ↑a, im := -1 } = pellZd a1 m
⊢ b = pellZd a1 (m + 1)

Tactic:
rw [show b = b * ⟨a, -1⟩ * ⟨a, 1⟩ by rw [mul_assoc, Eq.trans (mul_comm _ _) a1m]; simp,
  pellZd_succ, e]

Result:
no goals