I formalize a proof from Constructive Analysis by Errett Bishop and Douglas Bridger, and notice that there may have been a tiny error in their inequalities. This section of the book is essentially the same as Foundations of Constructive Analysis.

error_in_textbook.lean

import tactic
import algebra.archimedean

def regular (x : ℕ → ℚ) : Prop :=
∀ m n, abs (x m - x n) ≤ m.succ⁻¹ + n.succ⁻¹

/-- Definition 2.1
A `myreal` number is a `regular` sequence of rational numbers -/
structure myreal :=
(seq : ℕ → ℚ) (reg : regular seq)

notation `ℜ` := myreal

namespace myreal

def eq_def (x y : ℜ) : Prop :=
∀ n, abs (x.seq n - y.seq n) ≤ 2 * n.succ⁻¹

notation x ` ≡ ` y := eq_def x y

/-- Helper lemma for demonstration below -/
lemma le_of_add_lt_all' (x y : ℚ) : (∀ n : ℕ, x < y + 3 * n.succ⁻¹) → x ≤ y :=
begin
  intro h,
  contrapose! h, -- Should be constructive since `rat.le` is decidable?
  cases exists_nat_one_div_lt (by linarith : 0 < (x-y)/6) with n hn,
  use n, apply le_of_lt,
  calc y + 3 * (↑(n.succ))⁻¹
      = y + 3 * (1 / (↑n + 1)) : by ring
  ... < y + 3 * ((x-y) / 6) : by apply add_lt_add_left _;rwa mul_lt_mul_left _;norm_num
  ... = (x+y) / 2 : by ring
  ... < x         : by linarith,
end
lemma zero_le_inv_succ (n : ℕ) : (0 : ℚ) ≤ n.succ⁻¹ :=
by rw inv_nonneg; apply le_of_lt; exact_mod_cast nat.succ_pos n

/-- Lemma 2.3
Two `myreal` numbers `x` and `y` are equal if and only if for each natural
number `j` there exists a natural number `N` such that |xₙ - yₙ| ≤ j.succ⁻¹
for all `n ≥ N`. -/
lemma eq_iff (x y : ℜ) : x ≡ y ↔
  ∀ j : ℕ, ∃ N, ∀ n ≥ N, abs (x.seq n - y.seq n) ≤ j.succ⁻¹ :=
begin
  split,
  { intros heq j,
    use 2 * j + 1,
    intros n hn,
    specialize heq n,
    cases nat.le.dest hn with m hm, clear hn,
    rw ←hm at *,
    apply le_trans heq,
    norm_num at *,
    have : (2:ℚ) / (2*j + 1 + m + 1) ≤ 2 / (2*j+2),
    { apply div_le_div,
      norm_num,
      norm_num,
      norm_cast, simp only [nat.succ_pos],
      norm_cast, linarith },
    apply le_trans this,
    rw ← mul_one (2:ℚ),
    rw mul_assoc,
    rw one_mul,
    rw ← mul_add (2:ℚ) j 1,
    rw mul_div_mul_left,
    field_simp only [le_refl],
    norm_num },
  intros h n,
  apply le_of_add_lt_all',
  intro j,
  cases x, cases y, dsimp at *, unfold regular at *,
  cases h j with N hN,
  let m := max j N + 37, -- OVER HERE! Errors below when changed to `m := max j N + 0`
  specialize x_reg n m,
  specialize hN m (le_add_right (le_max_right _ _)),
  specialize y_reg m n,
  have : (m.succ⁻¹ : ℚ) < j.succ⁻¹,
  { field_simp only [nat.cast_succ],
    rw div_lt_iff _,
    rw div_mul_comm', rw mul_one,
    rw lt_div_iff,
      norm_cast, simp only [one_mul],

      -- if `m = max j N`, it errors here. Have to prove `j + 1 < m + 1`
      linarith [le_max_left j N],

      exact_mod_cast nat.succ_pos _,
      exact_mod_cast nat.succ_pos _ },
  calc  abs (x_seq n - y_seq n)
      ≤ abs (x_seq n - x_seq m) +
        abs (x_seq m - y_seq n)   : abs_sub_le _ _ _
  ... ≤ abs (x_seq n - x_seq m) +
        (abs (x_seq m - y_seq m)+
         abs (y_seq m - y_seq n)) : add_le_add (le_refl _) (abs_sub_le _ _ _)
  ... ≤ n.succ⁻¹ + m.succ⁻¹ + (j + 1)⁻¹ + m.succ⁻¹ + n.succ⁻¹ : by linarith
  ... < n.succ⁻¹ + j.succ⁻¹ + (j + 1)⁻¹ + n.succ⁻¹ + j.succ⁻¹ : by linarith
  ... = 2 * (↑n + 1)⁻¹ + 3 * (↑j + 1)⁻¹ : by norm_cast; ring,
end

end myreal