-- Mathlib/Data/Real/Archimedean.lean
theorem exists_isLUB (hne : s.Nonempty) (hbdd : BddAbove s) : ∃ x, IsLUB s x

Proof state:
case intro.intro.refine_1.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n => ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
z : ℝ
K n : ℕ
nK : n ≥ K
xz : 0 < x - z
hK : (x - z)⁻¹ ≤ ↑n
n0 : 0 < n
⊢ z ≤ x - (↑n)⁻¹

Tactic:
rwa [le_sub_comm, inv_le_comm₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _) xz]

Result:
no goals

Proof state:
case intro.intro.refine_1.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n => ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
z : ℝ
xz : z < x
K : ℕ
hK : (x - z)⁻¹ < ↑K
n : ℕ
nK : n ≥ K
⊢ z ≤ ↑(↑g n)

Tactic:
replace xz := sub_pos.2 xz

Result:
case intro.intro.refine_1.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n => ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
z : ℝ
K : ℕ
hK : (x - z)⁻¹ < ↑K
n : ℕ
nK : n ≥ K
xz : 0 < x - z
⊢ z ≤ ↑(↑g n)

Proof state:
case intro.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
⊢ ∃ x, IsLUB s x

Tactic:
have hg : IsCauSeq abs (fun n => f n / n : ℕ → ℚ) := by
  intro ε ε0
  suffices ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, (f j / j - f k / k : ℚ) < ε by
    refine ⟨_, fun j ij => abs_lt.2 ⟨?_, this _ ij _ le_rfl⟩⟩
    rw [neg_lt, neg_sub]
    exact this _ le_rfl _ ij
  intro j ij k ik
  replace ij := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ij)
  replace ik := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ik)
  have j0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ij)
  have k0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ik)
  rcases hf₁ _ j0 with ⟨y, yS, hy⟩
  refine lt_of_lt_of_le ((Rat.cast_lt (K := ℝ)).1 ?_) ((inv_le_comm₀ ε0 (Nat.cast_pos.2 k0)).1 ik)
  simpa using sub_lt_iff_lt_add'.2 (lt_of_le_of_lt hy <| sub_lt_iff_lt_add.1 <| hf₂ _ k0 _ yS)

Result:
case intro.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
⊢ ∃ x, IsLUB s x

Proof state:
case intro.intro.refine_1.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n => ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
z : ℝ
K : ℕ
hK : (x - z)⁻¹ < ↑K
n : ℕ
nK : n ≥ K
xz : 0 < x - z
⊢ z ≤ ↑(↑g n)

Tactic:
replace hK := hK.le.trans (Nat.cast_le.2 nK)

Result:
case intro.intro.refine_1.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n => ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
z : ℝ
K n : ℕ
nK : n ≥ K
xz : 0 < x - z
hK : (x - z)⁻¹ ≤ ↑n
⊢ z ≤ ↑(↑g n)

Proof state:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |(fun n => ↑(f n) / ↑n) j - (fun n => ↑(f n) / ↑n) i| < ε

Tactic:
suffices ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, (f j / j - f k / k : ℚ) < ε by
  refine ⟨_, fun j ij => abs_lt.2 ⟨?_, this _ ij _ le_rfl⟩⟩
  rw [neg_lt, neg_sub]
  exact this _ le_rfl _ ij

Result:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
⊢ ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, ↑(f j) / ↑j - ↑(f k) / ↑k < ε

Proof state:
s : Set ℝ
hne : s.Nonempty
hbdd : BddAbove s
⊢ ∃ x, IsLUB s x

Tactic:
rcases hne, hbdd with ⟨⟨L, hL⟩, ⟨U, hU⟩⟩

Result:
case intro.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
⊢ ∃ x, IsLUB s x

Proof state:
case intro.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
⊢ ∃ x, IsLUB s x

Tactic:
have hf₂ : ∀ n > 0, ∀ y ∈ s, (y - ((n : ℕ) : ℝ)⁻¹) < (f n / n : ℚ) := by
  intro n n0 y yS
  have := (Int.sub_one_lt_floor _).trans_le (Int.cast_le.2 <| (hf n).2 _ ⟨y, yS, Int.floor_le _⟩)
  simp only [Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast, gt_iff_lt]
  rwa [lt_div_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _), sub_mul, inv_mul_cancel₀]
  exact ne_of_gt (Nat.cast_pos.2 n0)

Result:
case intro.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
⊢ ∃ x, IsLUB s x

Proof state:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
j0 : 0 < j
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε

Tactic:
have k0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ik)

Result:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
j0 : 0 < j
k0 : 0 < k
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε