-- Mathlib/Data/Real/Archimedean.lean
theorem exists_isLUB (hne : s.Nonempty) (hbdd : BddAbove 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
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n => ↑(f n) / ↑n
⊢ ∃ x, IsLUB s x

Tactic:
let g : CauSeq ℚ abs := ⟨fun n => f n / n, hg⟩

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
g : CauSeq ℚ abs := ⟨fun n => ↑(f n) / ↑n, hg⟩
⊢ ∃ x, IsLUB s x

Proof state:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
⊢ ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}

Tactic:
obtain ⟨k, hk⟩ := exists_int_gt U

Result:
case intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < ↑k
⊢ ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}

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
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * ↑n - 1 < ↑(f n)
⊢ ↑n ≠ 0

Tactic:
exact ne_of_gt (Nat.cast_pos.2 n0)

Result:
no goals

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)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
j0 : 0 < j
k0 : 0 < k
y : ℝ
yS : y ∈ s
hy : ↑(↑(f j) / ↑j) ≤ y
⊢ ↑(↑(f j) / ↑j - ↑(f k) / ↑k) < ↑(↑k)⁻¹

Tactic:
simpa using sub_lt_iff_lt_add'.2 (lt_of_le_of_lt hy <| sub_lt_iff_lt_add.1 <| hf₂ _ k0 _ yS)

Result:
no goals

Proof state:
case intro.intro.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < ↑k
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : ↑z ≤ y * ↑d
⊢ y * ↑d ≤ ↑(k * ↑d)

Tactic:
push_cast

Result:
case intro.intro.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < ↑k
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : ↑z ≤ y * ↑d
⊢ y * ↑d ≤ ↑k * ↑d

Proof state:
case intro.intro.intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < ↑k
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : ↑z ≤ y * ↑d
⊢ y * ↑d ≤ ↑k * ↑d

Tactic:
exact mul_le_mul_of_nonneg_right ((hU yS).trans hk.le) d.cast_nonneg

Result:
no goals

Proof state:
case intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < ↑k
⊢ ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}

Tactic:
refine fun d => ⟨k * d, fun z h => ?_⟩

Result:
case intro
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < ↑k
d : ℕ
z : ℤ
h : z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
⊢ z ≤ k * ↑d

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
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
hy : ↑(f n) ≤ y * ↑n
⊢ ↑(↑(f n) / ↑n) ≤ y

Tactic:
simpa using (div_le_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _)).2 hy

Result:
no goals

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}
⊢ ∃ x, IsLUB s x

Tactic:
choose f hf using fun d : ℕ =>
  Int.exists_greatest_of_bdd (this d) ⟨⌊L * d⌋, L, hL, Int.floor_le _⟩

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
⊢ ∃ 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
this : ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, ↑(f j) / ↑j - ↑(f k) / ↑k < ε
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
⊢ (fun n => ↑(f n) / ↑n) ⌈ε⁻¹⌉₊ - (fun n => ↑(f n) / ↑n) j < ε

Tactic:
exact this _ le_rfl _ ij

Result:
no goals

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
this : ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, ↑(f j) / ↑j - ↑(f k) / ↑k < ε
⊢ ∃ i, ∀ j ≥ i, |(fun n => ↑(f n) / ↑n) j - (fun n => ↑(f n) / ↑n) i| < ε

Tactic:
refine ⟨_, fun j ij => abs_lt.2 ⟨?_, this _ ij _ le_rfl⟩⟩

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
this : ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, ↑(f j) / ↑j - ↑(f k) / ↑k < ε
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
⊢ -ε < (fun n => ↑(f n) / ↑n) j - (fun n => ↑(f n) / ↑n) ⌈ε⁻¹⌉₊

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
⊢ z ≤ ↑(↑g n)

Tactic:
have n0 : 0 < n := Nat.cast_pos.1 ((inv_pos.2 xz).trans_le hK)

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
n0 : 0 < n
⊢ z ≤ ↑(↑g n)

Proof state:
case intro.intro.refine_1
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
⊢ z ≤ mk g

Tactic:
obtain ⟨K, hK⟩ := exists_nat_gt (x - z)⁻¹

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 : ℝ
xz : z < x
K : ℕ
hK : (x - z)⁻¹ < ↑K
⊢ z ≤ mk g