x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
⊢ ∃ x, f ≈ const abs x
x y : ℝ
f : CauSeq ℝ abs
⊢ ∃ x, f ≈ const abs x
let S := { x : ℝ | const abs x < f }
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
⊢ ∃ x, f ≈ const abs x
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
⊢ ∃ x, f ≈ const abs x
have lb : ∃ x, x ∈ S := exists_lt f
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
⊢ ∃ x, f ≈ const abs x
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
⊢ ∃ x, f ≈ const abs x
have ub' : ∀ x, f < const abs x → ∀ y ∈ S, y ≤ x := fun x h y yS =>
  le_of_lt <| const_lt.1 <| CauSeq.lt_trans yS h
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
⊢ ∃ x, f ≈ const abs x
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
⊢ ∃ x, f ≈ const abs x
have ub : ∃ x, ∀ y ∈ S, y ≤ x := (exists_gt f).imp ub'
case refine'_1
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
h : f < const abs (sSup S)
⊢ False

case refine'_2
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
h : const abs (sSup S) < f
⊢ False
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
⊢ ∃ x, f ≈ const abs x
refine' ⟨sSup S, ((lt_total _ _).resolve_left fun h => _).resolve_right fun h => _⟩
case refine'_1.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(const abs (sSup S) - f) j
⊢ False
case refine'_1
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
h : f < const abs (sSup S)
⊢ False
rcases h with ⟨ε, ε0, i, ih⟩
case refine'_1.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(const abs (sSup S) - f) j
⊢ f < const abs (sSup S - ε / 2)
case refine'_1.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(const abs (sSup S) - f) j
⊢ False
refine' (csSup_le lb (ub' _ _)).not_lt (sub_lt_self _ (half_pos ε0))
case refine'_1.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(const abs (sSup S) - f) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑(const abs (sSup S - ε / 2) - f) j
case refine'_1.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(const abs (sSup S) - f) j
⊢ f < const abs (sSup S - ε / 2)
refine' ⟨_, half_pos ε0, i, fun j ij => _⟩
case refine'_1.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(const abs (sSup S) - f) j
j : ℕ
ij : j ≥ i
⊢ ε ≤ sSup S - ↑f j
case refine'_1.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(const abs (sSup S) - f) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑(const abs (sSup S - ε / 2) - f) j
rw [sub_apply, const_apply, sub_right_comm, le_sub_iff_add_le, add_halves]
no goals
case refine'_1.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(const abs (sSup S) - f) j
j : ℕ
ij : j ≥ i
⊢ ε ≤ sSup S - ↑f j
exact ih _ ij
case refine'_2.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(f - const abs (sSup S)) j
⊢ False
case refine'_2
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
h : const abs (sSup S) < f
⊢ False
rcases h with ⟨ε, ε0, i, ih⟩
case refine'_2.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(f - const abs (sSup S)) j
⊢ ε / 2 + sSup S ∈ S
case refine'_2.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(f - const abs (sSup S)) j
⊢ False
refine' (le_csSup ub _).not_lt ((lt_add_iff_pos_left _).2 (half_pos ε0))
case refine'_2.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(f - const abs (sSup S)) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑(f - const abs (ε / 2 + sSup S)) j
case refine'_2.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(f - const abs (sSup S)) j
⊢ ε / 2 + sSup S ∈ S
refine' ⟨_, half_pos ε0, i, fun j ij => _⟩
case refine'_2.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(f - const abs (sSup S)) j
j : ℕ
ij : j ≥ i
⊢ ε ≤ ↑f j - sSup S
case refine'_2.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(f - const abs (sSup S)) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑(f - const abs (ε / 2 + sSup S)) j
rw [sub_apply, const_apply, add_comm, ← sub_sub, le_sub_iff_add_le, add_halves]
no goals
case refine'_2.intro.intro.intro
x y : ℝ
f : CauSeq ℝ abs
S : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ S
ub' : ∀ (x : ℝ), f < const abs x → ∀ (y : ℝ), y ∈ S → y ≤ x
ub : ∃ x, ∀ (y : ℝ), y ∈ S → y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ (j : ℕ), j ≥ i → ε ≤ ↑(f - const abs (sSup S)) j
j : ℕ
ij : j ≥ i
⊢ ε ≤ ↑f j - sSup S
exact ih _ ij