case intro
x✝ y : ℝ
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑(↑f j) ≤ x
⊢ mk f ≤ x
x✝ y : ℝ
f : CauSeq ℚ abs
x : ℝ
h : ∃ i, ∀ (j : ℕ), j ≥ i → ↑(↑f j) ≤ x
⊢ mk f ≤ x
cases' h with i H
case intro
x✝ y : ℝ
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑(↑f j) ≤ x
⊢ -x ≤ mk (-f)
case intro
x✝ y : ℝ
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑(↑f j) ≤ x
⊢ mk f ≤ x
rw [← neg_le_neg_iff, ← mk_neg]
no goals
case intro
x✝ y : ℝ
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑(↑f j) ≤ x
⊢ -x ≤ mk (-f)
exact le_mk_of_forall_le ⟨i, fun j ij => by simp [H _ ij]⟩
no goals
x✝ y : ℝ
f : CauSeq ℚ abs
x : ℝ
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ↑(↑f j) ≤ x
j : ℕ
ij : j ≥ i
⊢ -x ≤ ↑(↑(-f) j)
simp [H _ ij]